\chapter{The \whyml Programming Language}
\label{chap:whyml}

This chapter describes the \whyml programming language.
A \whyml input text contains a list of theories (see
Chapter~\ref{chap:syntax}) and/or modules.
Modules extend theories with \emph{programs}.
Programs can use all types, symbols, and constructs from the logic.
They also provide extra features:
\begin{itemize}
\item
  In a record type declaration, some fields can be declared
  \texttt{mutable} and/or \texttt{ghost}.
\item
  In an algebraic type declaration (this includes record types), an
  invariant can be specified.
\item
  There are programming constructs with no counterpart in the logic:
  \begin{itemize}
  \item mutable field assignment;
  \item sequence;
  \item loops;
  \item exceptions;
  \item local and anonymous functions;
  \item ghost parameters and ghost code;
  \item annotations: pre- and postconditions, assertions, loop invariants.
  \end{itemize}
\item
  A program function can be non-terminating or can be proved
  to be terminating using a variant (a term together with a well-founded
  order relation).
\item
  An abstract program type $t$ can be introduced with a logical
  \emph{model} $\tau$: inside programs, $t$ is abstract, and inside
  annotations, $t$ is an alias for $\tau$.
\end{itemize}
%
Programs are contained in files with suffix \verb|.mlw|.
They are handled by \texttt{why3}. For instance
\begin{verbatim}
> why3 prove myfile.mlw
\end{verbatim}
will display the verification conditions extracted from modules in
file \texttt{myfile.mlw}, as a set of corresponding theories, and
\begin{verbatim}
> why3 prove -P alt-ergo myfile.mlw
\end{verbatim}
will run the SMT solver Alt-Ergo on these verification conditions.
Program files are also handled by the GUI tool \texttt{why3ide}.
See Chapter~\ref{chap:manpages} for more details regarding command lines.

\medskip
As an introduction to \whyml, we use the five problems from the VSTTE
2010 verification competition~\cite{vstte10comp}.
The source code for all these examples is contained in \why's
distribution, in sub-directory \texttt{examples/}.

\section{Problem 1: Sum and Maximum}
\label{sec:MaxAndSum}

The first problem is stated as follows:
\begin{quote}
  Given an $N$-element array of natural numbers,
  write a program to compute the sum and the maximum of the
  elements in the array.
\end{quote}
We  assume $N \ge 0$ and $a[i] \ge 0$ for $0 \le i < N$, as precondition,
and we have to prove the following postcondition:
\begin{displaymath}
  sum \le N \times max.
\end{displaymath}
In a file \verb|max_sum.mlw|, we start a new module:
\begin{whycode}
module MaxAndSum
\end{whycode}
We are obviously needing arithmetic, so we import the corresponding
theory, exactly as we would do within a theory definition:
\begin{whycode}
  use import int.Int
\end{whycode}
We are also going to use references and arrays from \whyml's standard
library, so we import the corresponding modules, with a similar
declaration:
\begin{whycode}
  use import ref.Ref
  use import array.Array
\end{whycode}
Modules \texttt{Ref} and \texttt{Array} respectively provide a type
\texttt{ref 'a} for references and a type \texttt{array 'a} for
arrays, together with useful
operations and traditional syntax. They are loaded from the \whyml
files \texttt{ref.mlw} and \texttt{array.mlw} in the standard library.
\why reports an error when it finds a theory and a module with
the same name in the standard library, or when it finds a theory
declared in a \texttt{.mlw} file and in a \texttt{.why} file with
the same name.

We are now in position to define a program function
\verb|max_sum|. A function definition is introduced with the keyword
\texttt{let}. In our case, it introduces a function with two arguments,
an array \texttt{a} and its size \texttt{n}:
\begin{whycode}
  let max_sum (a: array int) (n: int) = ...
\end{whycode}
(There is a function \texttt{length} to get the size of an array but
we add this extra parameter \texttt{n} to stay close to the original
problem statement.) The function body is a Hoare triple, that is a
precondition, a program expression, and a postcondition.
\begin{whycode}
  let max_sum (a: array int) (n: int)
    requires { 0 <= n = length a }
    requires { forall i:int. 0 <= i < n -> a[i] >= 0 }
    ensures  { let (sum, max) = result in sum <= n * max }
  = ... expression ...
\end{whycode}
The first precondition expresses that \texttt{n} is non-negative and is
equal to the length of \texttt{a} (this will be needed for
verification conditions related to array bound checking).
The second precondition expresses that all
elements of \texttt{a} are non-negative.
The postcondition assumes that the value returned by the function,
denoted \texttt{result}, is a pair of integers, and decomposes it as
the pair \texttt{(sum, max)} to express the required property.
The same postcondition can be written in another form, doing the
pattern matching immediately:
\begin{whycode}
    returns { sum, max -> sum <= n * max }
\end{whycode}

We are now left with the function body itself, that is a code
computing the sum and the maximum of all elements in \texttt{a}. With
no surprise, it is as simple as introducing two local references
\begin{whycode}
    let sum = ref 0 in
    let max = ref 0 in
\end{whycode}
scanning the array with a \texttt{for} loop, updating \texttt{max}
and \texttt{sum}
\begin{whycode}
    for i = 0 to n - 1 do
      if !max < a[i] then max := a[i];
      sum := !sum + a[i]
    done;
\end{whycode}
and finally returning the pair of the values contained in \texttt{sum}
and \texttt{max}:
\begin{whycode}
  (!sum, !max)
\end{whycode}
This completes the code for function \texttt{max\_sum}.
As such, it cannot be proved correct, since the loop is still lacking
a loop invariant. In this case, the loop invariant is as simple as
\verb|!sum <= i * !max|, since the postcondition only requires to prove
\verb|sum <= n * max|. The loop invariant is introduced with the
keyword \texttt{invariant}, immediately after the keyword \texttt{do}.
\begin{whycode}
    for i = 0 to n - 1 do
      invariant { !sum <= i * !max }
      ...
    done
\end{whycode}
There is no need to introduce a variant, as the termination of a
\texttt{for} loop is automatically guaranteed.
This completes module \texttt{MaxAndSum}.
%BEGIN LATEX
Figure~\ref{fig:MaxAndSum} shows the whole code.
\begin{figure}
  \centering
%END LATEX
%HEVEA The whole code is shown below.
\begin{whycode}
module MaxAndSum

  use import int.Int
  use import ref.Ref
  use import array.Array

  let max_sum (a: array int) (n: int)
    requires { 0 <= n = length a }
    requires { forall i:int. 0 <= i < n -> a[i] >= 0 }
    returns  { sum, max -> sum <= n * max }
  = let sum = ref 0 in
    let max = ref 0 in
    for i = 0 to n - 1 do
      invariant { !sum <= i * !max }
      if !max < a[i] then max := a[i];
      sum := !sum + a[i]
    done;
    (!sum, !max)

end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 1}
  \label{fig:MaxAndSum}
\end{figure}
%END LATEX
We can now proceed to its verification.
Running \texttt{why3}, or better \texttt{why3ide}, on file
\verb|max_sum.mlw| will show a single verification condition with name
\verb|WP_parameter_max_sum|.
Discharging this verification condition with an automated theorem
prover will not succeed, most likely, as it involves non-linear
arithmetic. Repeated applications of goal splitting and calls to
SMT solvers (within \texttt{why3ide}) will typically leave a single,
unsolved goal, which reduces to proving the following sequent:
\begin{displaymath}
  s \le i \times max, ~ max < a[i] \vdash s + a[i] \le (i+1) \times a[i].
\end{displaymath}
This is easily discharged using an interactive proof assistant such as
Coq, and thus completes the verification.

\section{Problem 2: Inverting an Injection}

The second problem is stated as follows:
\begin{quote}
  Invert an injective array $A$ on $N$ elements in the
  subrange from $0$ to $N - 1$, \ie the output array $B$ must be
  such that $B[A[i]] = i$ for $0 \le i < N$.
\end{quote}
We may assume that $A$ is surjective and we have to prove
that the resulting array is also injective.
The code is immediate, since it is as simple as
\begin{whycode}
    for i = 0 to n - 1 do b[a[i]] <- i done
\end{whycode}
so it is more a matter of specification and of getting the proof done
with as much automation as possible. In a new file, we start a new
module and we import arithmetic and arrays:
\begin{whycode}
module InvertingAnInjection
  use import int.Int
  use import array.Array
\end{whycode}
It is convenient to introduce predicate definitions for the properties
of being injective and surjective. These are purely logical
declarations:
\begin{whycode}
  predicate injective (a: array int) (n: int) =
    forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]

  predicate surjective (a: array int) (n: int) =
    forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
\end{whycode}
It is also convenient to introduce the predicate ``being in the
subrange from 0 to $n-1$'':
\begin{whycode}
  predicate range (a: array int) (n: int) =
    forall i: int. 0 <= i < n -> 0 <= a[i] < n
\end{whycode}
Using these predicates, we can formulate the assumption that any
injective array of size $n$ within the range $0..n-1$ is also surjective:
\begin{whycode}
  lemma injective_surjective:
    forall a: array int, n: int.
      injective a n -> range a n -> surjective a n
\end{whycode}
We declare it as a lemma rather than as an axiom, since it is actually
provable. It requires induction and can be proved using the Coq proof
assistant for instance.
Finally we can give the code a specification, with a loop invariant
which simply expresses the values assigned to array \texttt{b} so far:
\begin{whycode}
  let inverting (a: array int) (b: array int) (n: int)
    requires { 0 <= n = length a = length b }
    requires { injective a n /\ range a n }
    ensures  { injective b n }
  = for i = 0 to n - 1 do
      invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
      b[a[i]] <- i
    done
\end{whycode}
Here we chose to have array \texttt{b} as argument; returning a
freshly allocated array would be equally simple.
%BEGIN LATEX
The whole module is given in Figure~\ref{fig:Inverting}.
%END LATEX
%HEVEA The whole module is given below.
The verification conditions for function \texttt{inverting} are easily
discharged automatically, thanks to the lemma.
%BEGIN LATEX
\begin{figure}
  \centering
%END LATEX
\begin{whycode}
module InvertingAnInjection

  use import int.Int
  use import array.Array

  predicate injective (a: array int) (n: int) =
    forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]

  predicate surjective (a: array int) (n: int) =
    forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)

  predicate range (a: array int) (n: int) =
    forall i: int. 0 <= i < n -> 0 <= a[i] < n

  lemma injective_surjective:
    forall a: array int, n: int.
      injective a n -> range a n -> surjective a n

  let inverting (a: array int) (b: array int) (n: int)
    requires { 0 <= n = length a = length b }
    requires { injective a n /\ range a n }
    ensures  { injective b n }
  = for i = 0 to n - 1 do
      invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
      b[a[i]] <- i
    done

end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 2}
  \label{fig:Inverting}
\end{figure}
%END LATEX

\section{Problem 3: Searching a Linked List}

The third problem is stated as follows:
\begin{quote}
  Given a linked list representation of a list of integers,
  find the index of the first element that is equal to 0.
\end{quote}
More precisely, the specification says
\begin{quote}
  You have to show that the program returns an index $i$ equal to the
  length of the list if there is no such element. Otherwise, the $i$-th
  element of the list must be equal to 0, and all the preceding
  elements must be non-zero.
\end{quote}
Since the list is not mutated, we can use the algebraic data type of
polymorphic lists from \why's standard library, defined in theory
\texttt{list.List}. It comes with other handy theories:
\texttt{list.Length}, which provides a function \texttt{length}, and
\texttt{list.Nth}, which provides a function \texttt{nth}
for the $n$-th element of a list. The latter returns an option type,
depending on whether the index is meaningful or not.
\begin{whycode}
module SearchingALinkedList
  use import int.Int
  use export list.List
  use export list.Length
  use export list.Nth
\end{whycode}
It is helpful to introduce two predicates: a first one
for a successful search,
\begin{whycode}
  predicate zero_at (l: list int) (i: int) =
    nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0
\end{whycode}
and another for a non-successful search,
\begin{whycode}
  predicate no_zero (l: list int) =
    forall j:int. 0 <= j < length l -> nth j l <> Some 0
\end{whycode}
We are now in position to give the code for the search function.
We write it as a recursive function \texttt{search} that scans a list
for the first zero value:
\begin{whycode}
  let rec search (i: int) (l: list int) =
    match l with
    | Nil      -> i
    | Cons x r -> if x = 0 then i else search (i+1) r
    end
\end{whycode}
Passing an index \texttt{i} as first argument allows to perform a tail
call. A simpler code (yet less efficient) would return 0 in the first
branch and \texttt{1 + search ...} in the second one, avoiding the
extra argument \texttt{i}.

We first prove the termination of this recursive function. It amounts
to give it a \emph{variant}, that is a value that strictly decreases
at each recursive call with respect to some well-founded ordering.
Here it is as simple as the list \texttt{l} itself:
\begin{whycode}
  let rec search (i: int) (l: list int) variant { l } = ...
\end{whycode}
It is worth pointing out that variants are not limited to values
of algebraic types. A non-negative integer term (for example,
\texttt{length l}) can be used, or a term of any other type
equipped with a well-founded order relation.
Several terms can be given, separated with commas,
for lexicographic ordering.

There is no precondition for function \texttt{search}.
The postcondition expresses that either a zero value is found, and
consequently the value returned is bounded accordingly,
\begin{whycode}
  i <= result < i + length l /\ zero_at l (result - i)
\end{whycode}
or no zero value was found, and thus the returned value is exactly
\texttt{i} plus the length of \texttt{l}:
\begin{whycode}
  result = i + length l /\ no_zero l
\end{whycode}
Solving the problem is simply a matter of calling \texttt{search} with
0 as first argument.
%BEGIN LATEX
The code is given Figure~\ref{fig:LinkedList}.
%END LATEX
%HEVEA The code is given below.
The verification conditions are all discharged automatically.
%BEGIN LATEX
\begin{figure}
  \centering
%END LATEX
\begin{whycode}
module SearchingALinkedList

  use import int.Int
  use export list.List
  use export list.Length
  use export list.Nth

  predicate zero_at (l: list int) (i: int) =
    nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0

  predicate no_zero (l: list int) =
    forall j:int. 0 <= j < length l -> nth j l <> Some 0

  let rec search (i: int) (l: list int) variant { l }
    ensures { (i <= result < i + length l /\ zero_at l (result - i))
           \/ (result = i + length l /\ no_zero l) }
  = match l with
    | Nil -> i
    | Cons x r -> if x = 0 then i else search (i+1) r
    end

  let search_list (l: list int)
    ensures { (0 <= result < length l /\ zero_at l result)
           \/ (result = length l /\ no_zero l) }
  = search 0 l

end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 3}
  \label{fig:LinkedList}
\end{figure}
%END LATEX

Alternatively, we can implement the search with a \texttt{while} loop.
To do this, we need to import references from the standard library,
together with theory \texttt{list.HdTl} which defines functions
\texttt{hd} and \texttt{tl} over lists.
\begin{whycode}
  use import ref.Ref
  use import list.HdTl
\end{whycode}
Being partial functions, \texttt{hd} and \texttt{tl} return options.
For the purpose of our code, though, it is simpler to have functions
which do not return options, but have preconditions instead. Such a
function \texttt{head} is defined as follows:
\begin{whycode}
  let head (l: list 'a)
    requires { l <> Nil } ensures { hd l = Some result }
  = match l with Nil -> absurd | Cons h _ -> h end
\end{whycode}
The program construct \texttt{absurd} denotes an unreachable piece of
code. It generates the verification condition \texttt{false}, which is
here provable using the precondition (the list cannot be \texttt{Nil}).
Function \texttt{tail} is defined similarly:
\begin{whycode}
  let tail (l : list 'a)
    requires { l <> Nil } ensures { tl l = Some result }
  = match l with Nil -> absurd | Cons _ t -> t end
\end{whycode}
Using \texttt{head} and \texttt{tail}, it is straightforward to
implement the search as a \texttt{while} loop.
It uses a local reference \texttt{i} to store the index and another
local reference \texttt{s} to store the list being scanned.
As long as \texttt{s} is not empty and its head is not zero, it
increments \texttt{i} and advances in \texttt{s} using function \texttt{tail}.
\begin{whycode}
  let search_loop l =
    ensures { ... same postcondition as in search_list ... }
  = let i = ref 0 in
    let s = ref l in
    while !s <> Nil && head !s <> 0 do
      invariant { ... }
      variant   { !s }
      i := !i + 1;
      s := tail !s
    done;
    !i
\end{whycode}
The postcondition is exactly the same as for function \verb|search_list|.
The termination of the \texttt{while} loop is ensured using a variant,
exactly as for a recursive function. Such a variant must strictly decrease at
each execution of the loop body. The reader is invited to figure out
the loop invariant.

\section{Problem 4: N-Queens}

The fourth problem is probably the most challenging one.
We have to verify the implementation of a program which solves the
$N$-queens puzzle: place $N$ queens on an $N \times N$
chess board so that no queen can capture another one with a
legal move.
The program should return a placement if there is a solution and
indicates that there is no solution otherwise. A placement is a
$N$-element array which assigns the queen on row $i$ to its column.
Thus we start our module by importing arithmetic and arrays:
\begin{whycode}
module NQueens
  use import int.Int
  use import array.Array
\end{whycode}
The code is a simple backtracking algorithm, which tries to put a queen
on each row of the chess board, one by one (there is basically no
better way to solve the $N$-queens puzzle).
A building block is a function which checks whether the queen on a
given row may attack another queen on a previous row. To verify this
function, we first define a more elementary predicate, which expresses
that queens on row \texttt{pos} and \texttt{q} do no attack each other:
\begin{whycode}
  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
\end{whycode}
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
\end{whycode}
Implementing a function which decides this predicate is another
matter. In order for it to be efficient, we want to return
\texttt{False} as soon as a queen attacks the queen on row
\texttt{pos}. We use an exception for this purpose and it carries the
row of the attacking queen:
\begin{whycode}
  exception Inconsistent int
\end{whycode}
The check is implemented by a function \verb|check_is_consistent|,
which takes the board and the row \texttt{pos} as arguments, and scans
rows from 0 to \texttt{pos-1} looking for an attacking queen. As soon
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)
    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
\end{whycode}
The assertion in the exception handler is a cut for SMT solvers.
%BEGIN LATEX
This first part of the solution is given in Figure~\ref{fig:NQueens1}.
%END LATEX
%HEVEA This first part of the solution is given below.
%BEGIN LATEX
\begin{figure}
  \centering
%END LATEX
\begin{whycode}
module NQueens
  use import int.Int
  use import array.Array

  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

  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
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 4 (1/2)}
  \label{fig:NQueens1}
\end{figure}
%END LATEX

We now proceed with the verification of the backtracking algorithm.
The specification requires us to define the notion of solution, which
is straightforward using the predicate \verb|is_consistent| above.
However, since the algorithm will try to complete a given partial
solution, it is more convenient to define the notion of partial
solution, up to a given row. It is even more convenient to split it in
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

  predicate solution (board: array int) (pos: int) =
    is_board board pos /\
    forall q:int. 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
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]
\end{whycode}
The search itself makes use of an exception to signal a successful search:
\begin{whycode}
  exception Solution
\end{whycode}
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 }
\end{whycode}
The precondition relates \texttt{board}, \texttt{pos}, and \texttt{n}
and requires \texttt{board} to be a solution up to \texttt{pos}:
\begin{whycode}
    requires { 0 <= pos <= n = length board }
    requires { solution board pos }
\end{whycode}
The postcondition is twofold: either the function exits normally and
then there is no solution extending the prefix in \texttt{board},
which has not been modified;
or the function raises \texttt{Solution} and we have a solution in
\texttt{board}.
\begin{whycode}
    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 }
  = '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}
    if pos = n then raise Solution;
\end{whycode}
Otherwise we scan all possible positions for the queen on row
\texttt{pos} with a \texttt{for} loop:
\begin{whycode}
    for i = 0 to n - 1 do
\end{whycode}
The loop invariant states that we have not modified the solution
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 { 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}
Then we assign column \texttt{i} to the queen on row \texttt{pos} and
we check for a possible attack with \verb|check_is_consistent|. If
not, we call \verb|bt_queens| recursively on the next row.
\begin{whycode}
      board[pos] <- i;
      if check_is_consistent board pos then bt_queens board n (pos + 1)
    done
\end{whycode}
This completes the loop and function \verb|bt_queens| as well.
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 }
    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
\end{whycode}
%BEGIN LATEX
This second part of the solution is given Figure~\ref{fig:NQueens2}.
%END LATEX
%HEVEA This second part of the solution is given below.
With the help of a few auxiliary lemmas --- not given here but available
from \why's sources --- the verification conditions are all discharged
automatically, including the verification of the lemmas themselves.
%BEGIN LATEX
\begin{figure}
  \centering
%END LATEX
\begin{whycode}
  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

  predicate eq_board (b1 b2: array int) (pos: int) =
    forall q:int. 0 <= q < pos -> b1[q] = b2[q]

  exception Solution

  let rec bt_queens (board: array int) (n: int) (pos: int)
    variant  { n - pos }
    requires { 0 <= pos <= n = length board }
    requires { solution board pos }
    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 }
  = 'Init:
    if pos = n then raise Solution;
    for i = 0 to n - 1 do
      invariant { eq_board board (at board 'Init) 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 }
    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

end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 4 (2/2)}
  \label{fig:NQueens2}
\end{figure}
%END LATEX

\section{Problem 5: Amortized Queue}

The last problem consists in verifying the implementation of a
well-known purely applicative data structure for queues.
A queue is composed of two lists, \textit{front} and \textit{rear}.
We push elements at the head of list \textit{rear} and pop them off
the head of list \textit{front}. We maintain that the length of
\textit{front} is always greater or equal to the length of \textit{rear}.
(See for instance Okasaki's \emph{Purely Functional Data
  Structures}~\cite{okasaki98} for more details.)

We have to implement operations \texttt{empty}, \texttt{head},
\texttt{tail}, and \texttt{enqueue} over this data type,
to show that the invariant over lengths is maintained, and finally
\begin{quote}
  to show that a client invoking these operations
  observes an abstract queue given by a sequence.
\end{quote}
In a new module, we import arithmetic and theory
\texttt{list.ListRich}, a combo theory that imports all list
operations we will require: length, reversal, and concatenation.
\begin{whycode}
module AmortizedQueue
  use import int.Int
  use export list.ListRich
\end{whycode}
The queue data type is naturally introduced as a polymorphic record type.
The two list lengths are explicitly stored, for better efficiency.
\begin{whycode}
  type queue 'a = { front: list 'a; lenf: int;
                    rear : list 'a; lenr: int; }
  invariant {
    length self.front = self.lenf >= length self.rear = self.lenr }
\end{whycode}
The type definition is accompanied with an invariant ---
a logical property imposed on any value of the type.
\why assumes that any \texttt{queue} passed as an argument to
a program function satisfies the invariant and it produces
a proof obligation every time a \texttt{queue} is created
or modified in a program.

For the purpose of the specification, it is convenient to introduce a function
\texttt{sequence} which builds the sequence of elements of a queue, that
is the front list concatenated to the reversed rear list.
\begin{whycode}
  function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear
\end{whycode}
It is worth pointing out that this function will only be used in
specifications.
We start with the easiest operation: building the empty queue.
\begin{whycode}
  let empty () ensures { sequence result = Nil }
  = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a
\end{whycode}
The postcondition states that the returned queue represents
the empty sequence. Another postcondition, saying that the
returned queue satisfies the type invariant, is implicit.
Note the cast to type \texttt{queue 'a}. It is required, for the
type checker not to complain about an undefined type variable.

The next operation is \texttt{head}, which returns the first element from
a given queue \texttt{q}. It naturally requires the queue to be non
empty, which is conveniently expressed as \texttt{sequence q} not
being \texttt{Nil}.
\begin{whycode}
  let head (q: queue 'a)
    requires { sequence q <> Nil }
    ensures { hd (sequence q) = Some result }
  = match q.front with
      | Nil      -> absurd
      | Cons x _ -> x
    end
\end{whycode}
That the argument \texttt{q} satisfies the type invariant is
implicitly assumed. The type invariant is
required to prove the absurdity of the first branch (if
\texttt{q.front} is \texttt{Nil}, then so should be \texttt{sequence q}).

The next operation is \texttt{tail}, which removes the first element
from a given queue. This is more subtle than \texttt{head}, since we
may have to re-structure the queue to maintain the invariant.
Since we will have to perform a similar operation when implementation
operation \texttt{enqueue}, it is a good idea to introduce a smart
constructor \texttt{create} which builds a queue from two lists, while
ensuring the invariant. The list lengths are also passed as arguments,
to avoid unnecessary computations.
\begin{whycode}
  let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
    requires { lf = length f /\ lr = length r }
    ensures  { sequence result = f ++ reverse r }
  = if lf >= lr then
      { front = f; lenf = lf; rear = r; lenr = lr }
    else
      let f = f ++ reverse r in
      { front = f; lenf = lf + lr; rear = Nil; lenr = 0 }
\end{whycode}
If the invariant already holds, it is simply a matter of building the
record. Otherwise, we empty the rear list and build a new front list
as the concatenation of list \texttt{f} and the reversal of list \texttt{r}.
The principle of this implementation is that the cost of this reversal
will be amortized over all queue operations. Implementing function
\texttt{tail} is now straightforward and follows the structure of
function \texttt{head}.
\begin{whycode}
  let tail (q: queue 'a)
    requires { sequence q <> Nil }
    ensures  { tl (sequence q) = Some (sequence result) }
  = match q.front with
      | Nil      -> absurd
      | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
    end
\end{whycode}
The last operation is \texttt{enqueue}, which pushes a new element in
a given queue. Reusing the smart constructor \texttt{create} makes it
a one line code.
\begin{whycode}
  let enqueue (x: 'a) (q: queue 'a)
    ensures { sequence result = sequence q ++ Cons x Nil }
  = create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
\end{whycode}
%BEGIN LATEX
The code is given Figure~\ref{fig:AQueue}.
%END LATEX
%HEVEA The code is given below.
The verification conditions are all discharged automatically.
%BEGIN LATEX
\begin{figure}[p]
  \centering
%END LATEX
\begin{whycode}
module AmortizedQueue
  use import int.Int
  use export list.ListRich

  type queue 'a = { front: list 'a; lenf: int;
                    rear : list 'a; lenr: int; }
  invariant {
    length self.front = self.lenf >= length self.rear = self.lenr }

  function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear

  let empty () ensures { sequence result = Nil }
  = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a

  let head (q: queue 'a)
    requires { sequence q <> Nil }
    ensures { hd (sequence q) = Some result }
  = match q.front with
      | Nil      -> absurd
      | Cons x _ -> x
    end

  let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
    requires { lf = length f /\ lr = length r }
    ensures  { sequence result = f ++ reverse r }
  = if lf >= lr then
      { front = f; lenf = lf; rear = r; lenr = lr }
    else
      let f = f ++ reverse r in
      { front = f; lenf = lf + lr; rear = Nil; lenr = 0 }

  let tail (q: queue 'a)
    requires { sequence q <> Nil }
    ensures  { tl (sequence q) = Some (sequence result) }
  = match q.front with
      | Nil      -> absurd
      | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
    end

  let enqueue (x: 'a) (q: queue 'a)
    ensures { sequence result = sequence q ++ Cons x Nil }
  = create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
  \caption{Solution for VSTTE'10 competition problem 5}
  \label{fig:AQueue}
\end{figure}
%END LATEX

% other examples: same fringe ?

%%% Local Variables:
%%% compile-command: "make -C .. doc"
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:

% LocalWords:  surjective