Commit b865c0c4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

vstte'10 : problem 4 completed, apart completeness

parent df8a5743
......@@ -2,3 +2,4 @@ next_digit_sum
vstte10_max_sum
vstte10_inverting
vstte10_search_list
vstte10_queens
(* VSTTE'10 competition
Problem 4: N-queens *)
{
use array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
}
let array_get (a : ref (array 'a)) i =
{ 0 <= i < A.length !a } A.get !a i { result = A.get !a i }
let array_set (a : ref (array 'a)) i v =
{ 0 <= i < A.length !a } a := A.set !a i v { !a = A.set (old !a) i v }
{
logic consistent_row (board : array int) (pos : int) (q : int) =
board#q <> board#pos and
board#q - board#pos <> pos - q and
board#pos - board#q <> pos - q
logic is_consistent (board : array int) (pos : int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q
axiom Is_consistent_eq :
forall board : array int, pos q i : int.
is_consistent board pos -> pos <= q -> is_consistent (A.set board q i) pos
}
exception Inconsistent
let check_is_consistent board pos =
{ 0 <= pos < A.length !board }
try
for q = 0 to pos-1 do
invariant { forall j:int. 0 <= j < q -> consistent_row !board pos j }
let bq = array_get board q in
let bpos = array_get board pos in
if bq = bpos then begin
assert { not (consistent_row !board pos q) }; (* to help the provers *)
raise Inconsistent
end;
if bq - bpos = pos - q then raise Inconsistent;
if bpos - bq = pos - q then raise Inconsistent
done;
True
with Inconsistent ->
False
end
{ result=True <-> is_consistent !board pos }
{
logic solution (board : array int) (pos : int) =
forall q:int. 0 <= q < pos ->
0 <= board#q < A.length board and is_consistent board q
}
exception Solution
let rec queens (board : ref (array int)) pos =
{ 0 <= pos <= A.length !board and solution !board pos }
label Init:
if pos = A.length !board then raise Solution;
for i = 0 to A.length !board - 1 do
invariant {
A.length !board = at (A.length !board) Init and
solution !board pos }
array_set board pos i;
if check_is_consistent board pos then queens board (pos+1)
done
{ (* no solution (TODO: show there is indeed no solution) *)
A.length !board = old (A.length !board) and solution !board pos }
| Solution ->
{ (* a solution *)
solution !board (A.length !board) }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_queens.gui"
End:
*)
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