Commit 2839e902 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix syntax of some examples.

parent d747d923
......@@ -79,7 +79,7 @@ module Check
let is_dyck (w: word) : bool
ensures { result <-> dyck w }
=
try match is_dyck_rec (ref Nil) w with
try match is_dyck_rec (ghost ref Nil) w with
| Nil -> true
| _ -> false
end with Failure -> false end
......
......@@ -40,28 +40,28 @@ module FIND
let find (a: array int) =
requires { length a = _N+1 }
ensures { found a /\ permut_all a (old a) }
'Init:
let m = ref 1 in let n = ref _N in
while !m < !n do
invariant { m_invariant !m a /\ n_invariant !n a /\
permut_all a (at a 'Init) /\ 1 <= !m /\ !n <= _N }
permut_all a (old a) /\ 1 <= !m /\ !n <= _N }
variant { !n - !m }
let r = a[f] in let i = ref !m in let j = ref !n in
while !i <= !j do
invariant { i_invariant !m !n !i r a /\ j_invariant !m !n !j r a /\
m_invariant !m a /\ n_invariant !n a /\ 0 <= !j /\ !i <= _N + 1 /\
termination !i !j !m !n r a /\ permut_all a (at a 'Init) }
termination !i !j !m !n r a /\ permut_all a (old a) }
variant { _N + 2 + !j - !i }
'L: while a[!i] < r do
label L in
while a[!i] < r do
invariant { i_invariant !m !n !i r a /\
at !i 'L <= !i <= !n /\ termination !i !j !m !n r a }
!i at L <= !i <= !n /\ termination !i !j !m !n r a }
variant { _N + 1 - !i }
i := !i + 1
done;
while r < a[!j] do
invariant { j_invariant !m !n !j r a /\
!j <= at !j 'L /\ !m <= !j /\ termination !i !j !m !n r a }
!j <= !j at L /\ !m <= !j /\ termination !i !j !m !n r a }
variant { !j }
j := !j - 1
done;
......@@ -70,7 +70,7 @@ module FIND
if !i <= !j then begin
let w = a[!i] in begin a[!i] <- a[!j]; a[!j] <- w end;
assert { exchange a (at a 'L) !i !j };
assert { exchange a (a at L) !i !j };
assert { a[!i] <= r }; assert { r <= a[!j] };
i := !i + 1;
j := !j - 1
......
......@@ -33,13 +33,12 @@ module Flag
let b = ref 0 in
let i = ref 0 in
let r = ref (length a) in
'Init:
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= length a }
invariant { monochrome a 0 !b Blue }
invariant { monochrome a !b !i White }
invariant { monochrome a !r (length a) Red }
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
variant { !r - !i }
match a[!i] with
| Blue ->
......
......@@ -80,24 +80,23 @@ module Flag
a := set !a j ai
let dutch_flag (a:ref (map int color)) (n:int) =
let dutch_flag (a:ref (map int color)) (n:int)
requires { 0 <= n }
ensures { (exists b:int. exists r:int.
monochrome !a 0 b Blue /\
monochrome !a b r White /\
monochrome !a r n Red) }
ensures { forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
let b = ref 0 in
= let b = ref 0 in
let i = ref 0 in
let r = ref n in
'Init:
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= n }
invariant { monochrome !a 0 !b Blue }
invariant { monochrome !a !b !i White }
invariant { monochrome !a !r n Red }
invariant {
forall c:color. nb_occ !a 0 n c = nb_occ (at !a 'Init) 0 n c }
forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
variant { !r - !i }
match get !a !i with
| Blue -> swap a !b !i; b := !b + 1; i := !i + 1
......
......@@ -55,7 +55,7 @@ module Utils_Spec
lemma countZero: count zeros = zeros
lemma numOfZero: NumOf.numof (\i. nth zeros i) 0 32 = 0
lemma numOfZero: NumOf.numof (fun i -> nth zeros i) 0 32 = 0
(** Now, for b a bitvector with n 1-bits, we check that if its
first bit is 0 then shifting b by one on the right doesn't
......@@ -86,7 +86,7 @@ module Utils_Spec
let x = (if nth_bv bv zeros then 1 else 0) in
let f = nth bv in
let g = nth (lsr_bv bv one) in
let h = \i. nth bv (i+1) in
let h = fun i -> nth bv (i+1) in
(forall i. 0 <= i < 31 -> g i = h i) &&
NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 &&
NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 &&
......@@ -117,7 +117,7 @@ module Utils_Spec
lemma separation: forall a b. hammingD a b = zeros <-> a = b
function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
function fun_or (f g : 'a -> bool) : 'a -> bool = fun x -> f x \/ g x
let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
variant {b - a}
......
......@@ -272,16 +272,16 @@ module N
value_sub x.elts 0 (to_int !i) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int l - to_int !i }
'L:
label L in
let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
if Int31.(>=) sum base31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else begin arr[!i] <- sum; carry := zero end;
if Int31.ne arr[!i] zero then non_null_idx := !i;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
i := Int31.(+) !i one;
done;
while Int31.(<) !i h do
......@@ -300,24 +300,24 @@ module N
value_sub x.elts 0 (to_int l) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int h - to_int !i }
'L:
label L in
let sum = Int31.(+) y[!i] !carry in
if Int31.(>=) sum base31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else begin arr[!i] <- sum; carry := zero end;
if Int31.ne arr[!i] zero then non_null_idx := !i;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
i := Int31.(+) !i one;
done;
'L:
label L in
arr[!i] <- !carry;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
assert { value_array arr = value_array x + value_array y };
abstract
ensures { -1 <= to_int !non_null_idx <= to_int !i }
......@@ -547,7 +547,7 @@ module Z
value_sub x.elts 0 (to_int !i) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int l - to_int !i }
'L:
label L in
let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
if Int31.(>=) sum max_digit31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
......@@ -556,9 +556,9 @@ module Z
then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
else begin arr[!i] <- sum; carry := zero end;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
i := Int31.(+) !i one;
done;
while Int31.(<) !i h do
......@@ -572,7 +572,7 @@ module Z
value_sub x.elts 0 (to_int l) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int h - to_int !i }
'L:
label L in
let sum = Int31.(+) y[!i] !carry in
if Int31.(>=) sum max_digit31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
......@@ -581,17 +581,17 @@ module Z
then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
else begin arr[!i] <- sum; carry := zero end;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
i := Int31.(+) !i one;
done;
'L:
label L in
arr[!i] <- !carry;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
arr
let add (x y:t) : t
......
......@@ -58,20 +58,20 @@ constant p2 : term =
(Lambda y (Var y)))
(Lambda x (Var x))
predicate ground_rec (t:term) (bound: H.pred identifier) =
predicate ground_rec (t:term) (bound: identifier -> bool) =
match t with
| Var v -> bound v
| App t1 t2 -> ground_rec t1 bound /\ ground_rec t2 bound
| Lambda x t -> ground_rec t (\v. v=x \/ bound v)
end
let lemma ground_rec_app (t1 t2 : term) (bound: H.pred identifier)
let lemma ground_rec_app (t1 t2 : term) (bound: identifier -> bool)
requires { ground_rec (App t1 t2) bound }
ensures { ground_rec t1 bound }
ensures { ground_rec t2 bound }
= ()
function no_bound : H.pred identifier = (\x. false)
function no_bound : identifier -> bool = fun x -> false
predicate ground (t:term) = ground_rec t no_bound
......
......@@ -6,11 +6,11 @@ module String
type char
constant dummy_char: char
type string = { length: int; chars: HO.func int char }
type string = { length: int; chars: int -> char }
function ([]) (s: string) (i: int) : char = s.chars i
constant empty : string = { length = 0; chars = \ i: int. dummy_char }
constant empty : string = { length = 0; chars = fun (i: int) -> dummy_char }
val get (s: string) (i:int) : char
requires { 0 <= i < s.length }
......@@ -18,11 +18,11 @@ module String
function app (s1 s2: string) : string =
{ length = s1.length + s2.length;
chars = \ i: int.
chars = fun i ->
if i < s1.length then s1.chars i else s2.chars (i - s1.length) }
function sub (s: string) (ofs: int) (len: int) : string =
{ length = len; chars = \ i: int. s.chars (i - ofs) }
{ length = len; chars = fun i -> s.chars (i - ofs) }
predicate (==) (s1 s2: string) =
s1.length = s2.length /\
......
......@@ -334,11 +334,10 @@ module M2
ensures { reverse (model (old !next) (old !p)) = model !next !result }
= let old_p = !p in
let q = ref null in
'Init:
while !p <> null do
invariant { is_list !next !p /\ is_list !next !q }
invariant { sep_list_list !next !p !q }
invariant { reverse (model (at !next 'Init) (old_p)) =
invariant { reverse (model (old !next) (old_p)) =
reverse (model !next !p) ++ model !next !q }
variant { model !next !p }
let tmp = !next[!p] in
......
......@@ -147,15 +147,14 @@ module N
ensures { MapEq.map_eq_sub x.digits.elts (Const.const Limb.zero_unsigned)
(p2i (old x).digits.length) (p2i l) }
ensures { value x = value (old x) }
= 'Init:
let limb_zero = Limb.of_int 0 in
= let limb_zero = Limb.of_int 0 in
let zero = Int31.of_int 0 in
let lx = x.digits.length in
let r = Array31.make l limb_zero in
assert { MapEq.map_eq_sub r.elts (Const.const limb_zero) (p2i lx) (p2i l) };
Array31.blit x.digits zero r zero lx;
assert { MapEq.map_eq_sub x.digits.elts r.elts 0 (p2i lx) };
assert { value_sub x.digits.elts 0 (p2i lx) = value (at x 'Init) };
assert { value_sub x.digits.elts 0 (p2i lx) = value (old x) };
assert { MapEq.map_eq_sub r.elts (Const.const limb_zero) (p2i lx) (p2i l) };
assert { value_sub r.elts (p2i lx) (p2i l) = 0 };
assert { value_sub r.elts 0 (p2i l) = value_sub r.elts 0 (p2i lx)
......@@ -287,24 +286,23 @@ module N
ensures { forall j. 0 <= j < p2i x1 \/ p2i x2 <= j < p2i x.length -> x[j] = (old x)[j] }
ensures { value_array x + power radix (p2i x2) * l2i result
= value_array (old x) + power radix (p2i x1) * l2i y }
= 'Init:
let limb_zero = Limb.of_int 0 in
= let limb_zero = Limb.of_int 0 in
let one = Int31.of_int 1 in
let i = ref x1 in
let c = ref y in
while Int31.(<) !i x2 && Limb.ne !c limb_zero do
invariant { forall j. 0 <= j < p2i x1 \/ p2i x2 <= j < p2i x.length ->
x[j] = (at x 'Init)[j] }
x[j] = (old x)[j] }
invariant { p2i x1 <= p2i !i <= p2i x2 }
invariant {
value_array x + power radix (p2i !i) * l2i !c =
value_array (at x 'Init) + power radix (p2i x1) * l2i y }
value_array (old x) + power radix (p2i x1) * l2i y }
variant { p2i x2 - p2i !i }
let (r,c') = Limb.add_with_carry x[!i] !c limb_zero in
'L:
label L in
x[!i] <- r;
assert { value_array x = value_array (at x 'L)
+ power radix (p2i !i) * (l2i r - l2i (at x 'L)[p2i !i]) };
assert { value_array x = value_array (x at L)
+ power radix (p2i !i) * (l2i r - l2i (x at L)[p2i !i]) };
c := c';
i := Int31.(+) !i one;
done;
......@@ -320,28 +318,27 @@ module N
value_array x + power radix (p2i x2) * l2i result
= value_array (old x) +
power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i y2) }
= 'Init:
let limb_zero = Limb.of_int 0 in
= let limb_zero = Limb.of_int 0 in
let one = Int31.of_int 1 in
let i = ref y1 in
let c = ref limb_zero in
while Int31.(<) !i y2 do
invariant { forall j. 0 <= j < p2i x1 \/ p2i x2 <= j < p2i x.length ->
x[j] = (at x 'Init)[j] }
x[j] = (old x)[j] }
invariant { p2i y1 <= p2i !i <= p2i y2 }
invariant {
let j = p2i x1 + (p2i !i - p2i y1) in
value_array x + power radix j * l2i !c
= value_array (at x 'Init) +
= value_array (old x) +
power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) }
invariant { 0 <= l2i !c <= 1 }
variant { p2i y2 - p2i !i }
let j = Int31.(+) x1 (Int31.(-) !i y1) in
let (r,c') = Limb.add_with_carry x[j] y[!i] !c in
'L:
label L in
x[j] <- r;
assert { value_array x = value_array (at x 'L)
+ power radix (p2i j) * (l2i r - l2i (at x 'L)[p2i j]) };
assert { value_array x = value_array (x at L)
+ power radix (p2i j) * (l2i r - l2i (x at L)[p2i j]) };
assert { value_sub y.elts (p2i y1) (p2i !i + 1) =
value_sub y.elts (p2i y1) (p2i !i)
+ power radix (p2i !i - p2i y1) * l2i y[p2i !i] };
......@@ -360,24 +357,23 @@ module N
writes { x.digits, x.digits.elts }
ensures { value x = value (old x) + value_array y }
raises { TooManyDigits -> true }
= 'Init:
let zero = Int31.of_int 0 in
= let zero = Int31.of_int 0 in
let one = Int31.of_int 1 in
let limb_zero = Limb.of_int 0 in
let lx = x.digits.length in
let c = add_limbs x.digits y zero lx zero y.length in
assert {
value x + power radix (p2i lx) * l2i c =
value (at x 'Init) + value_array y };
value (old x) + value_array y };
if Limb.eq c limb_zero then () else
begin
(* we enlarge x *)
if Int31.eq lx (of_int 0x3FFFFFFF) then raise TooManyDigits;
'L:
label L in
enlarge x (Int31.(+) lx one);
assert { l2i x.digits[p2i lx] = 0 };
x.digits[lx] <- c;
assert { value x = value_array (at x.digits 'L) + power radix (p2i lx) * l2i c };
assert { value x = value_array (x.digits at L) + power radix (p2i lx) * l2i c };
end
let add_in_place (x y:t) : unit
......@@ -409,10 +405,10 @@ module N
let c = add_limbs r y zero lx zero y.length in
assert {
value_array r + power radix (p2i lx) * l2i c = value_array x + value_array y };
'L:
label L in
assert { l2i r[p2i lx] = 0 };
r[lx] <- c;
assert { value_array r = value_array (at r 'L) + power radix (p2i lx) * l2i c };
assert { value_array r = value_array (r at L) + power radix (p2i lx) * l2i c };
r
let add (x y:t) : t
......@@ -436,28 +432,27 @@ module N
ensures { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i z.length -> z[j] = (old z)[j] }
ensures { value_array z + power radix (p2i z1 + (p2i x2 - p2i x1)) * l2i result
= value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * l2i y) }
= 'Init:
let limb_zero = Limb.of_int 0 in
= let limb_zero = Limb.of_int 0 in
let one = Int31.of_int 1 in
let i = ref x1 in
let c = ref limb_zero in
while Int31.(<) !i x2 do
invariant { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i z.length ->
z[j] = (at z 'Init)[j] }
z[j] = (old z)[j] }
invariant { p2i x1 <= p2i !i <= p2i x2 }
invariant {
value_array z + power radix (p2i z1 + (p2i !i - p2i x1)) * l2i !c =
value_array (at z 'Init) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i !i) * l2i y) }
value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i !i) * l2i y) }
variant { p2i x2 - p2i !i }
let (rl,rh) = Limb.mul_double x[!i] y in
let j = Int31.(+) z1 (Int31.(-) !i x1) in
let (v,c') = Limb.add3 z[j] rl !c in
assert { 0 <= l2i z[p2i j] + l2i !c + l2i x[p2i !i] * l2i y <= radix * radix - 1 };
assert { l2i v + radix * (l2i rh + l2i c') = l2i z[p2i j] + l2i !c + l2i x[p2i !i] * l2i y };
'L:
label L in
z[j] <- v;
assert { value_array z = value_array (at z 'L)
+ power radix (p2i z1 + (p2i !i - p2i x1)) * (l2i v - l2i (at z 'L)[p2i z1 + (p2i !i - p2i x1)]) };
assert { value_array z = value_array (z at L)
+ power radix (p2i z1 + (p2i !i - p2i x1)) * (l2i v - l2i (z at L)[p2i z1 + (p2i !i - p2i x1)]) };
c := Limb.(+) rh c';
i := Int31.(+) !i one;
done;
......@@ -474,18 +469,17 @@ module N
x[j] = (old x)[j] }
ensures { value_array z + power radix (p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1)) * l2i result
= value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * value_sub y.elts (p2i y1) (p2i y2)) }
= 'Init:
let limb_zero = Limb.of_int 0 in
= let limb_zero = Limb.of_int 0 in
let one = Int31.of_int 1 in
let c = ref limb_zero in
let i = ref y1 in
while Int31.(<) !i y2 do
invariant { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1) <= j < p2i z.length ->
z[j] = (at z 'Init)[j] }
z[j] = (old z)[j] }
invariant { p2i y1 <= p2i !i <= p2i y2 }
invariant {
value_array z + power radix (p2i z1 + (p2i x2 - p2i x1) + (p2i !i - p2i y1)) * l2i !c =
value_array (at z 'Init) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * value_sub y.elts (p2i y1) (p2i !i)) }
value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * value_sub y.elts (p2i y1) (p2i !i)) }
invariant { 0 <= l2i !c <= 1 }
variant { p2i y2 - p2i !i }
let j = Int31.(+) z1 (Int31.(-) !i y1) in
......
......@@ -46,7 +46,7 @@ module M
use int.Sum
function sum (m: M.map int int) (i j: int) : int =
Sum.sum i (j - 1) (\ k: int. M.get m k)
Sum.sum (fun k -> M.get m k) i (j - 1)
lemma Sum_is_sum_digits_interp:
forall x : M.map int int, i j : int.
......@@ -87,8 +87,7 @@ let search_safety ()
requires { length x = m }
ensures { true }
raises { Success -> true }
= 'Init:
let s = ref 0 in
= let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
s := !s + x[i]
done;
......@@ -123,8 +122,7 @@ let search ()
requires { length x = m /\ is_integer x.elts }
ensures { true }
raises { Success -> is_integer x.elts /\ sum x.elts 0 m = y }
= 'Init:
let s = ref 0 in
= let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
invariant { !s = sum x.elts 0 i }
s := !s + x[i]
......@@ -132,11 +130,11 @@ let search ()
assert { !s = sum x.elts 0 m };
for d = 0 to m - 1 do
invariant {
x = at x 'Init /\
x = old x /\
!s = sum x.elts d m
}
for c = x[d] + 1 to 9 do
invariant { x = at x 'Init }
invariant { x = old x }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
x[d] <- c;
......@@ -249,8 +247,7 @@ let search_smallest ()
interp x.elts 0 m > interp (old x.elts) 0 m /\
forall u : int. interp (old x.elts) 0 m < u < interp x.elts 0 m ->
sum_digits u <> y }
= 'Init:
let s = ref 0 in
= let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
invariant { !s = sum x.elts 0 i }
s := !s + x[i]
......@@ -258,24 +255,24 @@ let search_smallest ()
assert { !s = sum x.elts 0 m };
for d = 0 to m - 1 do
invariant {
x = at x 'Init /\
x = old x /\
!s = sum x.elts d m /\
forall u : int.
interp (at x.elts 'Init) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
interp (old x.elts) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
}
for c = x[d] + 1 to 9 do
invariant {
x = at x 'Init /\
x = old x /\
forall c' : int. x[d] < c' < c ->
forall u : int.
interp (at x.elts 'Init) 0 m < u <= interp9 (M.set x.elts d c') d m ->
interp (old x.elts) 0 m < u <= interp9 (M.set x.elts d c') d m ->
sum_digits u <> y }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
assert { smallest_size delta <= d };
x[d] <- c;
assert { sum x.elts d m = y - delta };
assert { gt_digit x.elts (at x.elts 'Init) d };
assert { gt_digit x.elts (old x.elts) d };
let k = div delta 9 in
assert { k <= d };
for i = 0 to d - 1 do
......@@ -286,7 +283,7 @@ let search_smallest ()
(forall j : int. 0 <= j < i ->
(j < smallest_size delta -> x[j] = M.get (smallest delta) j) /\
(j >= smallest_size delta -> x[j] = 0)) /\
gt_digit x.elts (at x.elts 'Init) d }
gt_digit x.elts (old x.elts) d }
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0;
......
......@@ -575,15 +575,15 @@ this is true but with 2 different possible reasons:
end
else
begin
'L:
label L in
let k = ref n1 in
while Int31.(<=) !k n9 do
invariant { 1 <= t !k <= 10 }
invariant { grid_eq (at g 'L).elts (Map.set g.elts (t i) n0) }
invariant { grid_eq (g at L).elts (Map.set g.elts (t i) n0) }
invariant { full_up_to g.elts (t i) }
invariant { (* for completeness *)
forall k'. 1 <= t k' < t !k ->
let g' = Map.set (at g 'L).elts (t i) k' in
let g' = Map.set (g at L).elts (t i) k' in
forall h : grid. included g' h /\ full h -> not (valid s h) }
variant { 9 - t !k }
g[i] <- !k;
......@@ -592,7 +592,7 @@ this is true but with 2 different possible reasons:
check_valid_chunk g i s.row_start s.row_offsets;
check_valid_chunk g i s.square_start s.square_offsets;
(* the hard part: see lemma valid_up_to_change *)
assert { let grid' = Map.set (at g 'L).elts (t i) !k in
assert { let grid' = Map.set (g at L).elts (t i) !k in
grid_eq grid' g.elts &&
valid_chunk grid' (t i) s.column_start s.column_offsets &&
valid_chunk grid' (t i) s.row_start s.row_offsets &&
......@@ -602,22 +602,22 @@ this is true but with 2 different possible reasons:
solve_aux s g (Int31.(+) i n1)
with Invalid ->
assert {
grid_eq g.elts (Map.set (at g 'L).elts (t i) !k) };
grid_eq g.elts (Map.set (g at L).elts (t i) !k) };
assert { (* for completeness *)
not (valid s g.elts) };
assert { (* for completeness *)
not (valid s (Map.set (at g 'L).elts (t i) !k)) };
not (valid s (Map.set (g at L).elts (t i) !k)) };
assert { (* for completeness *)
let g' = Map.set (at g 'L).elts (t i) !k in
let g' = Map.set (g at L).elts (t i) !k in
forall h : grid. included g' h /\ full h -> not (valid s h) }
end;
k := Int31.(+) !k n1;
done;
g[i] <- n0;
assert { (* for completeness *)
forall h:grid. included (at g 'L).elts h /\ full h ->
forall h:grid. included (g at L).elts h /\ full h ->
let k' = Map.get h (t i) in
let g' = Map.set (at g 'L).elts (t i) k' in
let g' = Map.set (g at L).elts (t i) k' in
included g' h }
end
......
......@@ -10,24 +10,23 @@ module InsertionSort
use import array.ArrayPermut
use import array.ArrayEq
let insertion_sort (a: array int) =
let insertion_sort (a: array int)
ensures { sorted a /\ permut_all (old a) a }
'L:
for i = 1 to length a - 1 do
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a }
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
let j = ref i in
while !j > 0 && a[!j - 1] > v do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'L) a[!j <- v] }
invariant { permut_all (old a) a[!j <- v] }
invariant { forall k1 k2: int.
0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] }
invariant { forall k: int. !j+1 <= k <= i -> v < a[k] }
variant { !j }
'L1:
label L in
a[!j] <- a[!j - 1];
assert { exchange (at a 'L1)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
assert { exchange (a at L)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
j := !j - 1
done;
assert { forall k: int. 0 <= k < !j -> a[k] <= v };
......@@ -85,24 +84,23 @@ module InsertionSortGen
predicate sorted (a : array elt) =
M.sorted_sub a.elts 0 a.length
let insertion_sort (a: array elt) =
let insertion_sort (a: array elt)
ensures { sorted a /\ permut_all (old a) a }
'L:
for i = 1 to length a - 1 do
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a }
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
let j = ref i in
while !j > 0 && not (le a[!j - 1] v) do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'L) a[!j <- v] }
invariant { permut_all (old a) a[!j <- v] }
invariant { forall k1 k2: int.
0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> le a[k1] a[k2] }
invariant { forall k: int. !j+1 <= k <= i -> le v a[k] }
variant { !j }
'L1:
label L in
a[!j] <- a[!j - 1];
assert { exchange (at a 'L1)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
assert { exchange (a at L)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
j := !j - 1
done;
assert { forall k: int. 0 <= k < !j -> le a[k] v };
......
......@@ -19,25 +19,24 @@ module InsertionSortNaive
ensures { sorted a }
ensures { permut_all (old a) a }
=
'Init:
for i = 0 to a.length - 1 do
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub a 0 i }
let j = ref i in
while !j > 0 && a[!j-1] > a[!j] do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub a 0 !j }
invariant { sorted_sub a !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
a[k1] <= a[k2] }
variant { !j }
'L:
label L in
let b = !j - 1 in
let t = a[!j] in
a[!j] <- a[b];
a[b] <- t;
assert { exchange (at a 'L) a (!j-1) !j };
assert { exchange (a at L) a (!j-1) !j };
decr j
done
done
......@@ -72,25 +71,24 @@ module InsertionSortNaiveGen
ensures { sorted a }
ensures { permut_all (old a) a }
=
'Init:
for i = 0 to a.length - 1 do
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub a 0 i }
let j = ref i in
while !j > 0 && not (le a[!j-1] a[!j]) do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub a 0 !j }
invariant { sorted_sub a !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le a[k1] a[k2] }
variant { !j }
'L:
label L in
let b = !j - 1 in
let t = a[!j] in
a[!j] <- a[b];
a[b] <- t;
assert { exchange (at a 'L) a (!j-1) !j };
assert { exchange (a at L) a (!j-1) !j };
decr j
done
done
......@@ -132,25 +130,24 @@ module InsertionSortParam
ensures { sorted p a }
ensures { permut_all (old a) a }
=
'Init:
for i = 0 to a.length - 1 do
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub p a.elts 0 i }
let j = ref i in
while !j > 0 && not (le p a[!j-1] a[!j]) do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub p a.elts 0 !j }
invariant { sorted_sub p a.elts !j (i+1) }
invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
le p a[k1] a[k2] }
variant { !j }
'L:
label L in
let b = !j - 1 in
let t = a[!j] in
a[!j] <- a[b];