Commit ac1738ba authored by MARCHE Claude's avatar MARCHE Claude

more on hoare logic example

parent 26e6db7c
...@@ -242,21 +242,21 @@ ...@@ -242,21 +242,21 @@
</goal> </goal>
<goal <goal
name="many_steps_seq" name="many_steps_seq"
sum="dae00dd4ef3b6c0bd2bac324a43f8912" sum="771cc1d253a080268858269035654fe7"
proved="false" proved="false"
expanded="true" expanded="true"
shape="amany_stepsV4V3V1aSskipAamany_stepsV0V2V4aSskipEIamany_stepsV0aSseqV2V3V1aSskipF"> shape="amany_stepsV6V4V1aSskipAamany_stepsV0V3V6aSskipEIainfix =V5aSskipIainfix =V2aSseqV3V4Iamany_stepsV0V2V1V5F">
<proof <proof
prover="coq" prover="coq"
timelimit="5" timelimit="5"
edited="imp_Imp_many_steps_seq_1.v" edited="imp_Imp_many_steps_seq_1.v"
obsolete="false"> obsolete="true">
<result status="unknown" time="0.46"/> <result status="failure" time="0.45"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="eval_subst_expr" name="eval_subst_expr"
sum="14cc95a56d17cee5b1dc5efb931894d4" sum="dc8b48dfb119a06daa12809a1bc8a37d"
proved="false" proved="false"
expanded="true" expanded="true"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F"> shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
...@@ -264,49 +264,49 @@ ...@@ -264,49 +264,49 @@
prover="coq" prover="coq"
timelimit="5" timelimit="5"
edited="imp_Imp_eval_subst_expr_1.v" edited="imp_Imp_eval_subst_expr_1.v"
obsolete="false"> obsolete="true">
<result status="unknown" time="0.43"/> <result status="unknown" time="0.43"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="eval_subst" name="eval_subst"
sum="de5b9237db9ed93a3dc89a621ff33ac1" sum="db6e0424463873d4f3f5d039496a3510"
proved="true" proved="false"
expanded="false" expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1Iaeval_fmlaV0asubstV1V2V3F"> shape="aeval_fmlaasetV0V2aeval_exprV0V3V1Iaeval_fmlaV0asubstV1V2V3F">
<proof <proof
prover="coq" prover="coq"
timelimit="5" timelimit="5"
edited="imp_Imp_eval_subst_2.v" edited="imp_Imp_eval_subst_2.v"
obsolete="false"> obsolete="true">
<result status="valid" time="0.43"/> <result status="valid" time="0.43"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="assign_rule" name="assign_rule"
sum="41acd7707b568b56dbfbf43c39dc9142" sum="b128e9cf9280645c89fbe34176dc53b8"
proved="true" proved="false"
expanded="false" expanded="false"
shape="avalid_tripleaTasubstV0V1V2aSassignV1V2V0F"> shape="avalid_tripleaTasubstV0V1V2aSassignV1V2V0F">
<proof <proof
prover="coq" prover="coq"
timelimit="5" timelimit="5"
edited="imp_Imp_assign_rule_1.v" edited="imp_Imp_assign_rule_1.v"
obsolete="false"> obsolete="true">
<result status="valid" time="0.55"/> <result status="valid" time="0.55"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="seq_rule" name="seq_rule"
sum="509f2baa69407fb64a13daf344618b5a" sum="11646ebb9e6da0d832f0bf1eb67a1b76"
proved="true" proved="false"
expanded="false" expanded="false"
shape="avalid_tripleaTV0aSseqV3V4V1Iavalid_tripleaTV2V4V1Aavalid_tripleaTV0V3V2F"> shape="avalid_tripleaTV0aSseqV3V4V1Iavalid_tripleaTV2V4V1Aavalid_tripleaTV0V3V2F">
<proof <proof
prover="z3" prover="z3"
timelimit="5" timelimit="5"
edited="" edited=""
obsolete="false"> obsolete="true">
<result status="valid" time="0.17"/> <result status="valid" time="0.17"/>
</proof> </proof>
</goal> </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