Commit 3f58ce3c authored by MARCHE Claude's avatar MARCHE Claude

Completed part of the missing proofs of termination

parent dff7079b
......@@ -141,6 +141,8 @@ module Solve
invariant { !y = fib_even (!n+1) }
invariant { !y = fib (!k+3) }
invariant { !sum = fib_sum_even m !k }
invariant { 0 < !x < !y }
variant { m - !x }
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
......
This diff is collapsed.
......@@ -28,6 +28,7 @@ module FactImperative
let r = ref 1 in
while !y < x do
invariant { 0 <= !y <= x /\ !r = fact !y }
variant { x - !y }
y := !y + 1;
r := !r * !y
done;
......
......@@ -127,10 +127,10 @@
locfile="../fact.mlw"
loclnum="24" loccnumb="6" loccnume="14"
expl="VC for fact_imp"
sum="95b57589e42b60eab9fc2ba5169bbf1a"
sum="6ebaf9f4c656759c9693894b8ac005b9"
proved="true"
expanded="true"
shape="iainfix =V1afactV0ainfix =V4afactV3Aainfix &lt;=V3V0Aainfix &lt;=c0V3Iainfix =V4ainfix *V1V3FIainfix =V3ainfix +V2c1Fainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
expanded="false"
shape="iainfix =V1afactV0ainfix &lt;ainfix -V0V3ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4afactV3Aainfix &lt;=V3V0Aainfix &lt;=c0V3Iainfix =V4ainfix *V1V3FIainfix =V3ainfix +V2c1Fainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for fact_imp"/>
<proof
......@@ -145,7 +145,7 @@
<goal
name="WP_parameter test0"
locfile="../fact.mlw"
loclnum="36" loccnumb="6" loccnume="11"
loclnum="37" loccnumb="6" loccnume="11"
expl="VC for test0"
sum="c56f352251f72fcb62509c411e4ef4f5"
proved="true"
......@@ -165,7 +165,7 @@
<goal
name="WP_parameter test1"
locfile="../fact.mlw"
loclnum="37" loccnumb="6" loccnume="11"
loclnum="38" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="8e3cc4e59a682896fe45051e9ea93c4e"
proved="true"
......@@ -185,7 +185,7 @@
<goal
name="WP_parameter test7"
locfile="../fact.mlw"
loclnum="38" loccnumb="6" loccnume="11"
loclnum="39" loccnumb="6" loccnume="11"
expl="VC for test7"
sum="e3591dd2ba3bdda571e4d7ce05bb34c9"
proved="true"
......@@ -205,7 +205,7 @@
<goal
name="WP_parameter test42"
locfile="../fact.mlw"
loclnum="39" loccnumb="6" loccnume="12"
loclnum="40" loccnumb="6" loccnume="12"
expl="VC for test42"
sum="3b36ff4dc78444fb5d7765a03f5ae658"
proved="true"
......
......@@ -49,7 +49,9 @@ module FibRecGhost "recursive version, using ghost code"
use import int.Int
let rec fib_aux (ghost n: int) (a b k: int) : int
requires { k >= 0 }
requires { 0 <= n && a = fib n && b = fib (n+1) }
variant { k }
ensures { result = fib (n+k) }
= if k = 0 then a else fib_aux (n+1) b (a+b) (k-1)
......@@ -73,7 +75,9 @@ module FibRecNoGhost "recursive version, without ghost code"
use import int.Int
let rec fib_aux (a b k: int) : int
requires { k >= 0 }
requires { exists n: int. 0 <= n && a = fib n && b = fib (n+1) }
variant { k }
ensures { forall n: int. 0 <= n && a = fib n && b = fib (n+1) ->
result = fib (n+k) }
= if k = 0 then a else fib_aux b (a+b) (k-1)
......
This diff is collapsed.
......@@ -398,6 +398,7 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
forall sigma pi sigma' pi':env, n:int.
many_steps sigma pi s sigma' pi' Sskip n ->
assigns sigma result sigma' }
variant { s }
= match s with
| Sskip -> Set.empty
| Sassign i _ -> Set.singleton i
......@@ -427,6 +428,7 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
let rec wp (i:stmt) (q:fmla)
ensures { valid_triple result i q }
variant { i }
= match i with
| Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q)
......
This diff is collapsed.
......@@ -83,6 +83,7 @@ module InPlaceRev
invariant { list_seg !r !next !rM null }
invariant { disjoint !pM !rM }
invariant { (reverse !pM) ++ !rM = reverse lM }
variant { !pM }
let n = get !next !p in
next := set !next !p !r;
assert { list_seg !r !next !rM null };
......
......@@ -7,22 +7,26 @@
version="0.95.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="4"
name="Coq"
version="8.4pl2"/>
<prover
id="4"
id="5"
name="Z3"
version="2.19"/>
<prover
id="5"
id="6"
name="Z3"
version="3.2"/>
<file
......@@ -51,7 +55,7 @@
expanded="true"
shape="alist_segV2V1V5anullINamemV3V5Aainfix =V1asetV0V3V4Aalist_segV2V0V5anullF">
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="0"
edited="linked_list_rev_WP_InPlaceRev_list_seg_frame_1.v"
......@@ -69,7 +73,7 @@
expanded="true"
shape="ainfix =V1V2Ialist_segV3V0V2anullAalist_segV3V0V1anullF">
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="0"
edited="linked_list_rev_WP_InPlaceRev_list_seg_functional_1.v"
......@@ -87,7 +91,7 @@
expanded="true"
shape="alist_segV4V0aConsV4V2anullIalist_segV3V0ainfix ++V1aConsV4V2anullF">
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="0"
edited="linked_list_rev_WP_InPlaceRev_list_seg_sublistl_1.v"
......@@ -105,7 +109,7 @@
expanded="true"
shape="ano_repetV1Ialist_segV2V0V1anullF">
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="0"
edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v"
......@@ -119,16 +123,16 @@
locfile="../linked_list_rev.mlw"
loclnum="73" loccnumb="6" loccnume="22"
expl="VC for in_place_reverse"
sum="7f270f7d067f4679f0df1bade115842d"
sum="5cf3734fbf7edbb64be3f8bb3a95052a"
proved="true"
expanded="true"
shape="ialist_segV4V7areverseV1anullainfix =ainfix ++areverseV12V11areverseV1AadisjointV12V11Aalist_segV9V8V11anullAalist_segV10V8V12anullIainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FAalist_segV4V8V3anullIainfix =V8asetV7V6V4FNainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFAainfix =ainfix ++areverseV1aNilareverseV1AadisjointV1aNilAalist_seganullV2aNilanullAalist_segV0V2V1anullIalist_segV0V2V1anullFF">
expanded="false"
shape="ialist_segV4V7areverseV1anullCfaNilainfix =V13V12aConswVV5Aainfix =ainfix ++areverseV12V11areverseV1AadisjointV12V11Aalist_segV9V8V11anullAalist_segV10V8V12anullIainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FAalist_segV4V8V3anullIainfix =V8asetV7V6V4FNainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFAainfix =ainfix ++areverseV1aNilareverseV1AadisjointV1aNilAalist_seganullV2aNilanullAalist_segV0V2V1anullIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter in_place_reverse.1"
locfile="../linked_list_rev.mlw"
......@@ -136,7 +140,7 @@
expl="1. loop invariant init"
sum="a031c4edb9244bd9426fd0013e0b62c3"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant initalist_segV0V2V1anullIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -156,7 +160,7 @@
expl="2. loop invariant init"
sum="a1911d30ad06f5d2435c3e65ed2baaaf"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant initalist_seganullV2aNilanullIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -176,7 +180,7 @@
expl="3. loop invariant init"
sum="8a1458087787ef9f084d60c2ba7e0697"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant initadisjointV1aNilIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -196,7 +200,7 @@
expl="4. loop invariant init"
sum="0712d2b149a95684785c20fe4a576f94"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant initainfix =ainfix ++areverseV1aNilareverseV1Ialist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -209,7 +213,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -217,7 +221,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -225,7 +229,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -233,7 +237,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -248,7 +252,7 @@
expl="5. assertion"
sum="80958aae68cbe74204fc84ba50f169c7"
proved="true"
expanded="true"
expanded="false"
shape="assertionalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -268,7 +272,7 @@
expl="6. loop invariant preservation"
sum="cd5db00164ba7db9ab8fcfadf8782c9b"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationalist_segV10V8V12anullIainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FIalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -288,7 +292,7 @@
expl="7. loop invariant preservation"
sum="545345fdb17508638652de9fc6ced8fe"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationalist_segV9V8V11anullIainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FIalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -308,7 +312,7 @@
expl="8. loop invariant preservation"
sum="623f74c7944831af0eb2e9d42088443d"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationadisjointV12V11Iainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FIalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -321,7 +325,7 @@
<result status="valid" time="3.57"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -336,7 +340,7 @@
expl="9. loop invariant preservation"
sum="70474d9234c9b4375c5ea977a65771d3"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationainfix =ainfix ++areverseV12V11areverseV1Iainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FIalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -349,7 +353,7 @@
<result status="valid" time="0.93"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -361,10 +365,30 @@
name="WP_parameter in_place_reverse.10"
locfile="../linked_list_rev.mlw"
loclnum="73" loccnumb="6" loccnume="22"
expl="10. postcondition"
expl="10. loop variant decrease"
sum="f31ab1921be4fa8ab2b2b37bfd2bb44d"
proved="true"
expanded="false"
shape="loop variant decreaseCfaNilainfix =V13V12aConswVV5Iainfix =V12atailV5FIainfix =V11aConsaheadV5V3FIainfix =V10agetV7V6FIainfix =V9V6FIalist_segV4V8V3anullIainfix =V8asetV7V6V4FINainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="WP_parameter in_place_reverse.11"
locfile="../linked_list_rev.mlw"
loclnum="73" loccnumb="6" loccnume="22"
expl="11. postcondition"
sum="55df25c2782d2bd206d60f367d5d49ba"
proved="true"
expanded="true"
expanded="false"
shape="postconditionalist_segV4V7areverseV1anullINNainfix =V6anullIainfix =ainfix ++areverseV5V3areverseV1AadisjointV5V3Aalist_segV4V7V3anullAalist_segV6V7V5anullFIalist_segV0V2V1anullFF">
<label
name="expl:VC for in_place_reverse"/>
......@@ -377,7 +401,7 @@
<result status="valid" time="0.22"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -385,7 +409,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......
......@@ -102,6 +102,7 @@ module PrefixSumRec
requires { 0 <= left < right < a.length }
requires { -1 <= left - (right - left) }
requires { is_power_of_2 (right - left) }
variant { right - left }
ensures { phase1 left right (old a) a }
ensures { let space = right - left in
a[right] = sum (old a) (left-space+1) (right+1) /\
......@@ -137,6 +138,7 @@ module PrefixSumRec
requires { is_power_of_2 (right - left) }
requires { a[right] = sum a0 0 (left-(right-left) + 1) }
requires { phase1 left right a0 a }
variant { right - left }
ensures { partial_sum left right a0 a }
ensures { forall i: int. i <= left-(right-left) -> a[i] = (old a)[i] }
ensures { forall i: int. i > right -> a[i] = (old a)[i] }
......
......@@ -133,6 +133,7 @@ let lcp (a:array int) (x y:int) : int
let l = ref 0 in
while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
invariant { is_common_prefix a x y !l }
variant { n - !l }
incr l
done;
!l
......@@ -271,6 +272,7 @@ let sort (a:array int) (data : array int)
invariant { sorted_sub a data.elts !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le a data[k1] data[k2] }
variant { !j }
'L:
let b = !j - 1 in
let t = data[!j] in
......
......@@ -149,6 +149,7 @@ module Treedel
invariant { !p <> null /\ !mem[!p].left = !tt }
invariant { let pt = Node !subtree !pp !ppr in
istree !mem !pp pt /\ zip pt !zipper = it }
variant { !subtree }
assert { istree !mem !p !subtree };
ghost zipper := Left !zipper !pp !ppr;
ghost ppr := tree_right !subtree;
......
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