Commit 9cd7a836 authored by Martin Clochard's avatar Martin Clochard

double wp: added invariant witnesses

parent 9ea8a6a4
......@@ -41,6 +41,7 @@ module Compiler_logic
(* (Total) correctness for hoare triple. *)
invariant { forall x:'a,p ms. pre x p ms ->
exists ms'. post x p ms ms' /\ contextual_irrelevance code p ms ms' }
by { code = Nil; pre = (fun _ _ _ -> false); post = fun _ _ _ _ -> true }
(* Predicate transformer type. Same auxiliary variables as for
Hoare triples. *)
......@@ -51,6 +52,7 @@ module Compiler_logic
(* Similar invariant for backward predicate transformers *)
invariant { forall x:'a,p post ms. wp x p post ms ->
exists ms'. post ms' /\ contextual_irrelevance wcode p ms ms' }
by { wcode = Nil; wp = fun _ _ _ _ -> false }
(* WP combinator for sequence. Similar to the standard WP calculus
for sequence. The initial machine state is memorized in auxiliary
......
......@@ -6,7 +6,13 @@
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="1e34499ffffb0c2ecbb89014ad0e345a">
<theory name="Compiler_logic" sum="597c541efd25a851253c429676f44981">
<goal name="VC hl" expl="VC for hl">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC wp" expl="VC for wp">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="seq_wp_lemma" expl="">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
......
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