 ### Convert some more examples.

parent 4cb75244
 ... ... @@ -84,8 +84,8 @@ module Grid (** {3 Valid Sudoku Solutions} *) (** [valid_chunk g i start offsets] is true whenever the chunk denoted by [start,offsets] from cell [i] is "valid" in grid [g], in (** valid_chunk g i start offsets is true whenever the chunk denoted by start,offsets from cell i is "valid" in grid g, in the sense that it contains at most one occurence of each number between 1 and 9 *) ... ... @@ -107,16 +107,16 @@ module Grid predicate valid_square (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.square_start s.square_offsets (** [valid g] is true when all chunks are valid *) (** valid g is true when all chunks are valid *) predicate valid (s:sudoku_chunks) (g : grid) = forall i : int. is_index i -> valid_column s g i /\ valid_row s g i /\ valid_square s g i (** [full g] is true when all cells are filled *) (** full g is true when all cells are filled *) predicate full (g : grid) = forall i : int. is_index i -> 1 <= Map.get g i <= 9 (** [included g1 g2] *) (** included g1 g2 *) predicate included (g1 g2 : grid) = forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 -> Map.get g2 i = Map.get g1 i ... ... @@ -132,8 +132,8 @@ module Grid forall s g h. well_formed_sudoku s /\ included g h /\ valid s h -> valid s g (** A solution of a grid [data] is a full grid [sol] that is valid and includes [data] *) (** A solution of a grid data is a full grid sol that is valid and includes data *) predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) = included data sol /\ full sol /\ valid s sol ... ... @@ -248,8 +248,8 @@ module Solver use import array.Array (** [check_valid_chunk g i start offsets] checks the validity of the chunk that includes [i] *) (** check_valid_chunk g i start offsets checks the validity of the chunk that includes i *) let check_valid_chunk (g:array int) (i:int) (start:array int) (offsets:array int) : unit requires { g.length = 81 } ... ... @@ -283,8 +283,8 @@ module Solver forall j : int. 0 <= j < i -> valid_column s g j /\ valid_row s g j /\ valid_square s g j (** [check_valid s g] checks if the (possibly partially filled) grid [g] is valid. (This function is not needed by the solver) *) (** check_valid s g checks if the (possibly partially filled) grid g is valid. (This function is not needed by the solver) *) let check_valid (s:sudoku_chunks) (g : array int) : bool requires { well_formed_sudoku s } requires { g.length = 81 } ... ... @@ -302,7 +302,7 @@ module Solver with Invalid -> False end (** [full_up_to g i] is true when all cells [0..i-1] in grid [g] are (** full_up_to g i is true when all cells 0..i-1 in grid g are non empty *) predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= Map.get g j <= 9 ... ... @@ -358,31 +358,31 @@ module Solver (** how to prove the "hard" property : if [valid_up_to s g i] valid_up_to s g i and [h = g[i <- k] (with 1 <= k <= 9)] h = g[i <- k (with 1 <= k <= 9)] and [valid_column s h i /\ valid_row s h i /\ valid_square s h i] valid_column s h i /\ valid_row s h i /\ valid_square s h i then [valid_up_to s h (i+1)] valid_up_to s h (i+1) then the problem is that one should prove that for each [j] in [0..i-1] : then the problem is that one should prove that for each j in 0..i-1 : [valid_column s h j /\ valid_row s h j /\ valid_square s h j] valid_column s h j /\ valid_row s h j /\ valid_square s h j this is true but with 2 different possible reasons: if [column_start j = column_start i] then [valid_column s h j] is true because [valid_column s h i] is true if column_start j = column_start i then valid_column s h j is true because valid_column s h i is true else [valid_column s h j] is true because [valid_column s g j] is true because [valid_column s h j] does not depend on [h[i]] valid_column s h j is true because valid_column s g j is true because valid_column s h j does not depend on h[i] *) ... ...
 ... ... @@ -4,9 +4,9 @@ We are interested in specifying and proving correct data structures that support efficient computation of the sum of the values over an arbitrary range of an array. Concretely, given an array of integers [a], and given a range delimited by indices [i] (inclusive) and [j] (exclusive), we wish to compute the value: [\sum_{k=i}^{j-1} a[k]]. Concretely, given an array of integers a, and given a range delimited by indices i (inclusive) and j (exclusive), we wish to compute the value: \sum_{k=i}^{j-1} a[k]. In the first part, we consider a simple loop for computing the sum in linear time. ... ... @@ -15,7 +15,7 @@ In the second part, we introduce a cumulative sum array that allows answering arbitrary range queries in constant time. In the third part, we explore a tree data structure that supports modification of values from the underlying array [a], supports modification of values from the underlying array a, with logarithmic time operations. *) ... ... @@ -28,23 +28,23 @@ module ArraySum use export int.Int use export array.Array (** [sum a i j] denotes the sum [\sum_{i <= k < j} a[k]]. (** 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 = 0 if [i < j] then [sum a i j = a[i] + sum a (i+1) j] 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 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]] 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. ... ... @@ -63,8 +63,8 @@ module Simple use import ArraySum use import ref.Ref (** [query a i j] returns the sum of elements in [a] between index [i] inclusive and index [j] exclusive *) (** 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 requires { 0 <= i <= j <= a.length } ensures { result = sum a i j } ... ... @@ -80,7 +80,7 @@ end (** {2 Additional lemmas on [sum]} (** {2 Additional lemmas on sum} needed in the remaining code *) module ExtraLemmas ... ... @@ -93,8 +93,8 @@ module ExtraLemmas 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]] *) (** 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 -> ... ... @@ -102,8 +102,8 @@ module ExtraLemmas (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]] *) (** 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] ... ... @@ -135,7 +135,7 @@ module CumulativeArray c.length = a.length + 1 /\ forall i. 0 <= i < c.length -> c[i] = sum a 0 i (** [create a] builds the cumulative array associated with [a]. *) (** 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 ... ... @@ -146,8 +146,8 @@ module CumulativeArray done; s (** [query c i j a] returns the sum of elements in [a] between index [i] inclusive and index [j] exclusive, in constant time *) (** query c i j a returns the sum of elements in a between index i inclusive and index j exclusive, in constant time *) 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 } ... ... @@ -155,8 +155,8 @@ module CumulativeArray = c[j] - c[i] (** [update c i v a] updates cell [a[i]] to value [v] and updates the cumulative array [c] accordingly *) (** 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 requires { is_cumulative_array_for c a } requires { 0 <= i < a.length } ... ... @@ -290,7 +290,7 @@ module CumulativeTree = if i=j then 0 else query_aux t a i j (** frame lemma for predicate [is_tree_for] *) (** 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 -> k < i \/ k >= j -> ... ... @@ -343,10 +343,10 @@ module CumulativeTree (** {2 complexity analysis} We would like to prove that [query] is really logarithmic. This is We would like to prove that query is really logarithmic. This is non-trivial because there are two recursive calls in some cases. So far, we are only able to prove that [update] is logarithmic So far, we are only able to prove that update is logarithmic We express the complexity by passing a credit'' as a ghost parameter. We pose the precondition that the credit is at least ... ... @@ -384,7 +384,7 @@ module CumulativeTree end (** [update_aux] function instrumented with a credit *) (** update_aux function instrumented with a credit *) use import ref.Ref ... ... @@ -419,14 +419,14 @@ module CumulativeTree (Node {ind with isum = ind.isum + delta} l r',delta) (*>*) end (** [query_aux] function instrumented with a credit *) (** query_aux function instrumented with a credit *) let rec query_aux_complexity (t:tree) (ghost a: array int) (i j:int) (ghost c:ref int) : int 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 { !c - old !c <= ensures { !c - old !c <= 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 } ... ...
 ... ... @@ -160,26 +160,26 @@ module HeightSmallSpace (** Count number of leaves in a tree. *) function leaves (t: tree 'a) : int = 1 + size t (** [height_limited acc depth lim t]: Compute the [height t] if the number of leaves in [t] is at most [lim], fails otherwise. [acc] and [depth] are accumulators. (** height_limited acc depth lim t: Compute the height t if the number of leaves in t is at most lim, fails otherwise. acc and depth are accumulators. For maintaining the limit within the recursion, this routine also send back the difference between the number of leaves and the limit in case of success. Method: find out one child with number of leaves at most [lim/2] using Method: find out one child with number of leaves at most lim/2 using recursive calls. If no such child is found, the tree has at least [lim+1] leaves, hence fails. Otherwise, accumulate the result least lim+1 leaves, hence fails. Otherwise, accumulate the result of the recursive call for that child and make a recursive tail-call for the other child, using the computed difference in order to update [lim]. Since non-tail-recursive calls halve the limit, the space complexity is logarithmic in [lim]. update lim. Since non-tail-recursive calls halve the limit, the space complexity is logarithmic in lim. Note that as is, this has a degenerate case: if the small child is extremely small, we may waste a lot of computing time on the large child to notice it is large, while in the end processing only the small child until the tail-recursive call. Analysis shows that this results in super-polynomial time behavior (recursion T(N) = T(N/2)+T(N-1)) To mitigate this, we perform recursive calls on all [lim/2^k] limits To mitigate this, we perform recursive calls on all lim/2^k limits in increasing order (see process_small_child subroutine), until one succeed or maximal limits both fails. This way, the time spent by a single phase of the algorithm is representative ... ...
 ... ... @@ -166,8 +166,8 @@ module RedBlackTree (* insertion *) (** [almost_rbtree n t]: [t] may have one red-red conflict at its root; it satisfies [rbtree n] everywhere else *) (** almost_rbtree n t: t may have one red-red conflict at its root; it satisfies rbtree n everywhere else *) predicate almost_rbtree (n : int) (t : tree) = match t with ... ... @@ -190,8 +190,8 @@ module RedBlackTree forall x: key, v: value, l r: tree, n: int. almost_rbtree n (Node Black l x v r) -> rbtree n (Node Black l x v r) (** [lbalance c x l r] acts as a black node constructor, solving a possible red-red conflict on [l], using the following (** lbalance c x l r acts as a black node constructor, solving a possible red-red conflict on l, using the following schema: B (R (R a x b) y c) z d ... ... @@ -216,8 +216,8 @@ module RedBlackTree Node Black l k v r end (** [rbalance l x r] is similar to [lbalance], solving a possible red-red conflict on [r]. The balancing schema is similar: (** rbalance l x r is similar to lbalance, solving a possible red-red conflict on r. The balancing schema is similar: B a x (R (R b y c) z d) B a x (R b y (R c z d)) -> R (B a x b) y (R c z d) ... ... @@ -240,8 +240,8 @@ module RedBlackTree Node Black l k v r end (* [insert x s] inserts [x] in tree [s], resulting in a possible top red-red conflict when [s] is red. *) (* insert x s inserts x in tree s, resulting in a possible top red-red conflict when s is red. *) let rec insert (t : tree) (k : key) (v : value) : tree requires { bst t /\ exists n: int. rbtree n t } ... ... @@ -265,7 +265,7 @@ module RedBlackTree else (* k = k' *) Node Black l k' v r end (* finally [add x s] calls [insert] and recolors the root as black *) (* finally add x s calls insert and recolors the root as black *) let add (t : tree) (k : key) (v : value) : tree requires { bst t /\ exists n:int. rbtree n t } ... ... @@ -320,7 +320,7 @@ module Vacid0 = let (d, t) = !m in try find t k with Not_found -> d end (* the easy way: implements [remove] using [replace] *) (* the easy way: implements remove using replace *) let remove (m : ref rbt) k requires { inv !m } ensures { inv !m /\ ... ...
 ... ... @@ -63,13 +63,13 @@ module DancingLinks invariant { length prev = length next = n } by { prev = make 0 0; next = make 0 0; n = 0 } (** node [i] is a valid node i.e. it has consistent neighbors *) (** node i is a valid node i.e. it has consistent neighbors *) predicate valid_in (l: dll) (i: int) = 0 <= i < l.n /\ 0 <= l.prev[i] < l.n /\ 0 <= l.next[i] < l.n /\ l.next[l.prev[i]] = i /\ l.prev[l.next[i]] = i (** node [i] is ready to be put back in a list *) (** node i is ready to be put back in a list *) predicate valid_out (l: dll) (i: int) = 0 <= i < l.n /\ 0 <= l.prev[i] < l.n /\ 0 <= l.next[i] < l.n /\ l.next[l.prev[i]] = l.next[i] /\ ... ... @@ -78,8 +78,8 @@ module DancingLinks use seq.Seq as S function nth (s: S.seq 'a) (i: int) : 'a = S.([]) s i (** Representation predicate: Sequence [s] is the list of indices of a valid circular list in [l]. (** Representation predicate: Sequence s is the list of indices of a valid circular list in l. We choose to model circular lists, since this is the way the data structure is used in Knuth's dancing links algorithm. *) predicate is_list (l: dll) (s: S.seq int) = ... ... @@ -90,7 +90,7 @@ module DancingLinks (forall k': int. 0 <= k' < S.length s -> k <> k' -> nth s k <> nth s k') (** Note: the code below works fine even when the list has one element (necessarily [i] in that case). *) (necessarily i in that case). *) let remove (l: dll) (i: int) (ghost s: S.seq int) requires { valid_in l i } requires { is_list l (S.cons i s) } ... ... @@ -103,10 +103,10 @@ module DancingLinks nth (S.cons i s) (k + 1) = nth s k } (* to help SMT with triggers *) let put_back (l: dll) (i: int) (ghost s: S.seq int) requires { valid_out l i } (* [i] is ready to be reinserted *) requires { valid_out l i } (* i is ready to be reinserted *) requires { is_list l s } requires { 0 < S.length s } (* [s] must contain at least one element *) requires { l.next[i] = nth s 0 <> i } (* do not link [i] to itself *) requires { 0 < S.length s } (* s must contain at least one element *) requires { l.next[i] = nth s 0 <> i } (* do not link i to itself *) ensures { valid_in l i } ensures { is_list l (S.cons i s) } = ... ...
 ... ... @@ -87,7 +87,7 @@ module RelaxedPrefix type char val eq (x y : char) : bool ensures { result = True <-> x = y } (** [a1[ofs1..ofs1+len]] and [a2[ofs2..ofs2+len]] are valid sub-arrays (** a1[ofs1..ofs1+len] and a2[ofs2..ofs2+len] are valid sub-arrays and they are equal *) predicate eq_array (a1: array char) (ofs1: int) (a2: array char) (ofs2: int) (len: int) = ... ... @@ -110,7 +110,7 @@ module RelaxedPrefix exception NoPrefix (** Note regarding the code: the suggested pseudo-code is buggy, as it may access [a] out of bounds. We fix it by strengthening the may access a out of bounds. We fix it by strengthening the test in the conditional. *) let is_relaxed_prefix (pat a: array char) : bool ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!