## 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

Obligations | Alt-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 bounds | 0.02 | --- | --- | |

4. index in array bounds | 0.02 | --- | --- | |

5. type invariant | 0.01 | --- | --- | |

6. index in array bounds | --- | 0.02 | --- | |

7. index in array bounds | 0.01 | --- | --- | |

8. assertion | 0.02 | --- | --- | |

9. type invariant | 0.01 | --- | --- | |

10. type invariant | 0.02 | --- | --- | |

11. postcondition | 0.12 | --- | --- | |

12. postcondition | --- | --- | 0.21 | |

VC for put_back | --- | --- | --- | |

split_goal_wp | ||||

1. index in array bounds | 0.01 | --- | --- | |

2. index in array bounds | 0.02 | --- | --- | |

3. type invariant | 0.02 | --- | --- | |

4. index in array bounds | 0.02 | --- | --- | |

5. index in array bounds | 0.01 | --- | --- | |

6. type invariant | 0.02 | --- | --- | |

7. type invariant | 0.01 | --- | --- | |

8. postcondition | 0.05 | --- | --- | |

9. postcondition | --- | --- | 0.25 |