Wiki Agenda Contact Version française

VerifyThis 2015: solution to problem 3


Authors: Jean-Christophe Filliâtre / Guillaume Melquiond

Topics: Data Structures

Tools: Why3

References: 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 import int.Int
  use import ref.Ref
  use import array.Array

we model the data structure with two arrays, nodes being represented by array indices

  type dll = { prev: array int; next: array int; ghost n: int }
    invariant { length self.prev = length self.next = self.n }

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

  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]

  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. 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) =
    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')

Note: the code below works fine even when the list has one element (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) }
    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 *)

  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 in 0.98 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)Z3 (4.3.2)
VC for remove---------
split_goal_wp
  1. index in array bounds---0.08---
2. index in array bounds------0.03
3. index in array bounds0.02------
4. index in array bounds0.02------
5. type invariant0.01------
6. index in array bounds---0.02---
7. index in array bounds0.01------
8. assertion0.02------
9. type invariant0.01------
10. type invariant0.02------
11. postcondition0.12------
12. postcondition------0.21
VC for put_back---------
split_goal_wp
  1. index in array bounds0.01------
2. index in array bounds0.02------
3. type invariant0.02------
4. index in array bounds0.02------
5. index in array bounds0.01------
6. type invariant0.02------
7. type invariant0.01------
8. postcondition0.05------
9. postcondition------0.25