example: gcd with machine integers (note and proof)

parent 8804860a
......@@ -87,6 +87,9 @@ module BinaryGcd
end
(** With machine integers.
Note that we assume parameters u, v to be nonnegative.
Otherwise, for u = v = min_int, the gcd could not be represented. *)
module EuclideanAlgorithm31
......
......@@ -9,8 +9,9 @@
<prover id="4" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="4000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="7a432e31947f2a4bd6100c41353b8564" expanded="true">
<theory name="EuclideanAlgorithm" sum="7a432e31947f2a4bd6100c41353b8564">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. postcondition">
......@@ -36,7 +37,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative" sum="69a546e6ee7e5d52c2e5b10840140418" expanded="true">
<theory name="EuclideanAlgorithmIterative" sum="69a546e6ee7e5d52c2e5b10840140418">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. loop invariant init">
......@@ -61,7 +62,7 @@
</transf>
</goal>
</theory>
<theory name="BinaryGcd" sum="630c5b7df6b8be87bd48b3d822288805" expanded="true">
<theory name="BinaryGcd" sum="630c5b7df6b8be87bd48b3d822288805">
<goal name="even1">
<proof prover="5" memlimit="1000"><result status="valid" time="0.06" steps="18"/></proof>
</goal>
......@@ -171,29 +172,29 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31" sum="91fea75d1ece6ac0571a9d40b9bdc3dc" expanded="true">
<theory name="EuclideanAlgorithm31" sum="1571c2dfa83134d03ae4f2b3fae0cf1a">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="7"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. division by zero">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="47"/></proof>
<proof prover="7"><result status="valid" time="0.07" steps="50"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease">
<proof prover="5" timelimit="5"><result status="valid" time="0.49" steps="114"/></proof>
<proof prover="7"><result status="valid" time="0.67" steps="166"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. precondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="21"/></proof>
<proof prover="7"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="42"/></proof>
<proof prover="7"><result status="valid" time="0.11" steps="41"/></proof>
</goal>
</transf>
</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