doc, chapter 3: problem 4 updated

parent 17605fb8
......@@ -516,7 +516,7 @@ Then it is possible to define the consistency of row \texttt{pos}
with respect to all previous rows:
\begin{whycode}
predicate is_consistent (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q
forall q. 0 <= q < pos -> consistent_row board pos q
\end{whycode}
Implementing a function which decides this predicate is another
matter. In order for it to be efficient, we want to return
......@@ -533,9 +533,9 @@ as one is found, the exception is raised. It is caught immediately
outside the loop and \texttt{False} is returned. Whenever the end of
the loop is reached, \texttt{True} is returned.
\begin{whycode}
let check_is_consistent (board: array int) (pos: int)
let check_is_consistent (board: array int) (pos: int) : bool
requires { 0 <= pos < length board }
ensures { result=True <-> is_consistent board pos }
ensures { result <-> is_consistent board pos }
= try
for q = 0 to pos - 1 do
invariant {
......@@ -573,13 +573,13 @@ module NQueens
board[pos] - board[q] <> pos - q
predicate is_consistent (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q
forall q. 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 }
ensures { result <-> is_consistent board pos }
= try
for q = 0 to pos - 1 do
invariant {
......@@ -614,11 +614,11 @@ two predicates, one related to legal column values and another to
consistency of rows:
\begin{whycode}
predicate is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
forall q. 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
forall q. 0 <= q < pos -> is_consistent board q
\end{whycode}
The algorithm will not mutate the partial solution it is given and,
in case of a search failure, will claim that there is no solution
......@@ -626,7 +626,7 @@ extending this prefix. For this reason, we introduce a predicate
comparing two chess boards for equality up to a given row:
\begin{whycode}
predicate eq_board (b1 b2: array int) (pos: int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]
forall q. 0 <= q < pos -> b1[q] = b2[q]
\end{whycode}
The search itself makes use of an exception to signal a successful search:
\begin{whycode}
......@@ -636,8 +636,8 @@ The backtracking code is a recursive function \verb|bt_queens| which
takes the chess board, its size, and the starting row for the search.
The termination is ensured by the obvious variant \texttt{n-pos}.
\begin{whycode}
let rec bt_queens (board: array int) (n: int) (pos: int)
variant { n-pos }
let rec bt_queens (board: array int) (n: int) (pos: int) : unit
variant { n - pos }
\end{whycode}
The precondition relates \texttt{board}, \texttt{pos}, and \texttt{n}
and requires \texttt{board} to be a solution up to \texttt{pos}:
......@@ -655,11 +655,8 @@ or the function raises \texttt{Solution} and we have a solution in
ensures { 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:
=
\end{whycode}
We place a code mark \texttt{'Init} immediately at the beginning of
the program body to
be able to refer to the value of \texttt{board} in the pre-state.
Whenever we reach the end of the chess board, we have found a solution
and we signal it using exception \texttt{Solution}:
\begin{whycode}
......@@ -675,7 +672,7 @@ prefix so far, and that we have not found any solution that would
extend this prefix with a queen on row \texttt{pos} at a column below
\texttt{i}:
\begin{whycode}
invariant { eq_board board (at board 'Init) pos }
invariant { eq_board board (old board) pos }
invariant { forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
\end{whycode}
......@@ -692,8 +689,8 @@ Solving the puzzle is a simple call to \verb|bt_queens|, starting the
search on row 0. The postcondition is also twofold, as for
\verb|bt_queens|, yet slightly simpler.
\begin{whycode}
let queens (board: array int) (n: int)
requires { 0 <= length board = n }
let queens (board: array int) (n: int) : unit
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 }
......@@ -712,18 +709,18 @@ automatically, including the verification of the lemmas themselves.
%END LATEX
\begin{whycode}
predicate is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
forall q. 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
forall q. 0 <= q < pos -> is_consistent board q
predicate eq_board (b1 b2: array int) (pos: int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]
forall q. 0 <= q < pos -> b1[q] = b2[q]
exception Solution
let rec bt_queens (board: array int) (n: int) (pos: int)
let rec bt_queens (board: array int) (n: int) (pos: int) : unit
variant { n - pos }
requires { 0 <= pos <= n = length board }
requires { solution board pos }
......@@ -731,18 +728,17 @@ automatically, including the verification of the lemmas themselves.
ensures { 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;
= if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant { eq_board board (at board 'Init) pos }
invariant { eq_board board (old board) pos }
invariant { 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 { 0 <= length board = n }
let queens (board: array int) (n: int) : unit
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 }
......
......@@ -12,7 +12,7 @@ module NQueens
use import array.Array
predicate eq_board (b1 b2: array int) (pos: int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]
forall q. 0 <= q < pos -> b1[q] = b2[q]
lemma eq_board_set:
forall b: array int, pos q i: int.
......@@ -41,16 +41,16 @@ module NQueens
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
forall q. 0 <= q < pos -> consistent_row board pos q
exception Inconsistent int
let check_is_consistent (board: array int) (pos: int)
let check_is_consistent (board: array int) (pos: int) : bool
requires { 0 <= pos < length board }
ensures { result=True <-> is_consistent board pos }
ensures { result <-> is_consistent board pos }
= try
for q = 0 to pos - 1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
invariant { forall j. 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);
......@@ -64,11 +64,11 @@ module NQueens
end
predicate is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
forall q. 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
forall q. 0 <= q < pos -> is_consistent board q
lemma solution_eq_board:
forall b1 b2: array int, pos: int. length b1 = length b2 ->
......@@ -76,27 +76,27 @@ module NQueens
exception Solution
let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos }
let rec bt_queens (board: array int) (n: int) (pos: int) : unit
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 }
ensures { eq_board board (old board) pos }
ensures { 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 }
= if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
eq_board board (old board) 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) }
invariant { eq_board board (old board) pos }
invariant { 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)
if check_is_consistent board pos then bt_queens board n (pos + 1)
done
let queens (board: array int) (n: int)
let queens (board: array int) (n: int) : unit
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 }
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
......@@ -154,12 +154,11 @@ module NQueens63
use import mach.int.Int63
predicate is_board (board: array int63) (pos: int) =
forall q: int. 0 <= q < pos ->
0 <= board[q] < (length board)
forall q. 0 <= q < pos -> 0 <= board[q] < (length board)
exception MInconsistent
let check_is_consistent (board: array int63) (pos: int63)
let check_is_consistent (board: array int63) (pos: int63) : bool
requires { 0 <= pos < (length board) }
requires { is_board board (pos + 1) }
= try
......@@ -183,7 +182,7 @@ module NQueens63
use mach.peano.Peano as P
let rec count_bt_queens
(solutions: ref P.t) (board: array int63) (n: int63) (pos: int63)
(solutions: ref P.t) (board: array int63) (n: int63) (pos: int63) : unit
requires { (length board) = n }
requires { 0 <= pos <= n }
requires { is_board board (pos) }
......
......@@ -5,6 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../vstte10_queens.mlw" proved="true">
<theory name="NQueens" proved="true">
<goal name="eq_board_set" proved="true">
......@@ -34,33 +35,45 @@
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC bt_queens.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC bt_queens.2" expl="index in array bounds" proved="true">
<goal name="VC bt_queens.2" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC bt_queens.3" expl="precondition" proved="true">
<goal name="VC bt_queens.3" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC bt_queens.4" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC bt_queens.4" expl="variant decrease" proved="true">
<goal name="VC bt_queens.5" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC bt_queens.5" expl="precondition" proved="true">
<goal name="VC bt_queens.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC bt_queens.6" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="230"/></proof>
<goal name="VC bt_queens.7" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC bt_queens.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="136"/></proof>
</goal>
<goal name="VC bt_queens.7" expl="exceptional postcondition" proved="true">
<goal name="VC bt_queens.9" expl="exceptional postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC bt_queens.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.51" steps="850"/></proof>
<goal name="VC bt_queens.10" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC bt_queens.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.16" steps="402"/></proof>
</goal>
<goal name="VC bt_queens.12" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC bt_queens.9" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="33"/></proof>
<goal name="VC bt_queens.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC bt_queens.10" expl="postcondition" proved="true">
<goal name="VC bt_queens.14" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
......
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