## The N-queens problem, in Why3

How to place n queens on a nxn chessboard, Why3 version

**Authors:** Jean-Christophe Filliâtre

**Topics:** Exceptions

**Tools:** Why3

**References:** The 1st Verified Software Competition / The VerifyThis Benchmarks

**See also:** The N-queens problem, in C with Caduceus tool

see also the index (by topic, by tool, by reference, by year)

(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 4: N-queens Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) *) module NQueens use import int.Int use import array.Array predicate eq_board (b1 b2: array int) (pos: int) = forall q:int. 0 <= q < pos -> b1[q] = b2[q] lemma eq_board_set: forall b: array int, pos q i: int. pos <= q -> eq_board b b[q <- i] pos lemma eq_board_sym: forall b1 b2: array int, pos: int. eq_board b1 b2 pos -> eq_board b2 b1 pos lemma eq_board_trans: forall b1 b2 b3: array int, pos: int. eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos lemma eq_board_extension: forall b1 b2: array int, pos: int. eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1) predicate consistent_row (board: array int) (pos: int) (q: int) = board[q] <> board[pos] /\ board[q] - board[pos] <> pos - q /\ board[pos] - board[q] <> pos - q lemma consistent_row_eq: forall b1 b2: array int, pos: int. eq_board b1 b2 (pos+1) -> forall q: int. 0 <= q < pos -> consistent_row b1 pos q -> consistent_row b2 pos q predicate is_consistent (board: array int) (pos: int) = forall q:int. 0 <= q < pos -> consistent_row board pos q exception Inconsistent int let check_is_consistent (board: array int) (pos: int) requires { 0 <= pos < length board } ensures { result=True <-> is_consistent board pos } = try for q = 0 to pos - 1 do invariant { forall j:int. 0 <= j < q -> consistent_row board pos j } let bq = board[q] in let bpos = board[pos] in 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) done; True with Inconsistent q -> assert { not (consistent_row board pos q) }; False end predicate is_board (board: array int) (pos: int) = forall q:int. 0 <= q < pos -> 0 <= board[q] < length board predicate solution (board: array int) (pos: int) = is_board board pos /\ forall q:int. 0 <= q < pos -> is_consistent board q lemma solution_eq_board: forall b1 b2: array int, pos: int. length b1 = length b2 -> eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos exception Solution 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: if pos = n then raise Solution; for i = 0 to n - 1 do invariant { eq_board board (at board 'Init) pos /\ forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) } board[pos] <- i; if check_is_consistent board pos then bt_queens board n (pos+1) done let queens (board: array int) (n: int) requires { length board = n } 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 exception BenchFailure let test8 () raises { BenchFailure -> true } = let a = Array.make 8 0 in try queens a 8; raise BenchFailure with Solution -> a end

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

counting solutions with 63-bit machine integers

module NQueens63 use import ref.Refint use import mach.array.Array63 use import mach.int.Int63 predicate is_board (board: array63 int63) (pos: int) = forall q: int. 0 <= q < pos -> 0 <= to_int board[q] < to_int (length board) exception MInconsistent let check_is_consistent (board: array63 int63) (pos: int63) requires { 0 <= to_int pos < to_int (length board) } requires { is_board board (to_int pos + 1) } = try 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; True with MInconsistent -> False end use mach.peano.Peano as P let rec count_bt_queens (solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63) 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 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; if check_is_consistent board pos then count_bt_queens solutions board n (pos + of_int 1); i := !i + of_int 1 done let count_queens (n: int63) : P.t requires { to_int n >= 0 } ensures { true } = let solutions = ref (P.zero ()) in let board = Array63.make n (of_int 0) in count_bt_queens solutions board n (of_int 0); !solutions let test_count_8 () = let n = of_int 8 in count_queens n end

download ZIP archive

# Why3 Proof Results for Project "vstte10_queens"

## Theory "vstte10_queens.NQueens": fully verified in 1.91 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | CVC4 (1.4) | Z3 (3.2) |

eq_board_set | 0.00 | --- | --- | --- |

eq_board_sym | 0.01 | --- | --- | --- |

eq_board_trans | 0.01 | --- | --- | --- |

eq_board_extension | 0.01 | --- | --- | --- |

consistent_row_eq | 0.06 | --- | --- | --- |

VC for check_is_consistent | --- | 0.02 | --- | --- |

solution_eq_board | --- | --- | --- | 0.06 |

VC for bt_queens | --- | 1.42 | --- | --- |

VC for queens | 0.02 | --- | --- | --- |

VC for test8 | 0.01 | --- | --- | --- |

VC for count_bt_queens | --- | --- | 0.27 | --- |

VC for count_queens | 0.01 | --- | --- | --- |

VC for test_count_8 | 0.01 | --- | --- | --- |

## Theory "vstte10_queens.NQueens63": fully verified in 1.06 s

Obligations | Alt-Ergo (0.99.1) | CVC4 (1.4) | Z3 (4.3.2) | |

VC for check_is_consistent | --- | 0.09 | --- | |

VC for count_bt_queens | --- | --- | --- | |

split_goal_wp | ||||

1. postcondition | 0.02 | --- | --- | |

2. integer overflow | 0.02 | --- | --- | |

3. loop invariant init | 0.02 | --- | --- | |

4. loop invariant init | 0.02 | --- | --- | |

5. type invariant | 0.02 | --- | --- | |

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

7. precondition | 0.02 | --- | --- | |

8. precondition | 0.17 | --- | --- | |

9. integer overflow | 0.02 | --- | --- | |

10. integer overflow | 0.04 | --- | --- | |

11. variant decrease | 0.02 | --- | --- | |

12. precondition | 0.02 | --- | --- | |

13. precondition | 0.02 | --- | --- | |

14. precondition | 0.00 | 0.05 | --- | |

15. integer overflow | 0.02 | --- | --- | |

16. integer overflow | 0.13 | --- | --- | |

17. loop invariant preservation | 0.02 | --- | --- | |

18. loop invariant preservation | 0.02 | --- | --- | |

19. loop variant decrease | 0.02 | --- | --- | |

20. integer overflow | 0.01 | --- | --- | |

21. integer overflow | 0.02 | --- | --- | |

22. loop invariant preservation | 0.02 | --- | --- | |

23. loop invariant preservation | 0.11 | --- | --- | |

24. loop variant decrease | 0.02 | --- | --- | |

25. type invariant | 0.02 | 0.05 | --- | |

26. postcondition | 0.01 | --- | --- | |

VC for count_queens | 0.01 | --- | --- | |

VC for test_count_8 | 0.00 | --- | 0.01 |