From 2bf65706bd5592aa093240c49be88591ff9e0ad1 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 21 Sep 2012 17:44:20 +0200
Subject: [PATCH] Add syntactic coloring to some listings of the documentation.

---
 doc/whyml.tex | 547 +++++++++++++++++++++++++-------------------------
 1 file changed, 274 insertions(+), 273 deletions(-)

diff --git a/doc/whyml.tex b/doc/whyml.tex
index e5d896b3b..65217c7ca 100644
--- a/doc/whyml.tex
+++ b/doc/whyml.tex
@@ -65,21 +65,21 @@ and we have to prove the following postcondition:
   sum \le N \times max.
 \end{displaymath}
 In a file \verb|max_sum.mlw|, we start a new module:
-\begin{verbatim}
-  module MaxAndSum
-\end{verbatim}
+\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{verbatim}
-    use import int.Int
-\end{verbatim}
+\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{verbatim}
-    use import module ref.Ref
-    use import module array.Array
-\end{verbatim}
+\begin{whycode}
+  use import module ref.Ref
+  use import module array.Array
+\end{whycode}
 The additional keyword \texttt{module} means that we are looking for
 \texttt{.mlw} files from the standard library (namely \texttt{ref.mlw}
 and \texttt{array.mlw} here), instead of \texttt{.why} files.
@@ -92,19 +92,19 @@ 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{verbatim}
-    let max_sum (a: array int) (n: int) = ...
-\end{verbatim}
+\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{verbatim}
-    let max_sum (a: array int) (n: int) =
-      { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
-       ... expression ...
-      { let (sum, max) = result in sum <= n * max }
-\end{verbatim}
+\begin{whycode}
+  let max_sum (a: array int) (n: int) =
+    { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
+     ... expression ...
+    { let (sum, max) = result in sum <= n * max }
+\end{whycode}
 The 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), and that all
@@ -116,42 +116,42 @@ the pair \texttt{(sum, max)} to express the required property.
 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 surpise, it is as simple as introducing two local references
-\begin{verbatim}
+\begin{whycode}
     let sum = ref 0 in
     let max = ref 0 in
-\end{verbatim}
+\end{whycode}
 scanning the array with a \texttt{for} loop, updating \texttt{max}
 and \texttt{sum}
-\begin{verbatim}
+\begin{whycode}
     for i = 0 to n - 1 do
       if !max < a[i] then max := a[i];
       sum := !sum + a[i]
     done;
-\end{verbatim}
+\end{whycode}
 and finally returning the pair of the values contained in \texttt{sum}
 and \texttt{max}:
-\begin{verbatim}
-    (!sum, !max)
-\end{verbatim}
+\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{verbatim}
-      for i = 0 to n - 1 do
-        invariant { !sum <= i * !max }
-        ...
-      done
-\end{verbatim}
+\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}.
 Figure~\ref{fig:MaxAndSum} shows the whole code.
 \begin{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
 module MaxAndSum
 
   use import int.Int
@@ -171,7 +171,7 @@ module MaxAndSum
     { let (sum, max) = result in sum <= n * max }
 
 end
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 1.}
   \label{fig:MaxAndSum}
@@ -202,54 +202,54 @@ The second problem is stated as follows:
 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{verbatim}
+\begin{whycode}
     for i = 0 to n - 1 do b[a[i]] <- i done
-\end{verbatim}
+\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{verbatim}
-  module InvertingAnInjection
-    use import int.Int
-    use import module array.Array
-\end{verbatim}
+\begin{whycode}
+module InvertingAnInjection
+  use import int.Int
+  use import module 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{verbatim}
-    predicate injective (a: array int) (n: int) =
-      forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
+\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{verbatim}
+  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{verbatim}
-    predicate range (a: array int) (n: int) =
-      forall i: int. 0 <= i < n -> 0 <= a[i] < n
-\end{verbatim}
+\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{verbatim}
-    lemma injective_surjective:
-      forall a: array int, n: int.
-      injective a n -> range a n -> surjective a n
-\end{verbatim}
+\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{verbatim}
-    let inverting (a: array int) (b: array int) (n: int) =
-      { 0 <= n = length a = length b /\ injective a n /\ range a n }
-      for i = 0 to n - 1 do
-        invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
-        b[a[i]] <- i
-      done
-      { injective b n }
-\end{verbatim}
+\begin{whycode}
+  let inverting (a: array int) (b: array int) (n: int) =
+    { 0 <= n = length a = length b /\ injective a n /\ range a n }
+    for i = 0 to n - 1 do
+      invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
+      b[a[i]] <- i
+    done
+    { injective b n }
+\end{whycode}
 Here we chose to have array \texttt{b} as argument; returning a
 freshly allocated array would be equally simple.
 The whole module is given Figure~\ref{fig:Inverting}.
@@ -257,7 +257,7 @@ The verification conditions for function \texttt{inverting} are easily
 discharged automatically, thanks to the lemma.
 \begin{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
 module InvertingAnInjection
 
   use import int.Int
@@ -285,7 +285,7 @@ module InvertingAnInjection
     { injective b n }
 
 end
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 2.}
   \label{fig:Inverting}
@@ -312,33 +312,34 @@ polymorphic lists from \why's standard library, defined in theory
 \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{verbatim}
-  module SearchingALinkedList
-    use import int.Int
-    use export list.List
-    use export list.Length
-    use export list.Nth
-\end{verbatim}
+\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{verbatim}
-    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{verbatim}
+\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{verbatim}
-    predicate no_zero (l: list int) =
-      forall j:int. 0 <= j < length l -> nth j l <> Some 0
-\end{verbatim}
+\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{verbatim}
-    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{verbatim}
+\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
@@ -348,30 +349,30 @@ We first prove the termination of this recursive function. It amounts
 to give it a \emph{variant}, that is an term integer term which stays
 non-negative and strictly decreases at each recursive call. Here it is
 as simple as the length of \texttt{l}:
-\begin{verbatim}
-    let rec search (i: int) (l: list int) variant { length l } = ...
-\end{verbatim}
+\begin{whycode}
+  let rec search (i: int) (l: list int) variant { length l } = ...
+\end{whycode}
 (It is worth pointing out that variants are not limited to natural
 numbers. Any other type equipped with a well-founded order relation
 can be used instead.)
 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{verbatim}
+\begin{whycode}
   i <= result < i + length l /\ zero_at l (result - i)
-\end{verbatim}
+\end{whycode}
 or no zero value was found, and thus the returned value is exactly
 \texttt{i} plus the length of \texttt{l}:
-\begin{verbatim}
+\begin{whycode}
   result = i + length l /\ no_zero l
-\end{verbatim}
+\end{whycode}
 Solving the problem is simply a matter of calling \texttt{search} with
 0 as first argument.
 The code is given Figure~\ref{fig:LinkedList}. The verification
 conditions are all discharged automatically.
 \begin{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
 module SearchingALinkedList
 
   use import int.Int
@@ -403,7 +404,7 @@ module SearchingALinkedList
       (result = length l /\ no_zero l) }
 
 end
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 3.}
   \label{fig:LinkedList}
@@ -413,50 +414,50 @@ 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 function
 \texttt{hd} and \texttt{tl} over lists.
-\begin{verbatim}
-    use import module ref.Ref
-    use import list.HdTl
-\end{verbatim}
+\begin{whycode}
+  use import module 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{verbatim}
-    let head (l: list 'a) =
-      { l <> Nil }
-      match l with Nil -> absurd | Cons h _ -> h end
-      { hd l = Some result }
-\end{verbatim}
+\begin{whycode}
+  let head (l: list 'a) =
+    { l <> Nil }
+    match l with Nil -> absurd | Cons h _ -> h end
+    { hd l = Some result }
+\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{verbatim}
-    let tail (l : list 'a) =
-      { l <> Nil }
-      match l with Nil -> absurd | Cons _ t -> t end
-      { tl l = Some result }
-\end{verbatim}
+\begin{whycode}
+  let tail (l : list 'a) =
+    { l <> Nil }
+    match l with Nil -> absurd | Cons _ t -> t end
+    { tl l = Some result }
+\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{verbatim}
-    let search_loop l =
-      { }
-      let i = ref 0 in
-      let s = ref l in
-      while !s <> Nil && head !s <> 0 do
-        invariant { ... }
-        variant   { length !s }
-        i := !i + 1;
-        s := tail !s
-      done;
-      !i
-      { ... same postcondition as search_list ... }
-\end{verbatim}
+\begin{whycode}
+  let search_loop l =
+    { }
+    let i = ref 0 in
+    let s = ref l in
+    while !s <> Nil && head !s <> 0 do
+      invariant { ... }
+      variant   { length !s }
+      i := !i + 1;
+      s := tail !s
+    done;
+    !i
+    { ... same postcondition as search_list ... }
+\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
@@ -474,11 +475,11 @@ 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{verbatim}
-  module NQueens
-    use import int.Int
-    use import module array.Array
-\end{verbatim}
+\begin{whycode}
+module NQueens
+  use import int.Int
+  use import module 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).
@@ -486,58 +487,58 @@ 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{verbatim}
-    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{verbatim}
+\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{verbatim}
-    predicate is_consistent (board: array int) (pos: int) =
-      forall q:int. 0 <= q < pos -> consistent_row board pos q
-\end{verbatim}
+\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{verbatim}
-    exception Inconsistent int
-\end{verbatim}
+\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{verbatim}
-    let check_is_consistent (board: array int) (pos: int) =
-      { 0 <= pos < length board }
-      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
-      { result=True <-> is_consistent board pos }
-\end{verbatim}
+\begin{whycode}
+  let check_is_consistent (board: array int) (pos: int) =
+    { 0 <= pos < length board }
+    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
+    { result=True <-> is_consistent board pos }
+\end{whycode}
 The assertion in the exception handler is a cut for SMT solvers.
 This first part of the solution is given Figure~\ref{fig:NQueens1}.
 \begin{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
 module NQueens
   use import int.Int
   use import module array.Array
@@ -571,7 +572,7 @@ module NQueens
       False
     end
     { result=True <-> is_consistent board pos }
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 4 (1/2).}
   \label{fig:NQueens1}
@@ -585,101 +586,101 @@ 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{verbatim}
-    predicate is_board (board: array int) (pos: int) =
-      forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
+\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{verbatim}
+  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{verbatim}
-    predicate eq_board (b1 b2: array int) (pos: int) =
-      forall q:int. 0 <= q < pos -> b1[q] = b2[q]
-\end{verbatim}
+\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{verbatim}
-    exception Solution
-\end{verbatim}
+\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{verbatim}
-    let rec bt_queens (board: array int) (n: int) (pos: int) 
-                      variant {n-pos} =
-\end{verbatim}
+\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{verbatim}
-      { length board = n /\ 0 <= pos <= n /\ solution board pos }
-      'Init:
-\end{verbatim}
+\begin{whycode}
+    { length board = n /\ 0 <= pos <= n /\ solution board pos }
+    'Init:
+\end{whycode}
 We place a code mark \texttt{'Init} immediately after the precondition 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{verbatim}
-      if pos = n then raise Solution;
-\end{verbatim}
+\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{verbatim}
-      for i = 0 to n - 1 do
-\end{verbatim}
+\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{verbatim}
-        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) }
-\end{verbatim}
+\begin{whycode}
+      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) }
+\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{verbatim}
-        board[pos] <- i;
-        if check_is_consistent board pos then bt_queens board n (pos + 1)
-      done
-\end{verbatim}
+\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.
 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{verbatim}
-      { 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) }
-      | Solution ->
-      { solution board n }
-\end{verbatim}
+\begin{whycode}
+    { 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) }
+    | Solution ->
+    { solution board n }
+\end{whycode}
 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{verbatim}
-    let queens (board: array int) (n: int) =
-      { 0 <= length board = n }
-      bt_queens board n 0
-      { forall b:array int. length b = n -> is_board b n ->
-                              not (solution b n) }
-      | Solution -> { solution board n }
-\end{verbatim}
+\begin{whycode}
+  let queens (board: array int) (n: int) =
+    { 0 <= length board = n }
+    bt_queens board n 0
+    { forall b:array int. length b = n -> is_board b n ->
+                            not (solution b n) }
+    | Solution -> { solution board n }
+\end{whycode}
 This second part of the solution is given Figure~\ref{fig:NQueens2}.
 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{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
   predicate is_board (board: array int) (pos: int) =
     forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
 
@@ -720,7 +721,7 @@ automatically, including the verification of the lemmas themselves.
                             not (solution b n) }
     | Solution -> { solution board n }
 end
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 4 (2/2).}
   \label{fig:NQueens2}
@@ -748,40 +749,40 @@ to show that the invariant over lengths is maintained, and finally
 In a new module, we import arithmetic and theory
 \texttt{list.ListRich}, a combo theory which imports all list
 operations we will require: length, reversal, and concatenation.
-\begin{verbatim}
-  module AmortizedQueue
-    use import int.Int
-    use export list.ListRich
-\end{verbatim}
+\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{verbatim}
-    type queue 'a = {| front: list 'a; lenf: int;
-                       rear : list 'a; lenr: int; |}
-\end{verbatim}
+\begin{whycode}
+  type queue 'a = {| front: list 'a; lenf: int;
+                     rear : list 'a; lenr: int; |}
+\end{whycode}
 We start with the definition of the data type invariant, as a
 predicate \texttt{inv}. It makes use of the ability to chain
 several equalities and inequalities.
-\begin{verbatim}
-    predicate inv (q: queue 'a) =
-      length q.front = q.lenf >= length q.rear = q.lenr
-\end{verbatim}
+\begin{whycode}
+  predicate inv (q: queue 'a) =
+    length q.front = q.lenf >= length q.rear = q.lenr
+\end{whycode}
 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 reversed rear list.
-\begin{verbatim}
-    function sequence (q: queue 'a) : list 'a =
-      q.front ++ reverse q.rear
-\end{verbatim}
+\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{verbatim}
+\begin{whycode}
   let empty () =
     {}
     {| front = Nil; lenf = 0; rear = Nil; lenr = 0 |} : queue 'a
     { inv result /\ sequence result = Nil }
-\end{verbatim}
+\end{whycode}
 The postcondition is twofold: the returned queue satisfies its
 invariant and represents the empty sequence.
 Note the cast to type \texttt{queue 'a}. It is required, for the
@@ -791,7 +792,7 @@ 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{verbatim}
+\begin{whycode}
   let head (q: queue 'a) =
     { inv q /\ sequence q <> Nil }
     match q.front with
@@ -799,7 +800,7 @@ being \texttt{Nil}.
       | Cons x _ -> x
     end
     { hd (sequence q) = Some result }
-\end{verbatim}
+\end{whycode}
 Note the presence of the invariant in the precondition, which is
 required to prove the absurdity of the first branch (if
 \texttt{q.front} is \texttt{Nil}, then so should be \texttt{sequence q}).
@@ -812,16 +813,16 @@ 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{verbatim}
-    let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) =
-      { lf = length f /\ lr = length 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 |}
-      { inv result /\ sequence result = f ++ reverse r }
-\end{verbatim}
+\begin{whycode}
+  let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) =
+    { lf = length f /\ lr = length 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 |}
+    { inv result /\ sequence result = f ++ reverse r }
+\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}.
@@ -829,29 +830,29 @@ 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{verbatim}
-    let tail (q: queue 'a) =
-      { inv q /\ sequence q <> Nil }
-      match q.front with
-        | Nil      -> absurd
-        | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
-      end
-      { inv result /\ tl (sequence q) = Some (sequence result) }
-\end{verbatim}
+\begin{whycode}
+  let tail (q: queue 'a) =
+    { inv q /\ sequence q <> Nil }
+    match q.front with
+      | Nil      -> absurd
+      | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
+    end
+    { inv result /\ tl (sequence q) = Some (sequence result) }
+\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{verbatim}
-    let enqueue (x: 'a) (q: queue 'a) =
-      { inv q }
-      create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
-      { inv result /\ sequence result = sequence q ++ Cons x Nil }
-\end{verbatim}
+\begin{whycode}
+  let enqueue (x: 'a) (q: queue 'a) =
+    { inv q }
+    create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
+    { inv result /\ sequence result = sequence q ++ Cons x Nil }
+\end{whycode}
 The code is given Figure~\ref{fig:AQueue}. The verification conditions
 are all discharged automatically.
 \begin{figure}
   \centering
-\begin{verbatim}
+\begin{whycode}
 module AmortizedQueue
   use import int.Int
   use export list.ListRich
@@ -899,7 +900,7 @@ module AmortizedQueue
     create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
     { inv result /\ sequence result = sequence q ++ Cons x Nil }
 end
-\end{verbatim}
+\end{whycode}
 \vspace*{-2em}\hrulefill
   \caption{Solution for VSTTE'10 competition problem 5.}
   \label{fig:AQueue}
-- 
GitLab