gallery: more proofs of termination

parent 0f3e08d5
......@@ -108,7 +108,7 @@ module BSTree
end
let rec bst_mem (x: elt) (t: tree)
requires { bst t } ensures { result=True <-> mem x t }
requires { bst t } ensures { result=True <-> mem x t } variant { t }
= match t with
| Empty ->
False
......@@ -124,6 +124,7 @@ module BSTree
ensures { bst result /\ not (mem x t) /\
forall y: elt. mem y result <-> y=x || mem y t }
raises { Already -> mem x t }
variant { t }
= match t with
| Empty ->
Node Empty x Empty
......
......@@ -150,11 +150,11 @@
name="WP_parameter next"
locfile="../snapshotable_trees.mlw"
loclnum="82" loccnumb="6" loccnume="10"
expl="unreachable point"
expl="VC for next"
sum="21d22249fce304653ce93159579bfcca"
proved="true"
expanded="false"
shape="unreachable pointCfaDoneainfix =aenum_elementsV0aConsV1aenum_elementsV5Iainfix =V5V4FIainfix =aenum_elementsV4ainfix ++atree_elementsV2aenum_elementsV3FaNextVVVV0INainfix =V0aDoneF">
shape="CfaDoneainfix =aenum_elementsV0aConsV1aenum_elementsV5Iainfix =V5V4FIainfix =aenum_elementsV4ainfix ++atree_elementsV2aenum_elementsV3FaNextVVVV0INainfix =V0aDoneF">
<label
name="expl:VC for next"/>
<proof
......@@ -178,10 +178,10 @@
locfile="../snapshotable_trees.mlw"
loclnum="110" loccnumb="10" loccnume="17"
expl="VC for bst_mem"
sum="f00befd8e616ab0b900beb88cb38b6d3"
sum="88d13471b1d7c7dcaf22ad8a5a237ce4"
proved="true"
expanded="false"
shape="CNamemV0V1aEmptyiiamemV0V1qainfix =V5aTrueIamemV0V4qainfix =V5aTrueFAabstV4amemV0V1ainfix =V0V3amemV0V1qainfix =V6aTrueIamemV0V2qainfix =V6aTrueFAabstV2ainfix &lt;V0V3aNodeVVVV1IabstV1F">
shape="CNamemV0V1aEmptyiiamemV0V1qainfix =V5aTrueIamemV0V4qainfix =V5aTrueFAabstV4ACfaEmptyainfix =V7V4Oainfix =V6V4aNodeVwVV1amemV0V1ainfix =V0V3amemV0V1qainfix =V8aTrueIamemV0V2qainfix =V8aTrueFAabstV2ACfaEmptyainfix =V10V2Oainfix =V9V2aNodeVwVV1ainfix &lt;V0V3aNodeVVVV1IabstV1F">
<label
name="expl:VC for bst_mem"/>
<proof
......@@ -198,10 +198,10 @@
locfile="../snapshotable_trees.mlw"
loclnum="122" loccnumb="10" loccnume="17"
expl="VC for bst_add"
sum="4b91c7972454823cf380df8c171db019"
sum="4ad1cd30b2a7ec0aef8e9b8c6818011b"
proved="true"
expanded="false"
shape="CamemV3V1Oainfix =V3V0qamemV3V2FANamemV0V1AabstV2LaNodeaEmptyV0aEmptyaEmptyiiamemV0V1IamemV0V6AamemV9V1Oainfix =V9V0qamemV9V8FANamemV0V1AabstV8LaNodeV4V5V7IamemV10V6Oainfix =V10V0qamemV10V7FANamemV0V6AabstV7FAabstV6amemV0V1IamemV0V4AamemV13V1Oainfix =V13V0qamemV13V12FANamemV0V1AabstV12LaNodeV11V5V6IamemV14V4Oainfix =V14V0qamemV14V11FANamemV0V4AabstV11FAabstV4ainfix &lt;V0V5amemV0V1ainfix =V0V5aNodeVVVV1IabstV1F">
shape="CamemV3V1Oainfix =V3V0qamemV3V2FANamemV0V1AabstV2LaNodeaEmptyV0aEmptyaEmptyiiamemV0V1IamemV0V6AamemV9V1Oainfix =V9V0qamemV9V8FANamemV0V1AabstV8LaNodeV4V5V7IamemV10V6Oainfix =V10V0qamemV10V7FANamemV0V6AabstV7FAabstV6ACfaEmptyainfix =V12V6Oainfix =V11V6aNodeVwVV1amemV0V1IamemV0V4AamemV15V1Oainfix =V15V0qamemV15V14FANamemV0V1AabstV14LaNodeV13V5V6IamemV16V4Oainfix =V16V0qamemV16V13FANamemV0V4AabstV13FAabstV4ACfaEmptyainfix =V18V4Oainfix =V17V4aNodeVwVV1ainfix &lt;V0V5amemV0V1ainfix =V0V5aNodeVVVV1IabstV1F">
<label
name="expl:VC for bst_add"/>
<proof
......@@ -210,20 +210,20 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.27"/>
</proof>
</goal>
</theory>
<theory
name="ITree"
locfile="../snapshotable_trees.mlw"
loclnum="139" loccnumb="7" loccnume="12"
loclnum="140" loccnumb="7" loccnume="12"
verified="true"
expanded="true">
<goal
name="WP_parameter create"
locfile="../snapshotable_trees.mlw"
loclnum="146" loccnumb="6" loccnume="12"
loclnum="147" loccnumb="6" loccnume="12"
expl="VC for create"
sum="2663e28679babb1ca192f0db8d819782"
proved="true"
......@@ -243,7 +243,7 @@
<goal
name="WP_parameter contains"
locfile="../snapshotable_trees.mlw"
loclnum="148" loccnumb="6" loccnume="14"
loclnum="149" loccnumb="6" loccnume="14"
expl="VC for contains"
sum="df5eea712d087c76098731af2aff38f1"
proved="true"
......@@ -263,7 +263,7 @@
<goal
name="WP_parameter add"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="VC for add"
sum="f2de3007e6a37a37ce8f6c26507f5d83"
proved="true"
......@@ -278,7 +278,7 @@
<goal
name="WP_parameter add.1"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="1. precondition"
sum="241e2e582d364749402be0d3a10a4388"
proved="true"
......@@ -298,7 +298,7 @@
<goal
name="WP_parameter add.2"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="2. type invariant"
sum="45711f4768c2d9a329cbc424e30c09ad"
proved="true"
......@@ -318,7 +318,7 @@
<goal
name="WP_parameter add.3"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="3. postcondition"
sum="e7f4df6ded9650d319ec627d54d0a230"
proved="true"
......@@ -333,7 +333,7 @@
<goal
name="WP_parameter add.3.1"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="1."
sum="a4e53ced958d6eaaf95a3770fbbd99b5"
proved="true"
......@@ -353,7 +353,7 @@
<goal
name="WP_parameter add.3.2"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="2."
sum="4cc93716e993c19154efb3be657c170a"
proved="true"
......@@ -373,7 +373,7 @@
<goal
name="WP_parameter add.3.3"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="3."
sum="da77206c6482d3d5fdc42e53cb80e4f1"
proved="true"
......@@ -395,7 +395,7 @@
<goal
name="WP_parameter add.4"
locfile="../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="153" loccnumb="6" loccnume="9"
expl="4. postcondition"
sum="d8709993769bf330fcf5e82836de1f85"
proved="true"
......@@ -417,7 +417,7 @@
<goal
name="WP_parameter snapshot"
locfile="../snapshotable_trees.mlw"
loclnum="157" loccnumb="6" loccnume="14"
loclnum="158" loccnumb="6" loccnume="14"
expl="VC for snapshot"
sum="60ed8092aff68967041f94a4e6a912e8"
proved="true"
......@@ -437,7 +437,7 @@
<goal
name="WP_parameter iterator"
locfile="../snapshotable_trees.mlw"
loclnum="159" loccnumb="6" loccnume="14"
loclnum="160" loccnumb="6" loccnume="14"
expl="VC for iterator"
sum="4f79dff251136cb021570a9df6080001"
proved="true"
......@@ -458,13 +458,13 @@
<theory
name="Harness"
locfile="../snapshotable_trees.mlw"
loclnum="165" loccnumb="7" loccnume="14"
loclnum="166" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
<goal
name="WP_parameter test"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="VC for test"
sum="f406234226bd2451bb236c7a206e0d9c"
proved="true"
......@@ -479,7 +479,7 @@
<goal
name="WP_parameter test.1"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="1. assertion"
sum="682dc84d7f7d4baa7af6fe285e6b2e63"
proved="true"
......@@ -499,7 +499,7 @@
<goal
name="WP_parameter test.2"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="2. loop invariant init"
sum="e569eda897a31ec565678da2db26ab85"
proved="true"
......@@ -519,7 +519,7 @@
<goal
name="WP_parameter test.3"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="3. precondition"
sum="bdfe121804f3249854cd00aaf4a7bd71"
proved="true"
......@@ -539,7 +539,7 @@
<goal
name="WP_parameter test.4"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="4. type invariant"
sum="d071539ff651ded36ac4c31bd0088bf1"
proved="true"
......@@ -559,7 +559,7 @@
<goal
name="WP_parameter test.5"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="5. loop invariant preservation"
sum="471c92c06b504a433a15797fd440bb13"
proved="true"
......@@ -579,7 +579,7 @@
<goal
name="WP_parameter test.6"
locfile="../snapshotable_trees.mlw"
loclnum="169" loccnumb="6" loccnume="10"
loclnum="170" loccnumb="6" loccnume="10"
expl="6. loop variant decrease"
sum="3ade566bec30f2d724c87ed284f65341"
proved="true"
......
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