Commit 3a9ea01e authored by Andrei Paskevich's avatar Andrei Paskevich

Matrix: add the pure "update" function for applicative updates

parent 05648746
......@@ -19,21 +19,21 @@ module BinarySort
use array.Array
use array.ArrayPermut
let lemma occ_shift (m1 m2: M.map int 'a) (mid k: int) (x: 'a) : unit
let lemma occ_shift (m1 m2: int -> 'a) (mid k: int) (x: 'a) : unit
requires { 0 <= mid <= k }
requires { forall i. mid < i <= k -> M.get m2 i = M.get m1 (i - 1) }
requires { M.get m2 mid = M.get m1 k }
requires { forall i. mid < i <= k -> m2 i = m1 (i - 1) }
requires { m2 mid = m1 k }
ensures { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1) }
= for i = mid to Int.(-) k 1 do
= for i = mid to k - 1 do
invariant { M.Occ.occ x m1 mid i = M.Occ.occ x m2 (mid+1) (i+1) }
()
done;
assert { M.Occ.occ (M.get m1 k) m1 mid (k+1) =
1 + M.Occ.occ (M.get m1 k) m1 mid k };
assert { M.Occ.occ (M.get m1 k) m2 mid (k+1) =
1 + M.Occ.occ (M.get m1 k) m2 (mid+1) (k+1) };
assert { M.Occ.occ (m1 k) m1 mid (k+1) =
1 + M.Occ.occ (m1 k) m1 mid k };
assert { M.Occ.occ (m1 k) m2 mid (k+1) =
1 + M.Occ.occ (m1 k) m2 (mid+1) (k+1) };
assert { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1)
by x = M.get m1 k \/ x <> M.get m1 k }
by x = m1 k \/ x <> m1 k }
let binary_sort (a: array int) : unit
ensures { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
......
......@@ -23,21 +23,21 @@ module M
(* interp x i j is the integer X[j-1]...X[i] *)
function interp (M.map int int) int int : int
function interp (int -> int) int int : int
axiom Interp_1 :
forall x : M.map int int, i j : int.
forall x : int -> int, i j : int.
i >= j -> interp x i j = 0
axiom Interp_2 :
forall x : M.map int int, i j : int.
i < j -> interp x i j = M.get x i + 10 * interp x (i+1) j
forall x : int -> int, i j : int.
i < j -> interp x i j = x i + 10 * interp x (i+1) j
(* to allow provers to prove that an assignment does not change the
interpretation on the left (or on the right); requires induction *)
let rec lemma interp_eq
(x1 x2 : M.map int int) (i j : int)
requires { forall k : int. i <= k < j -> M.get x1 k = M.get x2 k }
(x1 x2 : int -> int) (i j : int)
requires { forall k : int. i <= k < j -> x1 k = x2 k }
ensures { interp x1 i j = interp x2 i j }
variant { j - i }
= if i < j then interp_eq x1 x2 (i+1) j
......@@ -45,26 +45,26 @@ module M
(* the sum of the elements of x[i..j[ *)
use int.Sum
function sum (m: M.map int int) (i j: int) : int =
Sum.sum (fun k -> M.get m k) i (j - 1)
function sum (m: int -> int) (i j: int) : int =
Sum.sum m i (j - 1)
lemma Sum_is_sum_digits_interp:
forall x : M.map int int, i j : int.
forall x : int -> int, i j : int.
sum x i j = sum_digits (interp x i j)
lemma Sum_digits_a_set_eq:
forall x : array int, i j k v : int.
(k < i \/ k >= j) -> sum (M.set x.elts k v) i j = sum x.elts i j
(k < i \/ k >= j) -> sum (Map.set x.elts k v) i j = sum x.elts i j
(* interp9 X i j is the j-digit integer obtained by replacing the i least
significant digits in X by 9, i.e. X[j-1]...X[i]9...9 *)
function interp9 (x : M.map int int) (i j : int) : int =
function interp9 (x : int -> int) (i j : int) : int =
power 10 i * (interp x i j + 1) - 1
lemma Interp9_step:
forall x : M.map int int, i j : int.
i < j -> interp9 (M.set x i 9) i j = interp9 x (i+1) j
forall x : int -> int, i j : int.
i < j -> interp9 (Map.set x i 9) i j = interp9 x (i+1) j
val x : array int
......@@ -115,8 +115,8 @@ let search_safety ()
with digit sum y *)
(* x[0..m-1] is a well-formed integer i.e. has digits in 0..9 *)
predicate is_integer (x : M.map int int) =
forall k : int. 0 <= k < m -> 0 <= M.get x k <= 9
predicate is_integer (x : int -> int) =
forall k : int. 0 <= k < m -> 0 <= x k <= 9
let search ()
requires { length x = m /\ is_integer x.elts }
......@@ -163,18 +163,18 @@ let search ()
4. Completeness: we always raise the Success exception *)
(* x1 > x2 since x1[d] > x2[d] and x1[d+1..m-1] = x2[d+1..m-1] *)
predicate gt_digit (x1 x2 : M.map int int) (d : int) =
predicate gt_digit (x1 x2 : int -> int) (d : int) =
is_integer x1 /\ is_integer x2 /\ 0 <= d < m /\
M.get x1 d > M.get x2 d /\ forall k : int. d < k < m -> M.get x1 k = M.get x2 k
x1 d > x2 d /\ forall k : int. d < k < m -> x1 k = x2 k
lemma Gt_digit_interp:
forall x1 x2 : M.map int int, d : int.
forall x1 x2 : int -> int, d : int.
gt_digit x1 x2 d -> interp x1 0 m > interp x2 0 m
lemma Gt_digit_update:
forall x1 x2 : M.map int int, d i v : int.
forall x1 x2 : int -> int, d i v : int.
gt_digit x1 x2 d -> 0 <= i < d -> 0 <= v <= 9 ->
gt_digit (M.set x1 i v) x2 d
gt_digit (Map.set x1 i v) x2 d
(* the number of digits of a given integer *)
function nb_digits int : int
......@@ -188,7 +188,7 @@ let search ()
(* the smallest integer with digit sum y is (y mod 9)9..9
with exactly floor(y/9) trailing 9s *)
function smallest int : M.map int int
function smallest int : int -> int
function smallest_size int : int
......@@ -202,7 +202,7 @@ let search ()
(* smallest(y) is an integer *)
axiom Smallest_def1:
forall y : int. y >= 0 ->
forall k : int. 0 <= k < smallest_size y -> 0 <= M.get (smallest y) k <= 9
forall k : int. 0 <= k < smallest_size y -> 0 <= smallest y k <= 9
(* smallest(y) has digit sum y *)
axiom Smallest_def2:
......@@ -217,12 +217,12 @@ let search ()
lemma Smallest_shape_1:
forall y : int. y >= 0 -> mod y 9 = 0 ->
forall k : int. 0 <= k < smallest_size y -> M.get (smallest y) k = 9
forall k : int. 0 <= k < smallest_size y -> smallest y k = 9
lemma Smallest_shape_2:
forall y : int. y >= 0 -> mod y 9 <> 0 ->
(forall k : int. 0 <= k < smallest_size y - 1 -> M.get (smallest y) k = 9) /\
M.get (smallest y) (smallest_size y - 1) = mod y 9
(forall k : int. 0 <= k < smallest_size y - 1 -> smallest y k = 9) /\
smallest y (smallest_size y - 1) = mod y 9
lemma Smallest_nb_digits:
forall y : int. y >= 0 ->
......@@ -265,7 +265,7 @@ let search_smallest ()
x = old x /\
forall c' : int. x[d] < c' < c ->
forall u : int.
interp (old x.elts) 0 m < u <= interp9 (M.set x.elts d c') d m ->
interp (old x.elts) 0 m < u <= interp9 (Map.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
......@@ -281,7 +281,7 @@ let search_smallest ()
sum x.elts d m = y - delta /\
sum x.elts 0 i = (if i <= k then 9*i else delta) /\
(forall j : int. 0 <= j < i ->
(j < smallest_size delta -> x[j] = M.get (smallest delta) j) /\
(j < smallest_size delta -> x[j] = smallest delta j) /\
(j >= smallest_size delta -> x[j] = 0)) /\
gt_digit x.elts (old x.elts) d }
if i < k then x[i] <- 9
......
......@@ -24,8 +24,8 @@ module InverseInPlace
let function (~_) (x: int) : int = -x-1
function numof (m: M.map int int) (l r: int) : int =
NumOf.numof (fun n -> M.([]) m n >= 0) l r
function numof (m: int -> int) (l r: int) : int =
NumOf.numof (fun n -> m n >= 0) l r
predicate is_permutation (a: array int) =
forall i: int. 0 <= i < length a ->
......
......@@ -76,7 +76,7 @@ function make (len: int) (dummy: 'a) : rarray 'a =
let ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < r.length }
ensures { r.data.A.elts = A.M.([<-]) (old r).data.A.elts i v }
ensures { r.data.A.elts = A.Map.([<-]) (old r).data.A.elts i v }
=
A.([]<-) r.data i v
......
......@@ -12,11 +12,11 @@ use array.Array
use array.IntArraySorted
use abstract_heap.AbstractHeap
let rec lemma min_of_sorted (a:M.map int int) (i n :int)
let rec lemma min_of_sorted (a: int -> int) (i n: int)
requires { 0 <= i < n }
requires { M.sorted_sub a 0 n }
variant { n }
ensures { min_bag (elements a i n) = M.get a i }
ensures { min_bag (elements a i n) = a i }
= if n > 0 && i < n - 1 then min_of_sorted a i (n-1)
(* heap sort *)
......
......@@ -10,7 +10,7 @@ modification of an array does not modify its length.
module Array
use int.Int
use map.Map as M
use map.Map
type array 'a = private {
mutable ghost elts : int -> 'a;
......@@ -25,11 +25,11 @@ module Array
val ghost function ([<-]) (a: array 'a) (i: int) (v: 'a): array 'a
ensures { result.length = a.length }
ensures { result.elts = M.set a.elts i v }
ensures { result.elts = Map.set a.elts i v }
val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = M.set (old a).elts i v }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = (old a)[i <- v] }
(** unsafe get/set operations with no precondition *)
......
......@@ -3,7 +3,7 @@
module Matrix
use int.Int
use map.Map as M
use map.Map
type matrix 'a = private {
ghost mutable elts: int -> int -> 'a;
......@@ -14,14 +14,22 @@ module Matrix
predicate valid_index (a: matrix 'a) (r c: int) =
0 <= r < a.rows /\ 0 <= c < a.columns
val function get (a: matrix 'a) (r c: int) : 'a
function get (a: matrix 'a) (r c: int) : 'a =
a.elts r c
val get (a: matrix 'a) (r c: int) : 'a
requires { [@expl:index in matrix bounds] valid_index a r c }
ensures { result = a.elts r c }
val ghost function update (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a
ensures { result.rows = a.rows }
ensures { result.columns = a.columns }
ensures { result.elts = a.elts[r <- (a.elts r)[c <- v]] }
val set (a: matrix 'a) (r c: int) (v: 'a) : unit
requires { [@expl:index in matrix bounds] valid_index a r c }
writes { a }
ensures { a.elts = M.((old a.elts)[r <- (old a.elts r)[c <- v]]) }
ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
(** unsafe get/set operations with no precondition *)
......@@ -36,7 +44,7 @@ module Matrix
let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
ensures { [@expl:index in matrix bounds] valid_index a r c }
ensures { a.elts = M.((old a.elts)[r <- (old a.elts r)[c <- v]]) }
ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a r c v
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment