VerifyThis @ ETAPS 2015: solution to challenge 3

parent 99666f94
(**
{1 VerifyThis @ ETAPS 2015 competition, Challenge 3: Dancing Links}
{h
The following is the original description of the verification task,
reproduced verbatim from
<a href="http://etaps2015.verifythis.org/challenges">the competition web site</a>.
<pre>
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.
</pre>}
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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<file name="../verifythis_2015_dancing_links.mlw" expanded="true">
<theory name="DancingLinks" sum="9ccd1c1f1172efa1e75be2e365507169" expanded="true">
<goal name="WP_parameter remove" expl="VC for remove" expanded="true">
<transf name="split_goal_wp">
<goal name="WP_parameter remove.1" expl="1. index in array bounds">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter remove.2" expl="2. index in array bounds">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter remove.3" expl="3. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter remove.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove.5" expl="5. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove.6" expl="6. index in array bounds">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter remove.7" expl="7. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter remove.9" expl="9. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove.10" expl="10. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.12" steps="34"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="12. postcondition">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter put_back" expl="VC for put_back" expanded="true">
<transf name="split_goal_wp">
<goal name="WP_parameter put_back.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter put_back.2" expl="2. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter put_back.3" expl="3. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter put_back.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter put_back.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="WP_parameter put_back.6" expl="6. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter put_back.7" expl="7. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter put_back.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.17" steps="35"/></proof>
</goal>
<goal name="WP_parameter put_back.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.80"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment