Wiki Agenda Contact English version

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

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 <=[i] < l.n /\[l.prev[i]] = i /\
    l.prev[[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 <=[i] < l.n /\[l.prev[i]] =[i] /\
    l.prev[[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) /\[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[[i]] <- l.prev[i];[l.prev[i]] <-[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 {[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[[i]] <- i;[l.prev[i]] <- i


download ZIP archive

Why3 Proof Results for Project "verifythis_2015_dancing_links"

Theory "verifythis_2015_dancing_links.DancingLinks": fully verified

ObligationsAlt-Ergo 2.1.0
VC for dll0.00
VC for remove1.21
index in array bounds0.01
index in array bounds0.01
index in array bounds0.01
index in array bounds0.00
index in array bounds0.01
index in array bounds0.02
type invariant0.02
VC for put_back0.71