Commit 2f1058c9 authored by Martin Clochard's avatar Martin Clochard

examples/double_wp: removed useless assertion

parent f158fe58
......@@ -23,12 +23,7 @@ module VM_instr_spec
ensures { result.pre --> pre }
ensures { result.post --> ifun_post f }
ensures { result.code --> code_f }
= let res = { pre = pre; code = code_f; post = ifun_post f } in
assert { forall x p ms. res.pre x p ms ->
not (exists ms' : machine_state. res.post x p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
contextual_irrelevance res.code p ms (f ms) && false };
res
= { pre = pre; code = code_f; post = ifun_post f }
(* Iconst spec *)
function iconst_post (n:int) : post 'a =
......
......@@ -5,29 +5,19 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../specs.mlw">
<theory name="VM_instr_spec" sum="a2d376bbabfff098d8d58fcfaf7df286">
<theory name="VM_instr_spec" sum="eb61121de19a3bce4f33bac444dd60ff">
<goal name="VC ifunf" expl="VC for ifunf">
<transf name="split_goal_wp">
<goal name="VC ifunf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC ifunf.2" expl="2. assertion">
<transf name="split_goal_wp">
<goal name="VC ifunf.2.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC ifunf.2.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="VC ifunf.3" expl="3. postcondition">
<goal name="VC ifunf.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
</goal>
<goal name="VC ifunf.4" expl="4. postcondition">
<goal name="VC ifunf.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
<goal name="VC ifunf.5" expl="5. postcondition">
<goal name="VC ifunf.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
</transf>
......
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