...
 
Commits (22)
......@@ -2,7 +2,7 @@ module M
use int.Int
use ref.Ref
use map.Map
use import map.MapBrackets as Map
let ghost test_map (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
......
module M
use map.Map
use import map.MapBrackets as Map
use int.Int
type r = {f [@model_trace:.field_f] :int; g:bool}
......
......@@ -195,3 +195,8 @@ theory map.Map
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
end
theory map.MapBrackets
syntax function ([]) "(%1[%2])"
syntax function ([<-]) "(%1[%2 <- %3])"
end
......@@ -63,6 +63,10 @@ theory map.Map
syntax function get "(%1 %2)"
end
theory map.MapBrackets
syntax function ([]) "(%1 %2)"
end
theory int.Int
prelude "
......
......@@ -163,4 +163,12 @@ theory map.Map
meta "encoding:lskept" function set
end
theory map.MapBrackets
syntax function ([]) "(%1[%2])"
syntax function ([<-]) "(%1 WITH [%2] := %3)"
meta "encoding:lskept" function ([])
meta "encoding:lskept" function ([<-])
end
import "discrimination.gen"
......@@ -137,8 +137,11 @@ end
theory map.Map
syntax function get "<app>%1%2</app>"
syntax function ([]) "<app>%1%2</app>"
syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
end
theory map.MapBrackets
syntax function ([]) "<app>%1%2</app>"
syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
end
......
......@@ -180,6 +180,14 @@ theory map.Map
meta "encoding:lskept" function set
end
theory map.MapBrackets
syntax function ([]) "(select %1 %2)"
syntax function ([<-]) "(store %1 %2 %3)"
meta "encoding:lskept" function ([])
meta "encoding:lskept" function ([<-])
end
theory map.Const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
......
......@@ -33,10 +33,12 @@ theory HighOrd
end
theory map.Map
syntax function get "%1(%2)"
syntax function ([]) "%1(%2)"
syntax function get "%1(%2)"
syntax function set "(%1 WITH [(%2) |-> %3])"
end
syntax function set "(%1 WITH [(%2) |-> %3])"
theory map.MapBrackets
syntax function ([]) "%1(%2)"
syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
end
......
......@@ -187,8 +187,16 @@ theory map.Map
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
end
theory map.MapBrackets
syntax function ([]) "(select %1 %2)"
syntax function ([<-]) "(store %1 %2 %3)"
meta "encoding:lskept" function ([])
meta "encoding:lskept" function ([<-])
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function ([<-])
end
......
......@@ -48,8 +48,13 @@ theory map.Map
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
end
theory map.MapBrackets
meta "encoding:lskept" function ([])
meta "encoding:lskept" function ([<-])
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function ([<-])
end
......
......@@ -144,14 +144,20 @@ end
theory map.Map
syntax function get "(%1 %2)"
syntax function ([]) "(%1 %2)"
syntax function set "(update %1 (%2) %3)"
syntax function ([<-]) "(update %1 (%2) %3)"
meta "encoding:lskept" function get
meta "encoding:lskept" function set
end
theory map.MapBrackets
syntax function ([]) "(%1 %2)"
syntax function ([<-]) "(update %1 (%2) %3)"
meta "encoding:lskept" function ([])
meta "encoding:lskept" function ([<-])
end
theory map.Const
meta "encoding:lskept" function const
end
......@@ -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>
......
......@@ -47,9 +47,9 @@ module ARM
(* memory *)
val mem : ref (map int int)
val mem_ldr (a:int) : int ensures { result = !mem[a] }
val mem_ldr (a:int) : int ensures { result = !mem a }
val mem_str (a:int) (v:int) : int writes { mem }
ensures { !mem = (old !mem)[a <- v] }
ensures { !mem = set (old !mem) a v }
(* data segment *)
(*
......@@ -69,10 +69,10 @@ module ARM
val pc : ref int (* pc *)
val ldr (r : ref int) (a : int) : unit writes {r}
ensures { !r = !mem[a] }
ensures { !r = !mem a }
val str (r : ref int) (a : int) : unit writes {mem}
ensures { !mem = (old !mem)[a <- !r] }
ensures { !mem = set (old !mem) a !r }
(* condition flags *)
val le : ref bool
......@@ -113,10 +113,10 @@ module InsertionSortExample
predicate separation (fp : int) = a+10 < fp-24
predicate inv (mem: map int int) =
mem[a] = 0 /\ forall k:int. 1 <= k <= 10 -> 0 < mem[a + k]
mem a = 0 /\ forall k:int. 1 <= k <= 10 -> 0 < mem (a + k)
predicate inv_l2 (mem: map int int) (fp : int) (l4 : int) =
2 <= mem[fp - 16] <= 11 /\ l4 = mem[fp-16] - 2 /\ inv mem
2 <= mem (fp - 16) <= 11 /\ l4 = mem (fp-16) - 2 /\ inv mem
let path_init_l2 ()
requires { separation !fp /\ inv !mem }
......
......@@ -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>
......
......@@ -33,5 +33,5 @@ theory Bug
goal bug: forall i.
let p = ((PTR i):(p (map t t))) in
let q = ((PTR i):(p t)) in
(load p)[i] = (load q)
load p i = load q
end
......@@ -37,6 +37,8 @@ lemma sorted_tail:
forall s. sorted s -> length s >= 1 -> sorted s[1 .. ]
lemma sorted_tail_tail:
forall s. sorted s -> length s >= 2 -> sorted s[2 .. ]
lemma sum_tail_tail:
forall s. #s >= 2 -> sum s = s[0] + s[1] + sum s[2 .. ]
let huffman_coding (s: seq int) : int
requires { length s > 0 }
......
......@@ -14,7 +14,7 @@ module Spec
use int.Int
use export array.Array
use export array.ArraySum
use export seq.Sum
(* provides [sum a l h] = the sum of a[l..h[ and suitable lemmas *)
(* s is no smaller than sums of subarrays a[l..h[ with 0 <= l < maxlo *)
......@@ -45,20 +45,20 @@ module Algo1
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 }
s += a[i]
done;
assert { !s = sum a l h };
if !s > !ms then begin ms := !s; lo := l; hi := h end
done
done;
......@@ -83,17 +83,17 @@ module Algo2
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 { forall h'. l <= h' < h -> sum a l h' <= !ms }
invariant { !s = sum a l (h-1) }
s += a[h-1]; (* update the sum *)
assert { !s = sum a l h };
if !s > !ms then begin ms := !s; lo := l; hi := h end
done
done;
......@@ -114,7 +114,7 @@ module Algo3
: 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 { 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 *)
......@@ -131,20 +131,15 @@ module Algo3
invariant { forall l': int. i < l' <= mid -> sum a l' mid <= !ms }
invariant { !s = sum a (i+1) mid }
s += a[i];
assert { !s = sum a i mid };
if !s > !ms then begin ms := !s; lo := i end
done;
assert { forall l': int. l <= l' <= mid ->
sum a l' mid <= sum a !lo mid };
s := !ms;
for i = mid to h-1 do
invariant { l <= !lo <= mid <= !hi <= h && !ms = sum a !lo !hi }
invariant { forall l' h': int. l <= l' <= mid <= h' <= i ->
sum a l' h' <= !ms }
invariant { !s = sum a !lo 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];
assert { !s = sum a !lo (i+1) };
assert { !s = sum a !lo mid + sum a mid (i+1) };
if !s > !ms then begin ms := !s; hi := (i+1) end
done;
(* then consider sums in a[l..mid[ and a[mid+1..h[, recursively *)
......@@ -189,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 <= !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': int. 0 <= l' < i -> sum a l' i <= !s }
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;
......@@ -207,7 +203,7 @@ module Algo5
use int.Int
use ref.Refint
use export array.Array
use export array.ArraySum
use export seq.Sum
(*
[| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |]
......@@ -216,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
......@@ -225,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
......@@ -249,7 +245,6 @@ module BoundedIntegers
use int.Int
use mach.int.Int63
use mach.int.Refint63
use seq.Seq
use mach.array.Array63
use int.Sum
......@@ -257,9 +252,9 @@ 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 ->
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 { 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;
......@@ -270,9 +265,9 @@ module BoundedIntegers
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 { forall l' h'. 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 { 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;
......
This diff is collapsed.
......@@ -18,8 +18,8 @@ module Elt
clone relations.TotalPreOrder with
type t = elt, predicate rel = le, axiom .
clone export array.Sorted with type
elt = elt, predicate le = le, axiom .
clone export seq.Sorted with type
t = elt, predicate rel = le, axiom .
end
......@@ -35,46 +35,58 @@ module Merge
clone export Elt with axiom .
use export ref.Refint
use export array.Array
use map.Occ
use export array.ArrayPermut
use export seq.Permut
(* merges tmp[l..m[ and tmp[m..r[ into a[l..r[ *)
let merge (tmp a: array elt) (l m r: int) : unit
let merge (tmp a: array elt) (l m r: int) : (ghost p: permutation)
requires { 0 <= l <= m <= r <= length tmp = length a }
requires { sorted_sub tmp l m }
requires { sorted_sub tmp m r }
ensures { sorted_sub a l r }
ensures { permut tmp a l r }
ensures { forall i: int.
(0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
= let i = ref l in
let j = ref m in
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
let ghost ref inv = create (length a) (fun i -> i) in
for k = l to r-1 do
invariant { l <= !i <= m <= !j <= r }
invariant { !i - l + !j - m = k - l }
invariant { sorted_sub 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 { forall v: elt.
occ v tmp.elts l !i + occ v tmp.elts m !j = occ v a.elts l k }
invariant { forall i: int.
(0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
if !i < m && (!j = r || le tmp[!i] tmp[!j]) then begin
a[k] <- tmp[!i];
incr i
invariant { l <= i <= m <= j <= r }
invariant { i - l + j - m = k - l }
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 }
invariant { forall x. l <= x < i \/ m <= x < j -> l <= fwd[x] < k }
invariant { forall x. l <= x < k -> l <= inv[x] < i \/ m <= inv[x] < j }
invariant { forall x. l <= x < i \/ m <= x < j -> inv[fwd[x]] = x }
invariant { forall x. l <= x < k -> fwd[inv[x]] = x }
invariant { forall x. 0 <= x < l \/ r <= x < #a-> fwd[x] = inv[x] = x }
invariant { forall x. l <= x < i \/ m <= x < j -> a[fwd[x]] = tmp[x] }
invariant { forall i.
(0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
if i < m && (j = r || le tmp[i] tmp[j]) then begin
a[k] <- tmp[i];
fwd := fwd[i <- k]; inv := inv[k <- i];
incr i;
end else begin
a[k] <- tmp[!j];
a[k] <- tmp[j];
fwd := fwd[j <- k]; inv := inv[k <- j];
incr j
end
done
end;
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 }
(*
(* merges a[l..m[ and a[m..r[ into a[l..r[, using tmp as a temporary *)
let merge_using (tmp a: array elt) (l m r: int) : unit
requires { 0 <= l <= m <= r <= length tmp = length a }
requires { sorted_sub a l m }
requires { sorted_sub a m r }
ensures { sorted_sub a l r }
ensures { permut (old a) a l r }
requires { sorted a[l..m] }
requires { sorted a[m..r] }
ensures { sorted a[l..r] }
(* ensures { permut (old a) a l r } *)
ensures { forall i: int.
(0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
= if l < m && m < r then (* both sides are non empty *)
......@@ -85,11 +97,12 @@ module Merge
label N in
blit a l tmp l (r - l);
merge tmp a l m r;
assert { permut_sub (a at N) a l r }
(* assert { permut_sub (a at N) a l r } *)
end
*)
end
(*
(** {2 Top-down, recursive mergesort}
Split in equal halves, recursively sort the two, and then merge. *)
......@@ -98,30 +111,34 @@ module TopDownMergesort
clone Merge with axiom .
use mach.int.Int
use array.Array
let rec mergesort_rec (a tmp: array elt) (l r: int) : unit
requires { 0 <= l <= r <= length a = length tmp }
ensures { sorted_sub a l r }
ensures { permut_sub (old a) a l r }
ensures { sorted a[l..r] }
(* ensures { permut_sub (old a) a l r } *)
variant { r - l }
= if l >= r-1 then return;
let m = l + (r - l) / 2 in
assert { l <= m < r };
mergesort_rec a tmp l m;
assert { permut_sub (old a) a l r };
(* assert { permut_sub (old a) a l r }; *)
label M in
mergesort_rec a tmp m r;
assert { permut_sub (a at M) a l r };
(* assert { permut_sub (a at M) a l r }; *)
merge_using tmp a l m r
let mergesort (a: array elt) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
(* ensures { permut_all (old a) a } *)
=
let tmp = Array.copy a in
mergesort_rec a tmp 0 (length a)
end
*)
(*
(** {2 Bottom-up, iterative mergesort}
......@@ -305,3 +322,5 @@ module NaturalMergesort
()
end
*)
......@@ -24,7 +24,7 @@ module Mjrty
use int.Int
use ref.Refint
use array.Array
use array.NumOfEq
use seq.Occ
exception Not_found
......@@ -35,15 +35,15 @@ module Mjrty
let mjrty (a: array candidate) : candidate
requires { 1 <= length a }
ensures { 2 * numof a result 0 (length a) > length a }
raises { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a }
ensures { 2 * occ result a > length a }
raises { Not_found -> forall c. 2 * occ c a <= length a }
= let n = length a in
let cand = ref a[0] in
let k = ref 0 in
for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *)
invariant { 0 <= !k <= numof a !cand 0 i }
invariant { 2 * (numof a !cand 0 i - !k) <= i - !k }
invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k }
invariant { 0 <= !k <= occ !cand a[..i] }
invariant { 2 * (occ !cand a[..i] - !k) <= i - !k }
invariant { forall c. c <> !cand -> 2 * occ c a[..i] <= i - !k }
if !k = 0 then begin
cand := a[i];
k := 1
......@@ -56,7 +56,7 @@ module Mjrty
if 2 * !k > n then return !cand;
k := 0;
for i = 0 to n - 1 do
invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
invariant { !k = occ !cand a[..i] /\ 2 * !k <= n }
if a[i] = !cand then begin
incr k;
if 2 * !k > n then return !cand
......
......@@ -2,12 +2,89 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="Z3" version="4.6.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/><path name="mjrty.mlw"/>
<theory name="Mjrty" proved="true">
<goal name="VC mjrty" expl="VC for mjrty" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="377443"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC mjrty.0" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18501"/></proof>
</goal>
<goal name="VC mjrty.1" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18639"/></proof>
</goal>
<goal name="VC mjrty.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18672"/></proof>
</goal>
<goal name="VC mjrty.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.07" steps="17423"/></proof>
</goal>
<goal name="VC mjrty.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="19843"/></proof>
</goal>
<goal name="VC mjrty.5" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="26744"/></proof>
</goal>
<goal name="VC mjrty.6" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.30" steps="61896"/></proof>
</goal>
<goal name="VC mjrty.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.38" steps="70907"/></proof>
</goal>
<goal name="VC mjrty.8" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="19849"/></proof>
</goal>
<goal name="VC mjrty.9" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18339"/></proof>
</goal>
<goal name="VC mjrty.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="17990"/></proof>
</goal>
<goal name="VC mjrty.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.34" steps="72473"/></proof>
</goal>
<goal name="VC mjrty.12" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18303"/></proof>
</goal>
<goal name="VC mjrty.13" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.05" steps="17977"/></proof>
</goal>
<goal name="VC mjrty.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="307"/></proof>
</goal>
<goal name="VC mjrty.15" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="22900"/></proof>
</goal>
<goal name="VC mjrty.16" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="16928"/></proof>
</goal>
<goal name="VC mjrty.17" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="17827"/></proof>
</goal>
<goal name="VC mjrty.18" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="21008"/></proof>
</goal>
<goal name="VC mjrty.19" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="26673"/></proof>
</goal>
<goal name="VC mjrty.20" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18984"/></proof>
</goal>
<goal name="VC mjrty.21" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="18854"/></proof>
</goal>
<goal name="VC mjrty.22" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="24171"/></proof>
</goal>
<goal name="VC mjrty.23" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="14203"/></proof>
</goal>
<goal name="VC mjrty.24" expl="out of loop bounds" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="14400"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
......@@ -6,40 +6,41 @@ module SelectionSort
use int.Int
use ref.Ref
use array.Array
use array.IntArraySorted
use array.ArraySwap
use array.ArrayPermut
use array.ArrayEq
use seq.SortedInt
use seq.Permut
let selection_sort (a: array int)
ensures { sorted a /\ permut_all (old a) a } =
let min = ref 0 in
let selection_sort (a: array int) : (ghost p: permutation)
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_sub a 0 i /\ permut_all (old a) a /\
forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
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
invariant {
i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
if a[j] < a[!min] then min := j
invariant { i <= min < j }
invariant { forall k. i <= k < j -> a[min] <= a[k] }
if a[j] < a[min] then min := j
done;
label L in
if !min <> i then swap a !min i;
assert { permut_all (a at L) a }
done
if min <> i then p := swap a min i p;
done;
p
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
selection_sort a;
let _ = selection_sort a in
a
let test2 () ensures { result.length = 8 } =
let a = make 8 0 in
a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
selection_sort a;
let _ = selection_sort a in
a
exception BenchFailure
......
......@@ -2,53 +2,83 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="Z3" version="4.8.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/><path name="selection_sort.mlw"/>
<theory name="SelectionSort" proved="true">
<goal name="VC selection_sort" expl="VC for selection_sort" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC selection_sort.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
<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="12544"/></proof>
</goal>
<goal name="VC selection_sort.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="13735"/></proof>
</goal>
<goal name="VC selection_sort.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<goal name="VC selection_sort.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.10" steps="21706"/></proof>
</goal>
<goal name="VC selection_sort.3" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<goal name="VC selection_sort.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="14422"/></proof>
</goal>
<goal name="VC selection_sort.4" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
<goal name="VC selection_sort.4" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="12636"/></proof>
</goal>
<goal name="VC selection_sort.5" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="27"/></proof>
<goal name="VC selection_sort.5" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="15561"/></proof>
</goal>
<goal name="VC selection_sort.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
<goal name="VC selection_sort.6" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="20525"/></proof>
</goal>
<goal name="VC selection_sort.7" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="73"/></proof>
<goal name="VC selection_sort.7" expl="index in array bounds" proved="true">
<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="1"><result status="valid" time="0.34" steps="573"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="13116"/></proof>
</goal>
<goal name="VC selection_sort.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
<goal name="VC selection_sort.9" expl="loop invariant preservation" proved="true">
<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="1"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="12982"/></proof>
</goal>
<goal name="VC selection_sort.11" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
<goal name="VC selection_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="18550"/></proof>
</goal>
<goal name="VC selection_sort.12" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
<goal name="VC selection_sort.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="20543"/></proof>
</goal>
<goal name="VC selection_sort.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<goal name="VC selection_sort.13" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="20826"/></proof>
</goal>
<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="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="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="0"><result status="valid" time="0.06" steps="66110"/></proof>
</goal>
<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.06" steps="19454"/></proof>
</goal>
<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="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="19715"/></proof>
</goal>
<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>
......
......@@ -21,40 +21,6 @@ with logarithmic time operations.
*)
(** {2 Specification of Range Sum} *)
module ArraySum
use int.Int
use array.Array
(** `sum a i j` denotes the sum `\sum_{i <= k < j} a[k]`.
It is axiomatizated by the two following axioms expressing
the recursive definition
if `i <= j` then `sum a i j = 0`
if `i < j` then `sum a i j = a[i] + sum a (i+1) j`
*)
let rec function sum (a:array int) (i j:int) : int
requires { 0 <= i <= j <= a.length }
variant { j - i }
= if j <= i then 0 else a[i] + sum a (i+1) j
(** lemma for summation from the right:
if `i < j` then `sum a i j = sum a i (j-1) + a[j-1]`
*)
lemma sum_right : forall a : array int, i j : int.
0 <= i < j <= a.length ->
sum a i j = sum a i (j-1) + a[j-1]
end
(** {2 First algorithm, a linear one} *)
......@@ -62,61 +28,40 @@ module Simple
use int.Int
use array.Array
use ArraySum
use ref.Ref
use seq.Sum
(** `query a i j` returns the sum of elements in `a` between
index `i` inclusive and index `j` exclusive *)
let query (a:array int) (i j:int) : int
let query (a: array int) (i j: int) : int
requires { 0 <= i <= j <= a.length }
ensures { result = sum a i j }
= let s = ref 0 in
for k=i to j-1 do
invariant { !s = sum a i k }
s := !s + a[k]
ensures { result = sum a i j }
= let ref s = 0 in
for k = i to j-1 do
invariant { s = sum a i k }
s <- s + a[k]
done;
!s
s
end
(** {2 Additional lemmas on `sum`}
needed in the remaining code *)
module ExtraLemmas
use int.Int
use array.Array
use ArraySum
(** summation in adjacent intervals *)
lemma sum_concat : forall a:array int, i j k:int.
0 <= i <= j <= k <= a.length ->
sum a i k = sum a i j + sum a j k
(** Frame lemma for `sum`, that is `sum a i j` depends only
of values of `a[i..j-1]` *)
lemma sum_frame : forall a1 a2 : array int, i j : int.
0 <= i <= j ->
j <= a1.length ->
j <= a2.length ->
(forall k : int. i <= k < j -> a1[k] = a2[k]) ->
sum a1 i j = sum a2 i j
(** Updated lemma for `sum`: how does `sum a i j` changes when
`a[k]` is changed for some `k` in `[i..j-1]` *)
lemma sum_update : forall a:array int, i v l h:int.
0 <= l <= i < h <= a.length ->
sum (a[i<-v]) l h = sum a l h + v - a[i]
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]
end
(** {2 Algorithm 2: using a cumulative array}
creation of cumulative array is linear
......@@ -132,19 +77,19 @@ module CumulativeArray
use int.Int
use array.Array
use ArraySum
use seq.Sum
use ExtraLemmas
predicate is_cumulative_array_for (c:array int) (a:array int) =
c.length = a.length + 1 /\
forall i. 0 <= i < c.length -> c[i] = sum a 0 i
predicate is_cumulative_array_for (c: seq int) (a: seq int) =
#c = #a + 1 /\
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
ensures { is_cumulative_array_for result a }
= let l = a.length in
let s = Array.make (l+1) 0 in
for i=1 to l do
for i = 1 to l do
invariant { forall k. 0 <= k < i -> s[k] = sum a 0 k }
s[i] <- s[i-1] + a[i-1]
done;
......@@ -161,7 +106,7 @@ module CumulativeArray
(** `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 }
......@@ -201,9 +146,9 @@ module CumulativeTree
use int.Int
use array.Array
use ArraySum
use ExtraLemmas
use seq.Sum
use int.ComputerDivision
use ExtraLemmas
type indexes =
{ low : int;
......@@ -219,12 +164,12 @@ module CumulativeTree
| Node ind _ _ -> ind
end
predicate is_indexes_for (ind:indexes) (a:array int) (i j:int) =
predicate is_indexes_for (ind:indexes) (a: seq int) (i j:int) =
ind.low = i /\ ind.high = j /\
0 <= i < j <= a.length /\
0 <= i < j <= #a /\
ind.isum = sum a i j
predicate is_tree_for (t:tree) (a:array int) (i j:int) =
predicate is_tree_for (t:tree) (a: seq int) (i j: int) =
match t with
| Leaf ind ->
is_indexes_for ind a i j /\ j = i+1
......@@ -242,22 +187,23 @@ module CumulativeTree
let rec tree_of_array (a:array int) (i j:int) : tree
requires { 0 <= i < j <= a.length }
variant { j - i }
ensures { is_tree_for result a i j }
= if i+1=j then begin
variant { j - i }
ensures { is_tree_for result a i j }
ensures { result.indexes.low = i }
ensures { result.indexes.high = j }
= if i+1 = j then begin
Leaf { low = i; high = j; isum = a[i] }
end
else
begin
end else begin
let m = div (i+j) 2 in
assert { i < m < j };
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 };
Node { low = i; high = j; isum = s} l r
end
let ind = { low = i; high = j; isum = s} in
assert { is_indexes_for ind a i j };
Node ind l r
end
let create (a:array int) : tree
requires { a.length >= 1 }
......@@ -296,8 +242,8 @@ module CumulativeTree
(** frame lemma for predicate `is_tree_for` *)
lemma is_tree_for_frame : forall t:tree, a:array int, k v i j:int.
0 <= k < a.length ->
lemma is_tree_for_frame : forall t:tree, a: seq int, k v i j:int.
0 <= k < #a ->
k < i \/ k >= j ->
is_tree_for t a i j ->
is_tree_for t a[k<-v] i j
......@@ -375,7 +321,7 @@ module CumulativeTree
use bv.Pow2int
let rec lemma depth_is_log (t:tree) (a :array int) (k:int)
let rec lemma depth_is_log (t:tree) (a: seq int) (k:int)
requires { k >= 0 }
requires { is_tree_for t a t.indexes.low t.indexes.high }
requires { t.indexes.high - t.indexes.low <= pow2 k }
......
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>
......
......@@ -61,6 +61,9 @@ let its_recursive s =
x.its_exposed && not x.its_liable &&
x.its_fixed && x.its_visible) s.its_arg_flg
(* FIXME: duplicated in vc.ml *)
let expl_type_inv = Ident.create_attribute "expl:type invariant"
let create_semi_constructor id s fdl pjl invl =
let tvl = List.map ity_var s.its_ts.ts_args in
let rgl = List.map ity_reg s.its_regions in
......@@ -72,6 +75,12 @@ let create_semi_constructor id s fdl pjl invl =
let eff = match ity.ity_node with
| Ityreg r -> eff_reset eff_empty (Sreg.singleton r)
| _ -> eff_empty in
let set_expl ({t_attrs=attrs} as t) =
let is_expl a = Strings.has_prefix "expl:" a.attr_string in
let attrs = if Sattr.exists is_expl attrs then attrs
else Sattr.add expl_type_inv attrs in
t_attr_set attrs t in
let invl = List.map set_expl invl in
let c = create_cty fdl invl [q] Mxs.empty Mpv.empty eff ity in
create_rsymbol id c
......
......@@ -131,7 +131,7 @@ let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
let op_char_pref = ['!' '?' '#']
rule token = parse
| "[##" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
......
......@@ -1246,7 +1246,7 @@ xsymbol:
invariant:
| INVARIANT option(ident_nq) LEFTBRC term RIGHTBRC
{ name_term $2 "LoopInvariant" $4 }
{ name_term $2 "Invariant" $4 }
variant:
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
......
......@@ -248,6 +248,17 @@ let find_symbol q tables =
try Tstysymbol (find_ts q tables) with
| Not_found -> raise (Arg_qid_not_found q)
let find_pr_list pr_list tables =
Lists.map_filter (fun id ->
try Some (find_pr id tables) with
| Not_found -> Warning.emit "Symbol '%a' not found, ignored"
Typing.print_qualid id; None) pr_list
let find_symbol_list pr_list tables =
Lists.map_filter (fun id ->
try Some (find_symbol id tables) with Arg_qid_not_found _ ->
Warning.emit "Symbol '%a' not found, ignored"
Typing.print_qualid id; None) pr_list
let type_ptree ~as_fmla t tables =
let km = tables.known_map in
......@@ -456,11 +467,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f pr) tail env tables task
| Tprlist t', s :: tail ->
let pr_list = parse_list_qualid s in
let pr_list =
List.map (fun id ->
try find_pr id tables with
| Not_found -> raise (Arg_qid_not_found id))
pr_list in
let pr_list = find_pr_list pr_list tables in
wrap_to_store t' (f pr_list) tail env tables task
| Tlsymbol t', s :: tail ->
let q = parse_qualid s in
......@@ -473,8 +480,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f symbol) tail env tables task
| Tlist t', s :: tail ->
let pr_list = parse_list_qualid s in
let pr_list =
List.map (fun id -> find_symbol id tables) pr_list in
let pr_list = find_symbol_list pr_list tables in
wrap_to_store t' (f pr_list) tail env tables task
| Ttheory t', s :: tail ->
let th = parse_theory env s in
......@@ -513,11 +519,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f arg) tail env tables task
| Tprlist t' ->
let pr_list = parse_list_qualid s' in
let pr_list =
List.map (fun id ->
try find_pr id tables with
| Not_found -> raise (Arg_qid_not_found id))
pr_list in
let pr_list = find_pr_list pr_list tables in
let arg = Some pr_list in
wrap_to_store t' (f arg) tail env tables task
| Ttermlist t' ->
......@@ -529,8 +531,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f (Some list)) tail env tables task
| Tlist t' ->
let pr_list = parse_list_qualid s' in
let pr_list =
List.map (fun id -> find_symbol id tables) pr_list in
let pr_list = find_symbol_list pr_list tables in
wrap_to_store t' (f (Some pr_list)) tail env tables task
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
......
......@@ -75,6 +75,13 @@ let remove_list ~is_rec (name_list: symbol list) =
if is_rec then
(Ident.Sid.union removed_ids d.d_news, task_uc)
else
let task_uc = match d.d_node with
| Dprop _ -> task_uc
| Dtype _ | Ddata _ | Dparam _ -> Task.add_decl task_uc d
| Dlogic dl -> List.fold_left (fun t (ls,_) ->
Task.add_param_decl t ls) task_uc dl
| Dind (_,il) -> List.fold_left (fun t (ls,_) ->
Task.add_param_decl t ls) task_uc il in
(removed_ids, task_uc)
| _ when not (Ident.Sid.is_empty removed_in_decls) ->
(* The task create an element we want to add but it uses deleted
......
......@@ -14,9 +14,9 @@ module Appmap
ensures { result.contents = const x }
val function ([]) (m: t 'a) (k: key): 'a
ensures { result = m.contents[k] }
ensures { result = m.contents k }
val function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
ensures { result.contents = m.contents[k <- v] }
ensures { result.contents = set m.contents k v }
end
This diff is collapsed.
......@@ -17,7 +17,7 @@ module Hashtbl
type t 'a = abstract { mutable contents: map key (list 'a) }
function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
function ([]) (h: t 'a) (k: key) : list 'a = Map.get h.contents k
val create (n:int) : t 'a ensures { forall k: key. result[k] = Nil }
......
......@@ -22,29 +22,29 @@ module Impmap
ensures { result <-> m.contents == const None }
val mem (k: key) (m: t 'a) : bool
ensures { result <-> m.contents[k] <> None }
ensures { result <-> m.contents k <> None }
val get (k: key) (m: t 'a) : 'a
requires { m.contents[k] <> None }
ensures { m.contents[k] = Some result }
requires { m.contents k <> None }
ensures { m.contents k = Some result }
val get_opt (k: key) (m: t 'a) : option 'a
ensures { result = m.contents[k] }
ensures { result = m.contents k }
val get_def (k: key) (d: 'a) (m: t 'a) : 'a
ensures { result = match m.contents[k] with None -> d | Some v -> v end }
ensures { result = match m.contents k with None -> d | Some v -> v end }
val find (k: key) (m: t 'a) : 'a
ensures { m.contents[k] = Some result }
raises { Not_found -> m.contents[k] = None }
ensures { m.contents k = Some result }
raises { Not_found -> m.contents k = None }
val add (k: key) (v: 'a) (m: t 'a) : unit
writes { m }
ensures { m.contents = old m.contents[k <- Some v] }
ensures { m.contents = set (old m.contents) k (Some v) }
val remove (k: key) (m: t 'a) : unit
writes { m }
ensures { m.contents = old m.contents[k <- None] }
ensures { m.contents = set (old m.contents) k None }
end
module ImpmapNoDom
......@@ -60,10 +60,10 @@ module ImpmapNoDom
ensures { result.contents = const x }
val function ([]) (m: t 'a) (k: key): 'a
ensures { result = m.contents[k] }
ensures { result = m.contents k }
val ghost function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
ensures { result.contents = m.contents[k <- v] }
ensures { result.contents = set m.contents k v }
val ([]<-) (m: t 'a) (k: key) (v: 'a): unit
writes { m }
......
......@@ -25,6 +25,11 @@ module Int
let predicate (<=) (x y : int) = x < y || x = y
let predicate (>=) (x y : int) = y <= x
meta "inline:no" function (-)
meta "inline:no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
clone export algebra.OrderedUnitaryCommutativeRing with
type t = int, constant zero = zero, constant one = one,
function (-_) = (-_), function (+) = (+),
......@@ -316,47 +321,60 @@ module NumOf
(** number of `n` such that `a <= n < b` and `p n` *)
let rec function numof (p: int -> bool) (a b: int) : int
variant { b - a }
= if b <= a then 0 else
if p (b - 1) then 1 + numof p a (b - 1)
else numof p a (b - 1)
= if a >= b then 0 else
if p a then 1 + numof p (a + 1) b
else numof p (a + 1) b
lemma Numof_bounds :
lemma numof_bounds:
forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
(* direct when a>=b, by induction on b when a <= b *)
(* direct when a>=b, by induction on a when a <= b *)
lemma Numof_append :
lemma numof_append:
forall p : int -> bool, a b c : int.
a <= b <= c -> numof p a c = numof p a b + numof p b c
(* by induction on c *)
(* by induction on a *)
lemma Numof_left_no_add :
forall p : int -> bool, a b : int.
a < b -> not p a -> numof p a b = numof p (a+1) b
(* by Numof_append *)
lemma Numof_left_add :
forall p : int -> bool, a b : int.
a < b -> p a -> numof p a b = 1 + numof p (a+1) b
(* by Numof_append *)
lemma numof_right:
forall p : int -> bool, a b : int. a <= b ->
if p b then numof p a (b + 1) = numof p a b + 1
else numof p a (b + 1) = numof p a b
(* by numof_append *)
lemma Empty :
lemma numof_empty:
forall p : int -> bool, a b : int.
(forall n : int. a <= n < b -> not p n) -> numof p a b = 0
(forall n : int. a <= n < b -> not p n) <-> numof p a b = 0
(* by induction on b *)
lemma Full :
lemma numof_full:
forall p : int -> bool, a b : int. a <= b ->
(forall n : int. a <= n < b -> p n) -> numof p a b = b - a
(forall n : int. a <= n < b -> p n) <-> numof p a b = b - a
(* by induction on b *)
lemma numof_increasing:
lemma numof_nonempty:
forall p : int -> bool, a b.
numof p a b > 0 <-> exists i. a <= i < b /\ p i
(*
lemma numof_increasing_right:
forall p : int -> bool, i j k : int.
i <= j <= k -> numof p i j <= numof p i k
(* by Numof_append and Numof_non_negative *)
(* by numof_append and numof_bounds *)
lemma numof_increasing_left:
forall p : int -> bool, i j k : int.
k <= i <= j -> numof p i j <= numof p k j
(* by numof_append and numof_bounds *)
lemma numof_strictly_increasing:
lemma numof_strictly_increasing_right:
forall p: int -> bool, i j k l: int.
i <= j <= k < l -> p k -> numof p i j < numof p i l
(* by Numof_append and numof_increasing *)
(* by numof_append and numof_increasing *)
lemma numof_strictly_increasing_left:
forall p: int -> bool, i j k l: int.
l <= k < i <= j -> p k -> numof p i j < numof p l j
(* by numof_append and numof_increasing *)
*)
lemma numof_change_any:
forall p1 p2: int -> bool, a b: int.
......@@ -385,11 +403,19 @@ module Sum
(** sum of `f n` for `a <= n < b` *)
let rec function sum (f: int -> int) (a b: int) : int
variant { b - a }
= if b <= a then 0 else sum f a (b - 1) + f (b - 1)
= if a < b then f a + sum f (a + 1) b else 0
lemma sum_left:
forall f: int -> int, a b: int.
a < b -> sum f a b = f a + sum f (a + 1) b