Commit 20204945 authored by MARCHE Claude's avatar MARCHE Claude

List, Option, BinTree : test for emptiness in programs

parent 71f138c5
......@@ -50,12 +50,9 @@ module BraunHeaps
requires { heap t && 0 < size t }
ensures { is_minimum (minimum t) t }
variant { t }
= match t with
| Empty -> absurd
| Node l _ r ->
if not is_empty l then root_is_min l;
if not is_empty r then root_is_min r
end
= let Node l _ r = t in
if not is_empty l then root_is_min l;
if not is_empty r then root_is_min r
predicate inv (t: tree elt) = match t with
| Empty -> true
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="4000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="1" memlimit="4000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="20f7ebde985c3ab8d295dc1512266772" expanded="true">
<theory name="BraunHeaps" sum="9334f80cdd6602327443c5aae6cefa84" expanded="true">
<goal name="VC le_root" expl="VC for le_root">
<proof prover="1" memlimit="1000"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="VC root_is_min" expl="VC for root_is_min">
<goal name="VC root_is_min" expl="VC for root_is_min" expanded="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty">
......
......@@ -13,10 +13,6 @@ module M
[0 <= y2 <= x2]. The seven other cases can be easily
deduced by symmetry. *)
constant x2: int
constant y2: int
axiom first_octant: 0 <= y2 <= x2
(* [best x y] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line
i.e. for all y', we have |y - x*y2/x2| <= |y' - x*y2/x2|
......@@ -24,7 +20,7 @@ module M
use import int.Abs
predicate best (x y: int) =
predicate best (x2 y2 x y: int) =
forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
(** Key lemma for Bresenham's proof: if [b] is at distance less or equal
......@@ -36,15 +32,16 @@ module M
abs (2 * a * b - 2 * c) <= a ->
forall b': int. abs (a * b - c) <= abs (a * b' - c)
let bresenham () =
let y = ref 0 in
let bresenham (x2 y2:int)
requires { 0 <= y2 <= x2 }
= let y = ref 0 in
let e = ref (2 * y2 - x2) in
for x = 0 to x2 do
invariant { !e = 2 * (x + 1) * y2 - (2 * !y + 1) * x2 }
invariant { 2 * (y2 - x2) <= !e <= 2 * y2 }
(* here we would plot (x, y),
so we assert this is the best possible row y for column x *)
assert { best x !y };
assert { best x2 y2 x !y };
if !e < 0 then
e := !e + 2 * y2
else begin
......
......@@ -2,44 +2,36 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="1" memlimit="1000"/>
<prover id="1" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="1" memlimit="1000"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="3d5e82bb9f3ea61d2077393703418500" expanded="true">
<theory name="M" sum="8d5a023211d939cd805712e7fb230d8c" expanded="true">
<goal name="closest" expanded="true">
<proof prover="2" edited="bresenham_M_closest_1.v"><result status="valid" time="1.19"/></proof>
<proof prover="1" edited="bresenham_M_closest_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<goal name="VC bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bresenham.1" expl="1. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<goal name="VC bresenham.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter bresenham.2" expl="2. loop invariant init" expanded="true">
<proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
<goal name="VC bresenham.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="3. assertion" expanded="true">
<proof prover="4"><result status="valid" time="1.67" steps="132"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="1.18" steps="129"/></proof>
<goal name="VC bresenham.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.13" steps="42"/></proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<goal name="VC bresenham.4" expl="4. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter bresenham.5" expl="5. loop invariant preservation" expanded="true">
<proof prover="5"><result status="valid" time="0.02" steps="11"/></proof>
<goal name="VC bresenham.5" expl="5. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter bresenham.6" expl="6. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
<goal name="VC bresenham.6" expl="6. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter bresenham.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="5"><result status="valid" time="0.02" steps="12"/></proof>
<goal name="VC bresenham.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>
</goal>
......
......@@ -13,20 +13,20 @@ module BubbleSort
let bubble_sort (a: array int)
ensures { permut_all (old a) a }
ensures { permut_all (old a) a }
ensures { sorted a }
= 'Init:
= label Init in
for i = length a - 1 downto 1 do
invariant { permut_all (at a 'Init) a }
invariant { permut_all (a at Init) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
for j = 0 to i - 1 do
invariant { permut_all (at a 'Init) a }
invariant { permut_all (a at Init) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
if a[j] > a[j+1] then swap a j (j+1);
......@@ -35,7 +35,7 @@ module BubbleSort
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
a[0] <- 7; a[1] <- 3; a[2] <- 1;
bubble_sort a;
a
......
This diff is collapsed.
......@@ -20,10 +20,10 @@ module CoincidenceCount
use import set.FsetComprehension
function setof (a: array 'a) : set 'a =
map (get a) (interval 0 (length a))
map (fun x -> a[x]) (interval 0 (length a))
function drop (a: array 'a) (n: int) : set 'a =
map (get a) (interval n (length a))
map (fun x -> a[x]) (interval n (length a))
lemma drop_left:
forall a: array 'a, n: int. 0 <= n < length a ->
......
......@@ -2,94 +2,104 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<file name="../coincidence_count.mlw" expanded="true">
<theory name="CoincidenceCount" sum="a8232d091a24913e7b296b0a1514ac32" expanded="true">
<goal name="drop_left">
<proof prover="2"><result status="valid" time="0.15" steps="486"/></proof>
<theory name="CoincidenceCount" sum="0132b9a7880f94ef4837b56d77339196" expanded="true">
<goal name="drop_left" expanded="true">
<proof prover="3"><result status="valid" time="0.21" steps="779"/></proof>
</goal>
<goal name="not_mem_inter_r">
<proof prover="1"><result status="valid" time="1.02" steps="585"/></proof>
<goal name="not_mem_inter_r" expanded="true">
<proof prover="3"><result status="valid" time="0.16" steps="396"/></proof>
</goal>
<goal name="not_mem_inter_l">
<proof prover="1"><result status="valid" time="1.01" steps="585"/></proof>
<goal name="not_mem_inter_l" expanded="true">
<proof prover="3"><result status="valid" time="0.17" steps="396"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count" expanded="true">
<goal name="VC coincidence_count" expl="VC for coincidence_count" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter coincidence_count.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.19" steps="375"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.29" steps="376"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.15" expl="15. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="2.23"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.17" expl="17. assertion">
<transf name="inline_goal">
<goal name="WP_parameter coincidence_count.17.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.69" steps="302"/></proof>
<goal name="VC coincidence_count.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC coincidence_count.2" expl="2. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC coincidence_count.3" expl="3. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC coincidence_count.4" expl="4. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC coincidence_count.5" expl="5. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC coincidence_count.6" expl="6. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC coincidence_count.7" expl="7. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC coincidence_count.8" expl="8. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.14" steps="343"/></proof>
</goal>
<goal name="VC coincidence_count.9" expl="9. loop variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC coincidence_count.10" expl="10. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC coincidence_count.11" expl="11. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC coincidence_count.12" expl="12. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC coincidence_count.13" expl="13. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC coincidence_count.14" expl="14. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.12" steps="344"/></proof>
</goal>
<goal name="VC coincidence_count.15" expl="15. loop variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC coincidence_count.16" expl="16. assertion">
<transf name="introduce_premises">
<goal name="VC coincidence_count.16.1" expl="1. assertion">
<transf name="inline_goal">
<goal name="VC coincidence_count.16.1.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="VC coincidence_count.16.1.1.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="0.74" steps="1167"/></proof>
</goal>
<goal name="VC coincidence_count.16.1.1.2" expl="2. assertion">
<transf name="introduce_premises">
<goal name="VC coincidence_count.16.1.1.2.1" expl="1. assertion">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="1.18" steps="2995"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter coincidence_count.18" expl="18. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
<goal name="VC coincidence_count.17" expl="17. assertion">
<proof prover="3"><result status="valid" time="0.61" steps="815"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
<goal name="VC coincidence_count.18" expl="18. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.20" expl="20. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.70" steps="167"/></proof>
<goal name="VC coincidence_count.19" expl="19. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.21" expl="21. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
<goal name="VC coincidence_count.20" expl="20. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.06" steps="121"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.08" steps="109"/></proof>
<goal name="VC coincidence_count.21" expl="21. loop variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.23" expl="23. postcondition">
<proof prover="1"><result status="valid" time="0.08" steps="108"/></proof>
<goal name="VC coincidence_count.22" expl="22. postcondition">
<proof prover="3"><result status="valid" time="0.04" steps="111"/></proof>
</goal>
</transf>
</goal>
......
......@@ -74,7 +74,7 @@ module Conjugate
invariant { 0 <= !partc < a.length }
invariant { forall j: int. a[!partc] <= j < b.length -> numofgt a b[j] j }
variant { a.length - !partc }
'L:
label L in
let ghost start = !partc in
let edge = a[!partc] in
incr partc;
......@@ -85,7 +85,7 @@ module Conjugate
incr partc
done;
for i = a[!partc] to edge - 1 do
invariant { forall j: int. edge <= j < b.length -> b[j] = (at b 'L)[j] }
invariant { forall j: int. edge <= j < b.length -> b[j] = (b at L)[j] }
invariant { forall j: int. a[!partc] <= j < i -> b[j] = !partc }
b[i] <- !partc
done
......
......@@ -2,101 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<file name="../conjugate.mlw" expanded="true">
<theory name="Conjugate" sum="d5ae5eea60f1c7dfc09f6ff24ea83b48" expanded="true">
<goal name="WP_parameter conjugate" expl="VC for conjugate" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter conjugate.1" expl="1. index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter conjugate.2" expl="2. array creation size">
<proof prover="2"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter conjugate.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter conjugate.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter conjugate.5" expl="5. index in array bounds">
<proof prover="2"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter conjugate.6" expl="6. index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.7" expl="7. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter conjugate.8" expl="8. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter conjugate.9" expl="9. index in array bounds">
<proof prover="2"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter conjugate.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter conjugate.11" expl="11. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter conjugate.12" expl="12. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.13" expl="13. index in array bounds">
<proof prover="2"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="WP_parameter conjugate.14" expl="14. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.15" expl="15. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter conjugate.16" expl="16. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.17" expl="17. loop invariant init">
<proof prover="2" timelimit="10"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter conjugate.18" expl="18. type invariant">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter conjugate.19" expl="19. index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="WP_parameter conjugate.20" expl="20. loop invariant preservation">
<proof prover="2" timelimit="10"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter conjugate.21" expl="21. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter conjugate.22" expl="22. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.23" expl="23. loop invariant preservation">
<proof prover="2" timelimit="10"><result status="valid" time="0.59" steps="150"/></proof>
</goal>
<goal name="WP_parameter conjugate.24" expl="24. loop variant decrease">
<proof prover="2"><result status="valid" time="0.06" steps="16"/></proof>
</goal>
<goal name="WP_parameter conjugate.25" expl="25. assertion">
<proof prover="2"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.26" expl="26. type invariant">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter conjugate.27" expl="27. postcondition">
<proof prover="2" timelimit="10"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
</transf>
<theory name="Conjugate" sum="d1d92de63fd7de6a5ce3684b4d2f5f68" expanded="true">
<goal name="VC conjugate" expl="VC for conjugate" expanded="true">
<proof prover="0"><result status="valid" time="0.34" steps="453"/></proof>
</goal>
</theory>
<theory name="Test" sum="b22149320dd0c24e561e0d5940d4fa12" expanded="true">
<goal name="WP_parameter test" expl="VC for test" expanded="true">
<proof prover="2"><result status="valid" time="0.09" steps="36"/></proof>
<theory name="Test" sum="671d1a98aec098c0499c7105eb5626d7" expanded="true">
<goal name="VC test" expl="VC for test" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="WP_parameter bench" expl="VC for bench" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
<goal name="VC bench" expl="VC for bench" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</theory>
</file>
......
......@@ -23,8 +23,8 @@ module Spec
use export array.IntArraySorted
(* values of the array are in the range 0..k-1 *)
constant k: int
axiom k_positive: 0 < k
val constant k: int
ensures { 0 < result }
predicate k_values (a: array int) =
forall i: int. 0 <= i < length a -> 0 <= a[i] < k
......@@ -33,10 +33,10 @@ module Spec
- [numeq a v l u] is the number of values in a[l..u[ equal to v
- [numlt a v l u] is the number of values in a[l..u[ less than v *)
function numeq (a: array int) (v i j : int) : int =
N.numof (\ k. a[k] = v) i j
N.numof (fun k -> a[k] = v) i j
function numlt (a: array int) (v i j : int) : int =
N.numof (\ k. a[k] < v) i j
N.numof (fun k -> a[k] < v) i j
(* an ovious lemma relates numeq and numlt *)
let rec lemma eqlt (a: array int) (v: int) (l u: int)
......@@ -64,7 +64,7 @@ module CountingSort
let counting_sort (a: array int) (b: array int)
requires { k_values a /\ length a = length b }
ensures { sorted b /\ permut a b }
= let c = make k 0 in
= let c = Array.make k 0 in
for i = 0 to length a - 1 do
invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
let v = a[i] in
......@@ -101,8 +101,7 @@ module InPlaceCountingSort
let in_place_counting_sort (a: array int)
requires { k_values a }
ensures { sorted a /\ permut (old a) a }
= 'L:
let c = make k 0 in
= let c = make k 0 in
for i = 0 to length a - 1 do
invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
let v = a[i] in
......@@ -110,17 +109,17 @@ module InPlaceCountingSort
done;
let j = ref 0 in
for v = 0 to k-1 do
invariant { !j = numlt (at a 'L) v 0 (length a) }
invariant { !j = numlt (old a) v 0 (length a) }
invariant { sorted_sub a 0 !j }
invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] < v }
invariant { forall f: int.
0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) }
0 <= f < v -> numeq a f 0 !j = numeq (old a) f 0 (length a) }
for i = 1 to c[v] do
invariant { !j -i+1 = numlt (at a 'L) v 0 (length a) }
invariant { !j -i+1 = numlt (old a) v 0 (length a) }
invariant { sorted_sub a 0 !j }
invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] <= v }
invariant { forall f: int.
0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) }
0 <= f < v -> numeq a f 0 !j = numeq (old a) f 0 (length a) }
invariant { numeq a v 0 !j = i-1 }
a[!j] <- v;
incr j;
......
This diff is collapsed.
......@@ -60,14 +60,13 @@ module TestCursor
let sum (t: t) (c: cursor) : int
requires { coherent t c }
requires { c.i = 0 }
ensures { result = sum 0 (length c.seq) (get c.seq) }
ensures { result = sum (get c.seq) 0 (length c.seq) }
=
let s = ref 0 in
'I:
while has_next t c do
invariant { coherent t c }
invariant { 0 <= c.i <= length c.seq }
invariant { !s = sum 0 c.i (get c.seq) }
invariant { !s = sum (get c.seq) 0 c.i }
variant { length c.seq - c.i }
let x = next t c in
s += x
......@@ -107,7 +106,7 @@ module IntListCursor (* : IterableList *)
requires { coherent t c }
ensures { result <-> c.to_do <> Nil }
=
c.to_do <> Nil
not is_nil c.to_do
let next (t: t) (c: cursor) : elt
requires { c.to_do <> Nil }
......
This diff is collapsed.
......@@ -5,8 +5,9 @@ theory Tree
type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)
let function is_empty (t:tree 'a) : bool =
match t with Empty -> true | Node _ _ _ -> false end
let predicate is_empty (t:tree 'a)
ensures { result <-> t = Empty }
= match t with Empty -> true | Node _ _ _ -> false end
end
......@@ -51,10 +52,8 @@ theory Height "height of a tree"
use import int.MinMax
let rec function height (t: tree 'a) : int = match t with
| Empty ->
0
| Node l _ r ->
1 + max (height l) (height r)
| Empty -> 0
| Node l _ r -> 1 + max (height l) (height r)
end
lemma height_nonneg:
......@@ -68,7 +67,7 @@ theory Inorder "inorder traversal"
use import list.List
use import list.Append
function inorder (t: tree 'a) : list 'a = match t with
let rec function inorder (t: tree 'a) : list 'a = match t with
| Empty -> Nil
| Node l x r -> inorder l ++ Cons x (inorder r)
end
......@@ -81,7 +80,7 @@ theory Preorder "preorder traversal"
use import list.List
use import list.Append
function preorder (t: tree 'a) : list 'a = match t with
let rec function preorder (t: tree 'a) : list 'a = match t with
| Empty -> Nil
| Node l x r -> Cons x (preorder l ++ preorder r)
end
......@@ -109,31 +108,32 @@ theory Zipper "Huet's zipper"
| Left (zipper 'a) 'a (tree 'a)
| Right (tree 'a) 'a (zipper 'a)
function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a =
match z with
| Top -> t
| Left z x r -> zip (Node t x r) z
| Right l x z -> zip (Node l x t) z
end
end
(* navigating in a tree using a zipper *)
type pointed 'a = (tree 'a, zipper 'a)
function start (t: tree 'a) : pointed 'a = (t, Top)
let function start (t: tree 'a) : pointed 'a = (t, Top)
function up (p: pointed 'a) : pointed 'a = match p with
let function up (p: pointed 'a) : pointed 'a = match p with
| _, Top -> p (* do nothing *)
| l, Left z x r | r, Right l x z -> (Node l x r, z)
end
function top (p: pointed 'a) : tree 'a = let t, z = p in zip t z
let function top (p: pointed 'a) : tree 'a = let t, z = p in zip t z
function down_left (p: pointed 'a) : pointed 'a = match p with
let function down_left (p: pointed 'a) : pointed 'a = match p with
| Empty, _ -> p (* do nothing *)
| Node l x r, z -> (l, Left z x r)
end
function down_right (p: pointed 'a) : pointed 'a = match p with
let function down_right (p: pointed 'a) : pointed 'a = match p with
| Empty, _ -> p (* do nothing *)
| Node l x r, z -> (r, Right l x z)
end
......
......@@ -7,6 +7,11 @@ theory List
type list 'a = Nil | Cons 'a (list 'a)
let predicate is_nil (l:list 'a)
ensures { result <-> l = Nil }
=
match l with Nil -> true | Cons _ _ -> false end
end
(** {2 Length of a list} *)
......
......@@ -4,4 +4,9 @@ theory Option
type option 'a = None | Some 'a
let predicate is_none (o: option 'a)
ensures { result <-> o = None }
=
match o with None -> true | Some _ -> false end
end