Commit e017894d authored by Martin Clochard's avatar Martin Clochard

Mini-compiler: loop in progress

parent b041d198
......@@ -151,7 +151,33 @@ module Compiler_logic
end
meta rewrite prop trivial_pre_lemma
inductive acc ('a -> 'a -> bool) 'a =
| Acc : forall r,x:'a. (forall y. r y x -> acc r y) -> acc r x
function loop_post (inv:'a -> pos -> pred)
(var:'a -> pos -> post)
(post:'a -> pos -> post)
(x:'a)
(p:pos)
(ms:machine_state) : pred =
\ms'. (inv x p ms /\ var x p ms' ms) \/ post x p ms ms'
meta rewrite_def function loop_post
(* Variant of hoare triplet introduction rule for looping code. *)
let make_loop (c:wp 'a)
(ghost inv:'a -> pos -> pred)
(ghost var: 'a -> pos -> post)
(ghost post : 'a -> pos -> post) : hl 'a
requires { wp_correctness c }
requires { forall x p ms. inv x p ms -> acc (var x p) ms }
requires { forall x p ms. inv x p ms ->
(c.wp x p (loop_post inv var post x p ms)) ms }
ensures { result.pre = inv /\ result.post = post }
ensures { result.code.length = c.wcode.length /\ hl_correctness result }
= { code = c.wcode ; pre = inv ; post = post }
end
......@@ -159,4 +185,4 @@ end
Local Variables:
compile-command: "why3 ide -L . logic.mlw"
End:
*)
\ No newline at end of file
*)
......@@ -2,27 +2,28 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../logic.mlw" expanded="true">
<theory name="Compiler_logic" sum="9dcaf842383ff8f3b36434fd4a939892" expanded="true">
<theory name="Compiler_logic" sum="278b30fc74b84398bcf3b01149ec3ca2" expanded="true">
<goal name="seq_wp_lemma">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter infix ~" expl="VC for infix ~" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter infix ~.1" expl="1. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter infix ~.1.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter infix ~.1.2" expl="2. assertion" expanded="true">
<transf name="simplify_trivial_quantification_in_goal" expanded="true">
<goal name="WP_parameter infix ~.1.2.1" expl="1." expanded="true">
<transf name="compute_specified" expanded="true">
<goal name="WP_parameter infix ~.1.2.1.1" expl="1.">
<proof prover="1"><result status="valid" time="0.23"/></proof>
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
......@@ -31,39 +32,51 @@
</transf>
</goal>
<goal name="WP_parameter infix ~.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter infix ~.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="fork_wp_lemma" expanded="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter infix %" expl="VC for infix %">
<transf name="split_goal_wp">
<goal name="WP_parameter infix %.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.10"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
<goal name="towp_wp_lemma">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prefix $" expl="VC for prefix $">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hoare" expl="VC for hoare">
<transf name="split_goal_wp">
<goal name="WP_parameter hoare.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="trivial_pre_lemma">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter make_loop" expl="VC for make_loop" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter make_loop.1" expl="1. postcondition" expanded="true">
<proof prover="2"><result status="unknown" time="0.04"/></proof>
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter make_loop.1.1" expl="1. postcondition" expanded="true">
<proof prover="0" edited="logic_Compiler_logic_WP_parameter_make_loop_1.v" obsolete="true"><undone/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../specs.mlw" expanded="true">
<theory name="VM_arith_instr_spec" sum="286760edf6bd01966f483d98d4242ea2" expanded="true">
<theory name="VM_arith_instr_spec" sum="286760edf6bd01966f483d98d4242ea2">
<goal name="WP_parameter iconstf" expl="VC for iconstf">
<proof prover="2" obsolete="true"><result status="unknown" time="0.07"/></proof>
<transf name="split_goal_wp">
......@@ -236,16 +236,16 @@
<goal name="WP_parameter ibgtf" expl="VC for ibgtf">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="isetvar_pre_lemma" expanded="true">
<goal name="isetvar_pre_lemma">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="isetvar_post_lemma" expanded="true">
<goal name="isetvar_post_lemma">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter isetvarf" expl="VC for isetvarf" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter isetvarf.1" expl="1. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter isetvarf" expl="VC for isetvarf">
<transf name="split_goal_wp">
<goal name="WP_parameter isetvarf.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter isetvarf.1.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
......@@ -263,8 +263,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter isetvarf.2" expl="2. postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter isetvarf.2" expl="2. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter isetvarf.2.1" expl="1.">
<proof prover="2"><result status="valid" time="0.04"/></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