 ### Add syntactic coloring to some listings of the documentation.

parent 964a3f8e
 ... ... @@ -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 ->