VerifyThis 2015: solution to problem 3
Auteurs: Jean-Christophe Filliâtre / Guillaume Melquiond
Catégories: Data Structures
Outils: Why3
Références: VerifyThis @ ETAPS 2015
see also the index (by topic, by tool, by reference, by year)
VerifyThis @ ETAPS 2015 competition, Challenge 3: Dancing Links
The following is the original description of the verification task, reproduced verbatim from the competition web site.
DANCING LINKS (90 minutes) ========================== Dancing links is a technique introduced in 1979 by Hitotumatu and Noshita and later popularized by Knuth. The technique can be used to efficiently implement a search for all solutions of the exact cover problem, which in its turn can be used to solve Tiling, Sudoku, N-Queens, and other problems. The technique ------------- Suppose x points to a node of a doubly linked list; let L[x] and R[x] point to the predecessor and successor of that node. Then the operations L[R[x]] := L[x]; R[L[x]] := R[x]; remove x from the list. The subsequent operations L[R[x]] := x; R[L[x]] := x; will put x back into the list again. A graphical illustration of the process is available at http://formal.iti.kit.edu/~klebanov/DLX.png Verification task ----------------- Implement the data structure with these operations, and specify and verify that they behave in the way described above.
The following is the solution by Jean-Christophe FilliĆ¢tre (CNRS) and Guillaume Melquiond (Inria) who entered the competition as "team Why3".
module DancingLinks use int.Int use ref.Ref use array.Array type dll = { prev: array int; next: array int; ghost n: int } invariant { length prev = length next = n } by { prev = make 0 0; next = make 0 0; n = 0 }
we model the data structure with two arrays, nodes being represented by array indices
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 a valid node i.e. it has consistent neighbors
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] /\ l.prev[l.next[i]] = l.prev[i]
node i
is ready to be put back in a list
use seq.Seq as S function nth (s: S.seq 'a) (i: int) : 'a = S.([]) s i predicate is_list (l: dll) (s: S.seq int) = forall k: int. 0 <= k < S.length s -> 0 <= nth s k < l.n /\ l.prev[nth s k] = nth s (if k = 0 then S.length s - 1 else k - 1) /\ l.next[nth s k] = nth s (if k = S.length s - 1 then 0 else k + 1) /\ (forall k': int. 0 <= k' < S.length s -> k <> k' -> nth s k <> nth s k')
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.
let remove (l: dll) (i: int) (ghost s: S.seq int) requires { valid_in l i } requires { is_list l (S.cons i s) } ensures { valid_out l i } ensures { is_list l s } = l.prev[l.next[i]] <- l.prev[i]; l.next[l.prev[i]] <- l.next[i]; assert { forall k: int. 0 <= k < S.length s -> nth (S.cons i s) (k + 1) = nth s k } (* to help SMT with triggers *)
Note: the code below works fine even when the list has one element
(necessarily i
in that case).
let put_back (l: dll) (i: int) (ghost s: S.seq int) 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 *) ensures { valid_in l i } ensures { is_list l (S.cons i s) } = l.prev[l.next[i]] <- i; l.next[l.prev[i]] <- i end
download ZIP archive
Why3 Proof Results for Project "verifythis_2015_dancing_links"
Theory "verifythis_2015_dancing_links.DancingLinks": fully verified
Obligations | Alt-Ergo 2.1.0 | |
VC for dll | 0.00 | |
VC for remove | 1.21 | |
split_goal_right | ||
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.00 | |
index in array bounds | 0.01 | |
index in array bounds | 0.02 | |
assertion | 0.01 | |
type invariant | 0.02 | |
postcondition | 0.06 | |
postcondition | 0.46 | |
VC for put_back | 0.71 |