gallery: more proofs of termination

parent 397e8c4d
......@@ -21,18 +21,20 @@ module M
val table : ref table
val add (x:int) (y:int) : unit writes { table }
val add (x:int) (y:int) : unit
writes { table }
ensures { !table = (old !table)[x <- Some y] }
exception Not_found
val find (x:int) : int
ensures { !table[x] = Some result }
raises { Not_found -> !table[x] = None }
raises { Not_found -> !table[x] = None }
let rec fibo n =
requires { 0 <= n /\ inv !table }
ensures { result = fib n /\ inv !table }
ensures { result = fib n /\ inv !table }
variant { 2*n }
if n <= 1 then
1
else
......@@ -40,7 +42,8 @@ module M
with memo_fibo n =
requires { 0 <= n /\ inv !table }
ensures { result = fib n /\ inv !table }
ensures { result = fib n /\ inv !table }
variant { 2*n+1 }
try find n
with Not_found -> let fn = fibo n in add n fn; fn end
......
......@@ -12,7 +12,7 @@
<file
name="../fib_memo.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="M"
locfile="../fib_memo.mlw"
......@@ -22,12 +22,12 @@
<goal
name="WP_parameter fibo"
locfile="../fib_memo.mlw"
loclnum="33" loccnumb="10" loccnume="14"
loclnum="34" loccnumb="10" loccnume="14"
expl="VC for fibo"
sum="2a649c2d30bb53dfaa7076541a6ec154"
sum="1c92730ae7a166108cdfa6c2c6409c1e"
proved="true"
expanded="true"
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Lainfix -V0c2ainvV1Aainfix =c1afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Aainfix &lt;ainfix +ainfix *c2V4c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Aainfix &lt;ainfix +ainfix *c2V2c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c2ainvV1Aainfix =c1afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for fibo"/>
<proof
......@@ -42,12 +42,12 @@
<goal
name="WP_parameter memo_fibo"
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
loclnum="43" loccnumb="7" loccnume="16"
expl="VC for memo_fibo"
sum="b54a77c76fca0c6de8f8d3bc49bc4476"
sum="b018158e5afc0812ef7e860f41f89dff"
proved="true"
expanded="true"
shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FAainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix &lt;=c0V0FF">
shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FAainvV1Aainfix &lt;=c0V0Aainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for memo_fibo"/>
<transf
......@@ -57,7 +57,7 @@
<goal
name="WP_parameter memo_fibo.1"
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
loclnum="43" loccnumb="7" loccnume="16"
expl="1. postcondition"
sum="316195b57b9a183f6b6c75aacee91777"
proved="true"
......@@ -77,8 +77,28 @@
<goal
name="WP_parameter memo_fibo.2"
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="2. precondition"
loclnum="43" loccnumb="7" loccnume="16"
expl="2. variant decrease"
sum="9d90acbce96fa42b719eaf6aca980e50"
proved="true"
expanded="false"
shape="variant decreaseainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for memo_fibo"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter memo_fibo.3"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
expl="3. precondition"
sum="b9069385630ec027acb3fe9c6f6c7a4d"
proved="true"
expanded="true"
......@@ -95,10 +115,10 @@
</proof>
</goal>
<goal
name="WP_parameter memo_fibo.3"
name="WP_parameter memo_fibo.4"
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="3. postcondition"
loclnum="43" loccnumb="7" loccnume="16"
expl="4. postcondition"
sum="15172e65467ccc671126b6844ce65ef5"
proved="true"
expanded="true"
......
......@@ -78,6 +78,7 @@ module HashtblImpl
ensures { forall k: key, v: 'a.
if 0 <= bucket k osize <= i then good_data k v h.view ndata
else not in_data k v ndata }
variant { l }
= match l with
| Nil -> ()
| Cons (k, v) r ->
......
This diff is collapsed.
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