stdlib:seq: _sub-based lemmas completed

parent 4a93b594
......@@ -7,7 +7,7 @@
<path name=".."/><path name="all_distinct.mlw"/>
<theory name="AllDistinct" proved="true">
<goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="263"/></proof>
<proof prover="1"><result status="valid" time="0.21" steps="269"/></proof>
</goal>
</theory>
</file>
......
......@@ -7,7 +7,7 @@ module Sum
use int.Int
use ref.Ref
use array.Array
use array.ArraySum
use seq.Sum
let sum (a: array int) (n: int)
requires { 0 <= n < a.length }
......
......@@ -7,15 +7,15 @@
<path name=".."/><path name="balance.mlw"/>
<theory name="Puzzle8" proved="true">
<goal name="VC solve3" expl="VC for solve3" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="52"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="57"/></proof>
</goal>
<goal name="VC solve8" expl="VC for solve8" proved="true">
<proof prover="1"><result status="valid" time="0.13" steps="267"/></proof>
<proof prover="1"><result status="valid" time="0.13" steps="294"/></proof>
</goal>
</theory>
<theory name="Puzzle12" proved="true">
<goal name="VC solve12" expl="VC for solve12" proved="true">
<proof prover="1"><result status="valid" time="0.53" steps="1204"/></proof>
<proof prover="1"><result status="valid" time="0.34" steps="1165"/></proof>
</goal>
</theory>
</file>
......
......@@ -7,17 +7,17 @@
<path name=".."/><path name="binary_search.mlw"/>
<theory name="BinarySearch" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="128"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="63"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
</theory>
<theory name="BinarySearchBranchless" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="218"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="194"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true">
......@@ -27,7 +27,7 @@
</theory>
<theory name="BinarySearchBoolean" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="245"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="215"/></proof>
</goal>
</theory>
</file>
......
......@@ -19,11 +19,11 @@ module Spec
(* s is no smaller than sums of subarrays a[l..h[ with 0 <= l < maxlo *)
predicate maxsublo (a: array int) (maxlo: int) (s: int) =
forall l h: int. 0 <= l < maxlo -> l <= h <= length a -> sum a[l..h] <= s
forall l h: int. 0 <= l < maxlo -> l <= h <= length a -> sum a l h <= s
(* s is no smaller than sums of subarrays of a *)
predicate maxsub (a: array int) (s: int) =
forall l h: int. 0 <= l <= h <= length a -> sum a[l..h] <= s
forall l h: int. 0 <= l <= h <= length a -> sum a l h <= s
end
......@@ -38,24 +38,25 @@ module Algo1
use Spec
let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a[!lo .. !hi] }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref 0 in
for l = 0 to n-1 do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a[!lo .. !hi] }
invariant { 0 <= !lo <= l && !lo <= !hi <= n }
invariant { 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
for h = l to n do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a[!lo .. !hi] }
invariant { 0 <= !lo <= l && !lo <= !hi <= n }
invariant { 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
invariant { forall h': int. l <= h' < h -> sum a[l..h'] <= !ms }
invariant { forall h'. l <= h' < h -> sum a l h' <= !ms }
(* compute the sum of a[l..h[ *)
let s = ref 0 in
for i = l to h-1 do
invariant { !s = sum a[l..i] }
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a[!lo .. !hi] }
invariant { !s = sum a l i }
s += a[i]
done;
if !s > !ms then begin ms := !s; lo := l; hi := h end
......@@ -75,22 +76,23 @@ module Algo2
use Spec
let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a[!lo .. !hi] }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref 0 in
for l = 0 to n-1 do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && 0 <= !ms = sum a[!lo .. !hi] }
invariant { 0 <= !lo <= l && !lo <= !hi <= n }
invariant { 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
let s = ref 0 in
for h = l+1 to n do
invariant
{ 0 <= !lo <= l && !lo <= !hi <= n && 0 <= !ms = sum a[!lo .. !hi] }
invariant { 0 <= !lo <= l && !lo <= !hi <= n }
invariant { 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
invariant { forall h': int. l <= h' < h -> sum a[l..h'] <= !ms }
invariant { !s = sum a[l .. h-1] }
invariant { forall h'. l <= h' < h -> sum a l h' <= !ms }
invariant { !s = sum a l (h-1) }
s += a[h-1]; (* update the sum *)
if !s > !ms then begin ms := !s; lo := l; hi := h end
done
......@@ -111,8 +113,8 @@ module Algo3
let rec maximum_subarray_rec (a: array int) (l h: int) (ghost lo hi: ref int)
: int
requires { 0 <= l <= h <= length a }
ensures { l <= !lo <= !hi <= h && result = sum a[!lo .. !hi] }
ensures { forall l' h': int. l <= l' <= h' <= h -> sum a[l'..h'] <= result }
ensures { l <= !lo <= !hi <= h && result = sum a !lo !hi }
ensures { forall l' h'. l <= l' <= h' <= h -> sum a l' h' <= result }
variant { h - l }
= if h = l then begin
(* base case: no element at all *)
......@@ -125,18 +127,18 @@ module Algo3
let ms = ref 0 in
let s = ref !ms in
for i = mid-1 downto l do
invariant { l <= !lo <= mid = !hi && !ms = sum a[!lo .. !hi] }
invariant { forall l': int. i < l' <= mid -> sum a[l'..mid] <= !ms }
invariant { !s = sum a[i+1 .. mid] }
invariant { l <= !lo <= mid = !hi && !ms = sum a !lo !hi }
invariant { forall l': int. i < l' <= mid -> sum a l' mid <= !ms }
invariant { !s = sum a (i+1) mid }
s += a[i];
if !s > !ms then begin ms := !s; lo := i end
done;
s := !ms;
for i = mid to h-1 do
invariant { mid <= !hi <= h && !ms = sum a[!lo .. !hi] }
invariant { forall l' h': int. l <= l' <= mid <= h' <= i ->
sum a[l'..h'] = sum a[l'..mid] + sum a[mid..h'] <= !ms }
invariant { !s = sum a[!lo..i] = sum a[!lo..mid] + sum a[mid..i] }
invariant { mid <= !hi <= h && !ms = sum a !lo !hi }
invariant { forall l' h'. l <= l' <= mid <= h' <= i ->
sum a l' h' = sum a l' mid + sum a mid h' <= !ms }
invariant { !s = sum a !lo i = sum a !lo mid + sum a mid i }
s += a[i];
if !s > !ms then begin ms := !s; hi := (i+1) end
done;
......@@ -157,7 +159,7 @@ module Algo3
end
let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a[!lo .. !hi] }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= maximum_subarray_rec a 0 (length a) lo hi
......@@ -173,7 +175,7 @@ module Algo4
use Spec
let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a[!lo .. !hi] }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
......@@ -182,10 +184,11 @@ module Algo4
let ghost l = ref 0 in
let s = ref 0 in
for i = 0 to n-1 do
invariant { 0 <= !lo <= !hi <= i && 0 <= !ms = sum a[!lo .. !hi] }
invariant { forall l' h': int. 0 <= l' <= h' <= i -> sum a[l'..h'] <= !ms }
invariant { 0 <= !l <= i && !s = sum a[!l..i] }
invariant { forall l': int. 0 <= l' < i -> sum a[l'..i] <= !s }
invariant { 0 <= !lo <= !hi <= i }
invariant { 0 <= !ms = sum a !lo !hi }
invariant { forall l' h'. 0 <= l' <= h' <= i -> sum a l' h' <= !ms }
invariant { 0 <= !l <= i && !s = sum a !l i }
invariant { forall l'. 0 <= l' < i -> sum a l' i <= !s }
if !s < 0 then begin s := a[i]; l := i end else s += a[i];
if !s > !ms then begin ms := !s; lo := !l; hi := (i+1) end
done;
......@@ -209,8 +212,8 @@ module Algo5
*)
let maximum_subarray (a: array int): int
ensures { forall l h: int. 0 <= l <= h <= length a -> sum a[l..h] <= result }
ensures { exists l h: int. 0 <= l <= h <= length a /\ sum a[l..h] = result }
ensures { forall l h. 0 <= l <= h <= length a -> sum a l h <= result }
ensures { exists l h. 0 <= l <= h <= length a /\ sum a l h = result }
=
let maxsum = ref 0 in
let curmax = ref 0 in
......@@ -218,10 +221,10 @@ module Algo5
let ghost hi = ref 0 in
let ghost cl = ref 0 in
for i = 0 to a.length - 1 do
invariant { forall l : int. 0 <= l <= i -> sum a[l..i] <= !curmax }
invariant { 0 <= !cl <= i /\ sum a[!cl..i] = !curmax }
invariant { forall l h: int. 0 <= l <= h <= i -> sum a[l..h] <= !maxsum }
invariant { 0 <= !lo <= !hi <= i /\ sum a[!lo .. !hi] = !maxsum }
invariant { forall l. 0 <= l <= i -> sum a l i <= !curmax }
invariant { 0 <= !cl <= i /\ sum a !cl i = !curmax >= 0 }
invariant { forall l h. 0 <= l <= h <= i -> sum a l h <= !maxsum }
invariant { 0 <= !lo <= !hi <= i /\ sum a !lo !hi = !maxsum >= 0 }
curmax += a[i];
if !curmax < 0 then begin curmax := 0; cl := i+1 end;
if !curmax > !maxsum then begin maxsum := !curmax; lo := !cl; hi := i+1 end
......@@ -236,7 +239,7 @@ end
than max_int. There is no need to require the sums to be no
smaller than min_int, since whenever the sum becomes negative it is
replaced by the next element. *)
(*
module BoundedIntegers
use int.Int
......@@ -250,10 +253,10 @@ module BoundedIntegers
Sum.sum (fun i -> (a[i] : int)) lo hi
let maximum_subarray (a: array int63) (ghost lo hi: ref int): int63
requires { [@no overflow] forall l h. 0 <= l <= h <= length a ->
sum a[l..h] <= max_int }
ensures { 0 <= !lo <= !hi <= length a && result = sum a[!lo..!hi] }
ensures { forall l h. 0 <= l <= h <= length a -> result >= sum a[!lo..!hi] }
requires { [@expl:no overflow] forall l h. 0 <= l <= h <= length a ->
sum a l h <= max_int }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { forall l h. 0 <= l <= h <= length a -> result >= sum a !lo !hi }
= lo := 0;
hi := 0;
let n = length a in
......@@ -262,13 +265,13 @@ module BoundedIntegers
let s = ref zero in
let i = ref zero in
while !i < n do
invariant { 0 <= !lo <= !hi <= !i <= n && 0 <= !ms = sum a[!lo..!hi] }
invariant { forall l' h': int. 0 <= l' <= h' <= !i -> sum a[l'..h'] <= !ms }
invariant { 0 <= !l <= !i && !s = sum a[!l..!i] }
invariant { forall l': int. 0 <= l' < !i -> sum a[l'..!i] <= !s }
invariant { 0 <= !lo <= !hi <= !i <= n && 0 <= !ms = sum a !lo !hi }
invariant { forall l' h'. 0 <= l' <= h' <= !i -> sum a l' h' <= !ms }
invariant { 0 <= !l <= !i && !s = sum a !l !i }
invariant { forall l'. 0 <= l' < !i -> sum a l' !i <= !s }
variant { n - !i }
if !s < zero then begin s := a[!i]; l := to_int !i end
else begin assert { sum a[!l.. !i + 1] <= max_int }; s += a[!i] end;
else begin assert { sum a !l (!i + 1) <= max_int }; s += a[!i] end;
if !s > !ms then begin
ms := !s; lo := !l; hi := to_int !i + 1 end;
incr i
......@@ -276,4 +279,3 @@ module BoundedIntegers
!ms
end
*)
This diff is collapsed.
......@@ -40,12 +40,11 @@ module Merge
(* merges tmp[l..m[ and tmp[m..r[ into a[l..r[ *)
let merge (tmp a: array elt) (l m r: int) : (ghost p: permutation)
requires { 0 <= l <= m <= r <= length tmp = length a }
requires { sorted tmp[l..m] }
requires { sorted tmp[m..r] }
ensures { sorted a[l..r] }
ensures { permut_slice tmp a l r p }
ensures { forall i: int.
(0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
requires { sorted tmp l m }
requires { sorted tmp m r }
ensures { sorted a l r }
ensures { permut tmp a l r p }
ensures { forall i. (0 <= i < l \/ r <= i < #a) -> a[i] = (old a)[i] }
= let ref i = l in
let ref j = m in
let ghost ref fwd = create (length a) (fun i -> i) in
......@@ -53,7 +52,7 @@ module Merge
for k = l to r-1 do
invariant { l <= i <= m <= j <= r }
invariant { i - l + j - m = k - l }
invariant { sorted a[l..k] }
invariant { sorted a l k }
invariant { forall x y: int. l <= x < k -> i <= y < m -> le a[x] tmp[y] }
invariant { forall x y: int. l <= x < k -> j <= y < r -> le a[x] tmp[y] }
invariant { #fwd = #inv = #a }
......@@ -74,9 +73,9 @@ module Merge
fwd := fwd[j <- k]; inv := inv[k <- j];
incr j
end;
assert { sorted a[l..k] };
assert { forall x y: int. l <= x < k -> i <= y < m -> le a[x] tmp[y] };
assert { forall x y: int. l <= x < k -> j <= y < r -> le a[x] tmp[y] };
assert { sorted a l k };
assert { forall x y. l <= x < k -> i <= y < m -> le a[x] tmp[y] };
assert { forall x y. l <= x < k -> j <= y < r -> le a[x] tmp[y] };
done;
ghost { forward = fwd; inverse = inv }
......
......@@ -11,13 +11,13 @@ module SelectionSort
use seq.Permut
let selection_sort (a: array int) : (ghost p: permutation)
ensures { sorted a /\ permut (old a) a p } =
ensures { sorted_all a /\ permut_all (old a) a p } =
let ref min = 0 in
let ghost ref p = identity a.length in
for i = 0 to length a - 1 do
(* a[0..i[ is sorted; now find minimum of a[i..n[ *)
invariant { sorted a[..i] }
invariant { permut (old a) a p }
invariant { sorted a 0 i }
invariant { permut_all (old a) a p }
invariant { forall k1 k2. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
(* let min = ref i in *) min := i;
for j = i + 1 to length a - 1 do
......@@ -27,7 +27,6 @@ module SelectionSort
done;
label L in
if min <> i then p := swap a min i p;
assert { sorted a[..i] };
done;
p
......
......@@ -12,79 +12,73 @@
<goal name="VC selection_sort" expl="VC for selection_sort" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC selection_sort.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="11762"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="12544"/></proof>
</goal>
<goal name="VC selection_sort.1" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="13989"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="13735"/></proof>
</goal>
<goal name="VC selection_sort.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.10" steps="25976"/></proof>
<proof prover="3"><result status="valid" time="0.10" steps="21706"/></proof>
</goal>
<goal name="VC selection_sort.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="13129"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="14422"/></proof>
</goal>
<goal name="VC selection_sort.4" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="11897"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="12636"/></proof>
</goal>
<goal name="VC selection_sort.5" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="14208"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="15561"/></proof>
</goal>
<goal name="VC selection_sort.6" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="19174"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="20525"/></proof>
</goal>
<goal name="VC selection_sort.7" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="19178"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="20529"/></proof>
</goal>
<goal name="VC selection_sort.8" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="12377"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="13116"/></proof>
</goal>
<goal name="VC selection_sort.9" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="18214"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="19061"/></proof>
</goal>
<goal name="VC selection_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="12243"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="12982"/></proof>
</goal>
<goal name="VC selection_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="17266"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="18550"/></proof>
</goal>
<goal name="VC selection_sort.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="19279"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="20543"/></proof>
</goal>
<goal name="VC selection_sort.13" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="19634"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="20826"/></proof>
</goal>
<goal name="VC selection_sort.14" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.30" steps="792581"/></proof>
<goal name="VC selection_sort.14" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.51" steps="1193457"/></proof>
</goal>
<goal name="VC selection_sort.15" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="227656"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="17626"/></proof>
</goal>
<goal name="VC selection_sort.16" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="13195"/></proof>
<proof prover="2"><result status="valid" time="2.31" steps="4091"/></proof>
</goal>
<goal name="VC selection_sort.17" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="1.25" steps="2750"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="66110"/></proof>
</goal>
<goal name="VC selection_sort.18" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="12489"/></proof>
<goal name="VC selection_sort.18" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="16549"/></proof>
</goal>
<goal name="VC selection_sort.19" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="34742"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="19454"/></proof>
</goal>
<goal name="VC selection_sort.20" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="12220"/></proof>
<goal name="VC selection_sort.20" expl="out of loop bounds" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="17536"/></proof>
</goal>
<goal name="VC selection_sort.21" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="18943"/></proof>
<goal name="VC selection_sort.21" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="19715"/></proof>
</goal>
<goal name="VC selection_sort.22" expl="out of loop bounds" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="15844"/></proof>
</goal>
<goal name="VC selection_sort.23" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="15297"/></proof>
</goal>
<goal name="VC selection_sort.24" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="13366"/></proof>
<goal name="VC selection_sort.22" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="18731"/></proof>
</goal>
</transf>
</goal>
......
......@@ -34,10 +34,10 @@ module Simple
index `i` inclusive and index `j` exclusive *)
let query (a: array int) (i j: int) : int
requires { 0 <= i <= j <= a.length }
ensures { result = sum a[i..j] }
ensures { result = sum a i j }
= let ref s = 0 in
for k = i to j-1 do
invariant { s = sum a[i..k] }
invariant { s = sum a i k }
s <- s + a[k]
done;
s
......@@ -50,13 +50,15 @@ module ExtraLemmas
use seq.Seq
use seq.Sum
(*
lemma slice_ext: forall s1 s2: seq 'a, i j.
0 <= i <= j <= #s1 -> j <= #s2 ->
(forall k. i <= k < j -> s1[k] = s2[k]) ->
s1[i..j] = s2[i..j]
*)
lemma sum_set_slice : forall s i j k v. 0 <= i <= k < j <= #s ->
sum s[k <- v][i..j] = sum s[i..j] + v - s[k]
sum s[k <- v] i j = sum s i j + v - s[k]
end
......@@ -80,7 +82,7 @@ module CumulativeArray
predicate is_cumulative_array_for (c: seq int) (a: seq int) =
#c = #a + 1 /\
forall i. 0 <= i < #c -> c[i] = sum a[..i]
forall i. 0 <= i < #c -> c[i] = sum a 0 i
(** `create a` builds the cumulative array associated with `a`. *)
let create (a:array int) : array int
......@@ -88,7 +90,7 @@ module CumulativeArray
= let l = a.length in
let s = Array.make (l+1) 0 in
for i = 1 to l do
invariant { forall k. 0 <= k < i -> s[k] = sum a[..k] }
invariant { forall k. 0 <= k < i -> s[k] = sum a 0 k }
s[i] <- s[i-1] + a[i-1]
done;
s
......@@ -98,13 +100,13 @@ module CumulativeArray
let query (c:array int) (i j:int) (ghost a:array int): int
requires { is_cumulative_array_for c a }
requires { 0 <= i <= j < c.length }
ensures { result = sum a[i..j] }
ensures { result = sum a i j }
= c[j] - c[i]
(** `update c i v a` updates cell `a[i]` to value `v` and updates
the cumulative array `c` accordingly *)
let update (c:array int) (i:int) (v:int) (ghost a:array int) : unit
let update (c: array int) (i: int) (v: int) (ghost a: array int) : unit
requires { is_cumulative_array_for c a }
requires { 0 <= i < a.length }
writes { c, a }
......@@ -115,8 +117,8 @@ module CumulativeArray
= let incr = v - c[i+1] + c[i] in
a[i] <- v;
for j=i+1 to c.length-1 do
invariant { forall k. j <= k < c.length -> c[k] = sum a[..k] - incr }
invariant { forall k. 0 <= k < j -> c[k] = sum a[..k] }
invariant { forall k. j <= k < c.length -> c[k] = sum a 0 k - incr }
invariant { forall k. 0 <= k < j -> c[k] = sum a 0 k }
c[j] <- c[j] + incr
done
......@@ -165,7 +167,7 @@ module CumulativeTree
predicate is_indexes_for (ind:indexes) (a: seq int) (i j:int) =
ind.low = i /\ ind.high = j /\
0 <= i < j <= #a /\
ind.isum = sum a[i..j]
ind.isum = sum a i j
predicate is_tree_for (t:tree) (a: seq int) (i j: int) =
match t with
......@@ -197,7 +199,7 @@ module CumulativeTree
let l = tree_of_array a i m in
let r = tree_of_array a m j in
let s = l.indexes.isum + r.indexes.isum in
assert { s = sum a[i..j] };
assert { s = sum a i j };
let ind = { low = i; high = j; isum = s} in
assert { is_indexes_for ind a i j };
Node ind l r
......@@ -217,7 +219,7 @@ module CumulativeTree
requires { is_tree_for t a t.indexes.low t.indexes.high }
requires { 0 <= t.indexes.low <= i < j <= t.indexes.high <= a.length }
variant { t }
ensures { result = sum a[i..j] }
ensures { result = sum a i j }
= match t with
| Leaf ind ->
ind.isum
......@@ -235,7 +237,7 @@ module CumulativeTree
let query (t:tree) (ghost a: array int) (i j:int) : int
requires { 0 <= i <= j <= a.length }
requires { is_tree_for t a 0 a.length }
ensures { result = sum a[i..j] }
ensures { result = sum a i j }
= if i=j then 0 else query_aux t a i j
......@@ -379,7 +381,7 @@ module CumulativeTree
if i = t.indexes.low /\ j = t.indexes.high then 1 else
if i = t.indexes.low \/ j = t.indexes.high then 2 * depth t else
4 * depth t }
ensures { result = sum a[i..j] }
ensures { result = sum a i j }
= c := !c + 1;
match t with
| Leaf ind ->
......
This diff is collapsed.
......@@ -7,27 +7,27 @@
<path name=".."/><path name="zeros.mlw"/>
<theory name="SetZeros" proved="true">
<goal name="VC set_zeros" expl="VC for set_zeros" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="37"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</theory>
<theory name="AllZeros" proved="true">
<goal name="VC all_zeros1" expl="VC for all_zeros1" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="71"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
</goal>
<goal name="VC all_zeros2" expl="VC for all_zeros2" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="78"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
</goal>
<goal name="VC all_zeros3" expl="VC for all_zeros3" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="41"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC all_zeros4" expl="VC for all_zeros4" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="55"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
<goal name="VC all_zeros5" expl="VC for all_zeros5" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="415"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="341"/></proof>
</goal>
</theory>
</file>
......
......@@ -178,18 +178,19 @@ module Init
end
module ArraySwap
module Swap
use int.Int
use Array
use seq.Permut
let swap (a:array 'a) (i: int) (j: int) (ghost p: permutation) :
let swap (a: array 'a) (i: int) (j: int) (ghost p: permutation) :
(ghost q: permutation)
requires { 0 <= i < #a /\ 0 <= j < #a }
requires { #p = #a }
ensures { a = (old a)[i <- old a[j]][j <- old a[i]] }
ensures { forall b: seq 'a. permut b (old a) p -> permut b a q }
ensures { forall b: seq 'a, l r. 0 <= l <= i < r <= #a -> l <= j < r ->
permut b (old a) l r p -> permut b a l r q }
= let v = a[i] in
a[i] <- a[j];
a[j] <- v;
......
......@@ -443,12 +443,14 @@ module Sum
a <= b <= c ->
sum f a c = sum f a b + sum f b c
(*
let rec lemma shift_left (f g: int -> int) (a b c d: int)
requires { b - a = d - c }
requires { forall i. a <= i < b -> f i = g (c + i - a) }
variant { b - a }
ensures { sum f a b = sum g c d }
= if a < b then shift_left f g (a+1) b (c+1) d
*)
end
......
......@@ -221,12 +221,12 @@ module Array63
use int.Int
use mach.int.Int63
use seq.Seq
use export seq.Seq
type array 'a = private {
mutable ghost elts : seq 'a;
length : int63;
} invariant { 0 <= length = Seq.length elts }
} invariant { 0 <= length = #elts }
meta coercion function elts
......@@ -326,86 +326,37 @@ module Array63
end
module Array63Exchange
(* module Array63Exchange *)
use int.Int
use mach.int.Int63
use Array63
use seq.Exchange as SE
(* use int.Int *)
(* use mach.int.Int63 *)
(* use Array63 *)
(* use seq.Exchange as SE *)
predicate exchange (a1 a2: array 'a) (i j: int) =
SE.exchange a1.elts a2.elts i j
(** `exchange a1 a2 i j` means that arrays `a1` and `a2` only differ
by the swapping of elements at indices `i` and `j` *)
(* predicate exchange (a1 a2: array 'a) (i j: int) = *)
(* SE.exchange a1.elts a2.elts i j *)
(* (\** `exchange a1 a2 i j` means that arrays `a1` and `a2` only differ *)
(* by the swapping of elements at indices `i` and `j` *\) *)
end
(* end *)
module Array63Swap
use int.Int
use mach.int.Int63
use Array63
use export Array63Exchange
let swap (a:array 'a) (i j:int63) : unit
let swap (a: array 'a) (i j: int63) : unit
requires { 0 <= i < length a /\ 0 <= j < length a }
writes { a }
ensures { exchange (old a) a i j }
(* ensures { exchange (old a) a i j } *)
ensures { a = (old a)[i <- old a[j]][j <- old a[i]] }
= let v = a[i] in
a[i] <- a[j];
a[j] <- v
end
module Array63Permut
use int.Int
use mach.int.Int63
use Array63
use seq.Seq
use seq.SeqEq
use seq.Permut as SP
use Array63Exchange
predicate permut (a1 a2: array 'a) (l u: int) =
SP.permut a1.elts a2.elts l u
(** `permut a1 a2 l u` is true when the segment
`a1(l..u-1)` is a permutation of the segment `a2(l..u-1)`.
Values outside of the interval `(l..u-1)` are ignored. *)
predicate array_eq (a1 a2: array 'a) (l u: int) =
seq_eq_sub a1.elts a2.elts l u
predicate permut_sub (a1 a2: array 'a) (l u: int) =
seq_eq_sub a1.elts a2.elts 0 l /\
permut a1 a2 l u /\
seq_eq_sub a1.elts a2.elts u (length a1)