Skip to content

GitLab

Commit 4b5cd36b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

WP, revised specs

parent af595b50
Hide whitespace changes
Inline Side-by-side
Showing with 70 additions and 149 deletions
examples/hoare_logic/wp2.mlw
View file @ 4b5cd36b
......@@ -262,6 +262,7 @@ use import Imp
function my_sigma : env = IdMap.const (Vint 42)
function my_pi : env = IdMap.const (Vint 0)
(*
goal Test13 :
eval_term my_sigma my_pi (Tconst 13) = Vint 13
......@@ -290,6 +291,7 @@ goal If42 :
sigma1 pi1 i ->
one_step sigma1 pi1 i sigma2 pi2 Sskip ->
IdMap.get sigma2 x = Vint 13
*)
end
......@@ -409,10 +411,11 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
val abstract_effects (i:stmt) (f:fmla) :
{ }
fmla
{ forall sigma pi sigma' pi':env, w:Set.set ident .
eval_fmla sigma pi f /\ stmt_writes i w /\
assigns sigma w sigma' ->
eval_fmla sigma' pi' result
{ forall sigma pi. eval_fmla sigma pi result ->
eval_fmla sigma pi f /\
forall sigma':env, w:Set.set ident.
stmt_writes i w /\ assigns sigma w sigma' ->
eval_fmla sigma' pi result
}
use HoareLogic
......
examples/hoare_logic/wp2/why3session.xml
View file @ 4b5cd36b
......@@ -210,101 +210,19 @@
name="TestSemantics"
locfile="wp2/../wp2.mlw"
loclnum="258" loccnumb="7" loccnume="20"
verified="false"
verified="true"
expanded="false">
<goal
name="Test13"
locfile="wp2/../wp2.mlw"
loclnum="265" loccnumb="5" loccnume="11"
sum="3c0145de004805afee4e91f7151c1d16"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTconstc13aVintc13">
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Test42"
locfile="wp2/../wp2.mlw"
loclnum="268" loccnumb="5" loccnume="11"
sum="2690191a2bfcc08e60123ee2d86d7bf5"
proved="false"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTvarc0aVintc42">
</goal>
<goal
name="Test0"
locfile="wp2/../wp2.mlw"
loclnum="271" loccnumb="5" loccnume="10"
sum="14eb3f7d7a707d06d898b3d763778657"
proved="false"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTderefc0aVintc0">
</goal>
<goal
name="Test55"
locfile="wp2/../wp2.mlw"
loclnum="274" loccnumb="5" loccnume="11"
sum="f4197d0d0abee013d73676fc07b57572"
proved="false"
expanded="false"
shape="ainfix =aeval_termamy_sigmaamy_piaTbinaTvarc0aOplusaTconstc13aVintc55">
</goal>
<goal
name="Ass42"
locfile="wp2/../wp2.mlw"
loclnum="277" loccnumb="5" loccnume="10"
sum="823cc8d3bbaf972bd76e091707e41d1d"
proved="true"
expanded="false"
shape="Lc0ainfix =agetV1V0aVintc42Iaone_stepamy_sigmaamy_piaSassignV0aTconstc42V1V2aSskipF">
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="If42"
locfile="wp2/../wp2.mlw"
loclnum="283" loccnumb="5" loccnume="9"
sum="f42228f6e306eb1bb41ba44d96ef30a4"
proved="false"
expanded="false"
shape="Lc0ainfix =agetV3V0aVintc13Iaone_stepV1V2V5V3V4aSskipIaone_stepamy_sigmaamy_piaSifaTbinaTderefV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V2V5F">
</goal>
</theory>
<theory
name="HoareLogic"
locfile="wp2/../wp2.mlw"
loclnum="297" loccnumb="7" loccnume="17"
loclnum="299" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
<goal
name="consequence_rule"
locfile="wp2/../wp2.mlw"
loclnum="304" loccnumb="6" loccnume="22"
loclnum="306" loccnumb="6" loccnume="22"
sum="c1f5595ddd954b6361531a9cb635279b"
proved="true"
expanded="false"
......@@ -327,7 +245,7 @@
<goal
name="skip_rule"
locfile="wp2/../wp2.mlw"
loclnum="311" loccnumb="6" loccnume="15"
loclnum="313" loccnumb="6" loccnume="15"
sum="73e47f5d6901d2f852f0c089cfe9027d"
proved="true"
expanded="false"
......@@ -344,7 +262,7 @@
<goal
name="assign_rule"
locfile="wp2/../wp2.mlw"
loclnum="314" loccnumb="6" loccnume="17"
loclnum="316" loccnumb="6" loccnume="17"
sum="5ad7f36cb5982497693bbd3917b38dd5"
proved="true"
expanded="false"
......@@ -361,7 +279,7 @@
<goal
name="seq_rule"
locfile="wp2/../wp2.mlw"
loclnum="319" loccnumb="6" loccnume="14"
loclnum="321" loccnumb="6" loccnume="14"
sum="1a26088dc2dd29482c5092b6ac4ff809"
proved="true"
expanded="false"
......@@ -384,7 +302,7 @@
<goal
name="if_rule"
locfile="wp2/../wp2.mlw"
loclnum="324" loccnumb="6" loccnume="13"
loclnum="326" loccnumb="6" loccnume="13"
sum="3bebb0334fdf15d6238553f897994e1d"
proved="true"
expanded="false"
......@@ -401,7 +319,7 @@
<goal
name="assert_rule"
locfile="wp2/../wp2.mlw"
loclnum="330" loccnumb="6" loccnume="17"
loclnum="332" loccnumb="6" loccnume="17"
sum="b11afd1baac4615f908daadec96d093c"
proved="true"
expanded="false"
......@@ -418,7 +336,7 @@
<goal
name="assert_rule_ext"
locfile="wp2/../wp2.mlw"
loclnum="334" loccnumb="6" loccnume="21"
loclnum="336" loccnumb="6" loccnume="21"
sum="189817af6b3e698754f066618e6681a5"
proved="true"
expanded="false"
......@@ -435,7 +353,7 @@
<goal
name="while_rule"
locfile="wp2/../wp2.mlw"
loclnum="338" loccnumb="6" loccnume="16"
loclnum="340" loccnumb="6" loccnume="16"
sum="a1136f47e552feb3c79f635b836bda93"
proved="true"
expanded="false"
......@@ -452,7 +370,7 @@
<goal
name="while_rule_ext"
locfile="wp2/../wp2.mlw"
loclnum="343" loccnumb="6" loccnume="20"
loclnum="345" loccnumb="6" loccnume="20"
sum="2b6ff464c6bc40e843b0c4d2e7536e09"
proved="true"
expanded="false"
......@@ -470,13 +388,13 @@
<theory
name="WP WP"
locfile="wp2/../wp2.mlw"
loclnum="354" loccnumb="7" loccnume="9"
loclnum="356" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="assigns_refl"
locfile="wp2/../wp2.mlw"
loclnum="364" loccnumb="6" loccnume="18"
loclnum="366" loccnumb="6" loccnume="18"
sum="aa2d95740fab1e3635f694dc96c50567"
proved="true"
expanded="false"
......@@ -492,7 +410,7 @@
<goal
name="assigns_trans"
locfile="wp2/../wp2.mlw"
loclnum="367" loccnumb="6" loccnume="19"
loclnum="369" loccnumb="6" loccnume="19"
sum="0cbbe8a4a0bb524c9eb5267c2e165996"
proved="true"
expanded="false"
......@@ -508,7 +426,7 @@
<goal
name="assigns_union_left"
locfile="wp2/../wp2.mlw"
loclnum="372" loccnumb="6" loccnume="24"
loclnum="374" loccnumb="6" loccnume="24"
sum="00edb9a60872fe96f7f07d1664b5b784"
proved="true"
expanded="false"
......@@ -524,7 +442,7 @@
<goal
name="assigns_union_right"
locfile="wp2/../wp2.mlw"
loclnum="376" loccnumb="6" loccnume="25"
loclnum="378" loccnumb="6" loccnume="25"
sum="70bd82cb54615334f173042f254c5bd9"
proved="true"
expanded="false"
......@@ -540,7 +458,7 @@
<goal
name="WP_parameter compute_writes"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="3849436ee1eee91832ef0eacdb5cc631"
proved="true"
......@@ -556,7 +474,7 @@
<goal
name="WP_parameter compute_writes.1"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="617e33b55d788337118c187682240436"
proved="true"
......@@ -576,7 +494,7 @@
<goal
name="WP_parameter compute_writes.2"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="a171b6344c0547d9efeb5733ca857b31"
proved="true"
......@@ -597,7 +515,7 @@
<goal
name="WP_parameter compute_writes.3"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="2b26b707574663ac9ea048af46720f50"
proved="true"
......@@ -624,7 +542,7 @@
<goal
name="WP_parameter compute_writes.4"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="2164b09f70565800acd808d0bf162dd5"
proved="true"
......@@ -645,7 +563,7 @@
<goal
name="WP_parameter compute_writes.5"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="0be8bdb7f61dabda5ba8bc28b2d663e0"
proved="true"
......@@ -666,7 +584,7 @@
<goal
name="WP_parameter compute_writes.6"
locfile="wp2/../wp2.mlw"
loclnum="390" loccnumb="10" loccnume="24"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="48ff95e748cba004c021eb0709567b1b"
proved="true"
......@@ -689,7 +607,7 @@
<goal
name="WP_parameter wp"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="1c0a7c65274132adb38c610fc4d856c7"
proved="false"
......@@ -705,7 +623,7 @@
<goal
name="WP_parameter wp.1"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="0ce0bf0a1a09361d7e5c1fae11f4320c"
proved="true"
......@@ -753,7 +671,7 @@
<goal
name="WP_parameter wp.2"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="659a8041ce0bdaf08e7037f521c9f105"
proved="true"
......@@ -801,7 +719,7 @@
<goal
name="WP_parameter wp.3"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="6130c16879ea5938d8b47ef1d0ab33a4"
proved="true"
......@@ -849,7 +767,7 @@
<goal
name="WP_parameter wp.4"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="5071f85b66d874821196c755dd2cc8d3"
proved="true"
......@@ -870,7 +788,7 @@
<goal
name="WP_parameter wp.5"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="50f5658baca164788a4475bd94d7bef2"
proved="true"
......@@ -918,7 +836,7 @@
<goal
name="WP_parameter wp.6"
locfile="wp2/../wp2.mlw"
loclnum="420" loccnumb="10" loccnume="12"
loclnum="422" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="98170f17b41280901c84f1c84f14916b"
proved="false"
......@@ -952,7 +870,7 @@
prover="3"
timelimit="3"
edited="wp2_WP_WP_WP_parameter_wp_2.v"
obsolete="false"
obsolete="true"
archived="false">
<result status="unknown" time="1.06"/>
</proof>
......
examples/hoare_logic/wp2/wp2_WP_WP_WP_parameter_wp_2.v
View file @ 4b5cd36b
......@@ -276,38 +276,6 @@ Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (sigma:(map
forall (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi i sigmaqt piqt Sskip n) -> (eval_fmla sigmaqt piqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Parameter set1 : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set1 a) -> Prop.
......@@ -414,6 +382,38 @@ Fixpoint stmt_writes(i:stmt) (w:(set1 Z)) {struct i}: Prop :=
end.
Unset Implicit Arguments.
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
(* Why3 goal *)
Theorem WP_parameter_wp : forall (i:stmt), forall (q:fmla),
match i with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment