Jean-Christophe Filliatre committed Apr 13, 2015 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 `````` (** {1 VerifyThis @ ETAPS 2015 competition, Challenge 3: Dancing Links} {h The following is the original description of the verification task, reproduced verbatim from the competition web site.
} The following is the solution by Jean-Christophe Filliâtre (CNRS) and Guillaume Melquiond (Inria) who entered the competition as "team Why3". *) module DancingLinks `````` Andrei Paskevich committed Jun 15, 2018 56 57 58 `````` use int.Int use ref.Ref use array.Array `````` Jean-Christophe Filliatre committed Apr 13, 2015 59 60 61 62 `````` (** 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 } `````` Guillaume Melquiond committed Mar 16, 2016 63 `````` invariant { length prev = length next = n } `````` Andrei Paskevich committed Jun 26, 2017 64 `````` by { prev = make 0 0; next = make 0 0; n = 0 } `````` Jean-Christophe Filliatre committed Apr 13, 2015 65 `````` `````` Guillaume Melquiond committed Jun 14, 2018 66 `````` (** node `i` is a valid node i.e. it has consistent neighbors *) `````` Jean-Christophe Filliatre committed Apr 13, 2015 67 68 69 70 71 `````` 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 `````` Guillaume Melquiond committed Jun 14, 2018 72 `````` (** node `i` is ready to be put back in a list *) `````` Jean-Christophe Filliatre committed Apr 13, 2015 73 74 75 76 77 78 79 80 `````` 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 `````` Guillaume Melquiond committed Jun 14, 2018 81 82 `````` (** Representation predicate: Sequence `s` is the list of indices of a valid circular list in `l`. `````` Jean-Christophe Filliatre committed Apr 13, 2015 83 84 85 86 87 88 89 90 91 92 `````` 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 `````` Guillaume Melquiond committed Jun 14, 2018 93 `````` (necessarily `i` in that case). *) `````` Jean-Christophe Filliatre committed Apr 13, 2015 94 95 96 97 98 99 100 101 102 103 104 105 `````` 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) `````` Guillaume Melquiond committed Jun 14, 2018 106 `````` requires { valid_out l i } (* `i` is ready to be reinserted *) `````` Jean-Christophe Filliatre committed Apr 13, 2015 107 `````` requires { is_list l s } `````` Guillaume Melquiond committed Jun 14, 2018 108 109 `````` 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 *) `````` Jean-Christophe Filliatre committed Apr 13, 2015 110 111 112 113 114 115 116 `````` 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``````