vstte10_queens.mlw 6.5 KB
 Jean-Christophe Filliatre committed Jun 22, 2011 1 2 3 4 ``````(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 4: N-queens `````` Jean-Christophe Filliatre committed Jul 05, 2011 5 6 `````` Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) `````` Jean-Christophe Filliatre committed Jun 22, 2011 7 ``````*) `````` Jean-Christophe Filliatre committed Nov 10, 2010 8 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 9 ``````module NQueens `````` Jean-Christophe Filliatre committed Nov 10, 2010 10 `````` `````` Jean-Christophe Filliatre committed Mar 18, 2011 11 `````` use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 12 `````` use import array.Array `````` Jean-Christophe Filliatre committed Nov 10, 2010 13 `````` `````` Andrei Paskevich committed Jun 29, 2011 14 `````` predicate eq_board (b1 b2: array int) (pos: int) = `````` Jean-Christophe Filliatre committed Mar 18, 2011 15 16 `````` forall q:int. 0 <= q < pos -> b1[q] = b2[q] `````` Jean-Christophe Filliatre committed May 17, 2011 17 18 `````` lemma eq_board_set: forall b: array int, pos q i: int. `````` Jean-Christophe Filliatre committed Mar 18, 2011 19 20 `````` pos <= q -> eq_board b b[q <- i] pos `````` Jean-Christophe Filliatre committed May 17, 2011 21 22 `````` lemma eq_board_sym: forall b1 b2: array int, pos: int. `````` Jean-Christophe Filliatre committed Mar 18, 2011 23 24 `````` eq_board b1 b2 pos -> eq_board b2 b1 pos `````` Jean-Christophe Filliatre committed May 17, 2011 25 26 `````` lemma eq_board_trans: forall b1 b2 b3: array int, pos: int. `````` Jean-Christophe Filliatre committed Mar 18, 2011 27 28 `````` eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos `````` Jean-Christophe Filliatre committed May 17, 2011 29 30 `````` lemma eq_board_extension: forall b1 b2: array int, pos: int. `````` Jean-Christophe Filliatre committed Mar 18, 2011 31 32 `````` eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1) `````` Andrei Paskevich committed Jun 29, 2011 33 34 35 `````` predicate consistent_row (board: array int) (pos: int) (q: int) = board[q] <> board[pos] /\ board[q] - board[pos] <> pos - q /\ `````` Jean-Christophe Filliatre committed Mar 18, 2011 36 `````` board[pos] - board[q] <> pos - q `````` Jean-Christophe Filliatre committed Nov 10, 2010 37 `````` `````` Jean-Christophe Filliatre committed May 17, 2011 38 39 40 `````` lemma consistent_row_eq: forall b1 b2: array int, pos: int. eq_board b1 b2 (pos+1) -> forall q: int. 0 <= q < pos -> `````` Andrei Paskevich committed Mar 19, 2011 41 `````` consistent_row b1 pos q -> consistent_row b2 pos q `````` Jean-Christophe Filliatre committed Mar 18, 2011 42 `````` `````` Andrei Paskevich committed Jun 29, 2011 43 `````` predicate is_consistent (board: array int) (pos: int) = `````` Jean-Christophe Filliatre committed Nov 10, 2010 44 45 `````` forall q:int. 0 <= q < pos -> consistent_row board pos q `````` Andrei Paskevich committed Mar 19, 2011 46 `````` exception Inconsistent int `````` Jean-Christophe Filliatre committed Mar 18, 2011 47 `````` `````` Andrei Paskevich committed Oct 13, 2012 48 49 50 51 `````` let check_is_consistent (board: array int) (pos: int) requires { 0 <= pos < length board } ensures { result=True <-> is_consistent board pos } = try `````` Jean-Christophe Filliatre committed Jun 22, 2011 52 `````` for q = 0 to pos - 1 do `````` Jean-Christophe Filliatre committed Mar 18, 2011 53 54 55 `````` invariant { forall j:int. 0 <= j < q -> consistent_row board pos j } let bq = board[q] in let bpos = board[pos] in `````` Andrei Paskevich committed Mar 19, 2011 56 57 58 `````` if bq = bpos then raise (Inconsistent q); if bq - bpos = pos - q then raise (Inconsistent q); if bpos - bq = pos - q then raise (Inconsistent q) `````` Jean-Christophe Filliatre committed Mar 18, 2011 59 60 `````` done; True `````` Andrei Paskevich committed Mar 19, 2011 61 62 `````` with Inconsistent q -> assert { not (consistent_row board pos q) }; `````` Jean-Christophe Filliatre committed Mar 18, 2011 63 64 `````` False end `````` Jean-Christophe Filliatre committed Nov 10, 2010 65 `````` `````` Andrei Paskevich committed Jun 29, 2011 66 `````` predicate is_board (board: array int) (pos: int) = `````` Jean-Christophe Filliatre committed Mar 18, 2011 67 `````` forall q:int. 0 <= q < pos -> 0 <= board[q] < length board `````` Jean-Christophe Filliatre committed Nov 11, 2010 68 `````` `````` Andrei Paskevich committed Jun 29, 2011 69 70 `````` predicate solution (board: array int) (pos: int) = is_board board pos /\ `````` Jean-Christophe Filliatre committed Nov 11, 2010 71 72 `````` forall q:int. 0 <= q < pos -> is_consistent board q `````` Jean-Christophe Filliatre committed May 17, 2011 73 74 `````` lemma solution_eq_board: forall b1 b2: array int, pos: int. length b1 = length b2 -> `````` Jean-Christophe Filliatre committed Mar 18, 2011 75 `````` eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos `````` Jean-Christophe Filliatre committed Nov 11, 2010 76 `````` `````` Jean-Christophe Filliatre committed Mar 18, 2011 77 78 `````` exception Solution `````` Andrei Paskevich committed Oct 13, 2012 79 80 81 82 83 84 85 86 `````` let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos } requires { length board = n /\ 0 <= pos <= n /\ solution board pos } ensures { (* no solution *) eq_board board (old board) pos /\ forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> not (solution b n) } raises { Solution -> solution board n } = 'Init: `````` Jean-Christophe Filliatre committed Mar 18, 2011 87 88 `````` if pos = n then raise Solution; for i = 0 to n - 1 do `````` Jean-Christophe Filliatre committed May 17, 2011 89 `````` invariant { `````` Jean-Christophe Filliatre committed Jul 05, 2011 90 `````` eq_board board (at board 'Init) pos /\ `````` Jean-Christophe Filliatre committed May 17, 2011 91 `````` forall b:array int. length b = n -> is_board b n -> `````` Jean-Christophe Filliatre committed Mar 18, 2011 92 `````` eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) } `````` Jean-Christophe Filliatre committed May 17, 2011 93 `````` board[pos] <- i; `````` Jean-Christophe Filliatre committed Mar 18, 2011 94 95 96 `````` if check_is_consistent board pos then bt_queens board n (pos+1) done `````` Andrei Paskevich committed Oct 13, 2012 97 `````` let queens (board: array int) (n: int) `````` Andrei Paskevich committed Jan 30, 2013 98 `````` requires { length board = n } `````` Andrei Paskevich committed Oct 13, 2012 99 100 101 `````` ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) } raises { Solution -> solution board n } = bt_queens board n 0 `````` Jean-Christophe Filliatre committed Nov 10, 2010 102 `````` `````` MARCHE Claude committed Jan 15, 2014 103 104 105 106 107 108 109 110 111 112 113 `````` exception BenchFailure let test8 () raises { BenchFailure -> true } = let a = Array.make 8 0 in try queens a 8; raise BenchFailure with Solution -> a end `````` Jean-Christophe Filliatre committed Apr 11, 2015 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 `````` (** variant: counting solutions (not part of the competition) TODO: prove soundness i.e. we indeed count the number of solutions *) use import ref.Refint let rec count_bt_queens (board: array int) (n: int) (pos: int) : int variant { n - pos } requires { length board = n /\ 0 <= pos <= n /\ solution board pos } ensures { eq_board board (old board) pos } = 'Init: if pos = n then 1 else begin let s = ref 0 in for i = 0 to n - 1 do invariant { eq_board board (at board 'Init) pos } board[pos] <- i; if check_is_consistent board pos then s += count_bt_queens board n (pos+1) done; !s end let count_queens (board: array int) (n: int) : int requires { length board = n } ensures { true } = count_bt_queens board n 0 let test_count_8 () = let a = Array.make 8 0 in count_queens a 8 end `````` Jean-Christophe Filliatre committed Jul 10, 2015 149 ``````(** counting solutions with 63-bit machine integers *) `````` Jean-Christophe Filliatre committed Apr 11, 2015 150 `````` `````` Jean-Christophe Filliatre committed Jul 10, 2015 151 ``````module NQueens63 `````` Jean-Christophe Filliatre committed Apr 11, 2015 152 153 154 155 156 `````` use import ref.Refint use import mach.array.Array63 use import mach.int.Int63 `````` Jean-Christophe Filliatre committed Jul 08, 2015 157 `````` predicate is_board (board: array63 int63) (pos: int) = `````` Jean-Christophe Filliatre committed Apr 11, 2015 158 159 160 `````` forall q: int. 0 <= q < pos -> 0 <= to_int board[q] < to_int (length board) `````` Jean-Christophe Filliatre committed Apr 20, 2015 161 `````` exception MInconsistent `````` Jean-Christophe Filliatre committed Apr 11, 2015 162 `````` `````` Jean-Christophe Filliatre committed Jul 10, 2015 163 `````` let check_is_consistent (board: array63 int63) (pos: int63) `````` Jean-Christophe Filliatre committed Apr 11, 2015 164 165 166 `````` requires { 0 <= to_int pos < to_int (length board) } requires { is_board board (to_int pos + 1) } = try `````` Jean-Christophe Filliatre committed Apr 20, 2015 167 168 169 170 171 172 173 174 175 176 177 178 `````` let q = ref (of_int 0) in while !q < pos do invariant { 0 <= to_int !q <= to_int pos } invariant { is_board board (to_int pos + 1) } variant { to_int pos - to_int !q } let bq = board[!q] in let bpos = board[pos] in if bq = bpos then raise MInconsistent; if bq - bpos = pos - !q then raise MInconsistent; if bpos - bq = pos - !q then raise MInconsistent; q := !q + of_int 1 done; `````` Jean-Christophe Filliatre committed Apr 11, 2015 179 `````` True `````` Jean-Christophe Filliatre committed Apr 20, 2015 180 `````` with MInconsistent -> `````` Jean-Christophe Filliatre committed Apr 11, 2015 181 182 183 `````` False end `````` Jean-Christophe Filliatre committed Apr 20, 2015 184 `````` use mach.peano.Peano as P `````` Jean-Christophe Filliatre committed Apr 11, 2015 185 `````` `````` Jean-Christophe Filliatre committed Jul 10, 2015 186 `````` let rec count_bt_queens `````` Jean-Christophe Filliatre committed Jul 08, 2015 187 `````` (solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63) `````` Jean-Christophe Filliatre committed Apr 11, 2015 188 189 190 191 192 193 194 `````` requires { to_int (length board) = to_int n } requires { 0 <= to_int pos <= to_int n } requires { is_board board (to_int pos) } variant { to_int n - to_int pos } ensures { is_board board (to_int pos) } = if eq pos n then `````` Jean-Christophe Filliatre committed Apr 20, 2015 195 196 197 198 199 200 201 202 `````` solutions := P.succ !solutions else let i = ref (of_int 0) in while !i < n do invariant { 0 <= to_int !i <= to_int n } invariant { is_board board (to_int pos) } variant { to_int n - to_int !i } board[pos] <- !i; `````` Jean-Christophe Filliatre committed Jul 10, 2015 203 204 `````` if check_is_consistent board pos then count_bt_queens solutions board n (pos + of_int 1); `````` Jean-Christophe Filliatre committed Apr 20, 2015 205 206 207 `````` i := !i + of_int 1 done `````` Jean-Christophe Filliatre committed Jul 10, 2015 208 209 `````` let count_queens (n: int63) : P.t requires { to_int n >= 0 } `````` Jean-Christophe Filliatre committed Apr 11, 2015 210 `````` ensures { true } `````` Jean-Christophe Filliatre committed Apr 20, 2015 211 212 `````` = let solutions = ref (P.zero ()) in `````` Jean-Christophe Filliatre committed Jul 10, 2015 213 `````` let board = Array63.make n (of_int 0) in `````` Jean-Christophe Filliatre committed Jul 10, 2015 214 `````` count_bt_queens solutions board n (of_int 0); `````` Jean-Christophe Filliatre committed Apr 20, 2015 215 `````` !solutions `````` Jean-Christophe Filliatre committed Apr 11, 2015 216 `````` `````` Jean-Christophe Filliatre committed Jul 10, 2015 217 `````` let test_count_8 () = `````` Jean-Christophe Filliatre committed Apr 11, 2015 218 `````` let n = of_int 8 in `````` Jean-Christophe Filliatre committed Jul 10, 2015 219 `````` count_queens n `````` Jean-Christophe Filliatre committed Apr 11, 2015 220 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 221 ``````end `````` Jean-Christophe Filliatre committed Apr 11, 2015 222