Previous Up Next

Chapter 3  The WhyML Programming Language

This chapter describes the WhyML programming language. A WhyML input text contains a list of theories (see Chapter 2) and/or modules. Modules extend theories with programs. Programs can use all types, symbols, and constructs from the logic. They also provide extra features:

Programs are contained in files with suffix .mlw. They are handled by why3. For instance

> why3 prove myfile.mlw

will display the verification conditions extracted from modules in file myfile.mlw, as a set of corresponding theories, and

> why3 prove -P alt-ergo myfile.mlw

will run the SMT solver Alt-Ergo on these verification conditions. Program files are also handled by the GUI tool why3ide. See Chapter 6 for more details regarding command lines.


As an introduction to WhyML, we use the five problems from the VSTTE 2010 verification competition [8]. The source code for all these examples is contained in Why3’s distribution, in sub-directory examples/.

3.1  Problem 1: Sum and Maximum

The first problem is stated as follows:

Given an N-element array of natural numbers, write a program to compute the sum and the maximum of the elements in the array.

We assume N ≥ 0 and a[i] ≥ 0 for 0 ≤ i < N, as precondition, and we have to prove the following postcondition:

  sum ≤ N × max.

In a file max_sum.mlw, we start a new module:

module MaxAndSum

We are obviously needing arithmetic, so we import the corresponding theory, exactly as we would do within a theory definition:

use import int.Int

We are also going to use references and arrays from WhyML’s standard library, so we import the corresponding modules, with a similar declaration:

use import ref.Ref use import array.Array

Modules Ref and Array respectively provide a type ref ’a for references and a type array ’a for arrays, together with useful operations and traditional syntax. They are loaded from the WhyML files ref.mlw and array.mlw in the standard library. Why3 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 .mlw file and in a .why file with the same name.

We are now in position to define a program function max_sum. A function definition is introduced with the keyword let. In our case, it introduces a function with two arguments, an array a and its size n:

let max_sum (a: array int) (n: int) = ...

(There is a function length to get the size of an array but we add this extra parameter 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.

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 ...

The first precondition expresses that n is non-negative and is equal to the length of a (this will be needed for verification conditions related to array bound checking). The second precondition expresses that all elements of a are non-negative. The postcondition assumes that the value returned by the function, denoted result, is a pair of integers, and decomposes it as the pair (sum, max) to express the required property. The same postcondition can be written in another form, doing the pattern matching immediately:

returns { sum, max -> sum <= n * max }

We are now left with the function body itself, that is a code computing the sum and the maximum of all elements in a. With no surprise, it is as simple as introducing two local references

let sum = ref 0 in let max = ref 0 in

scanning the array with a for loop, updating max and sum

for i = 0 to n - 1 do if !max < a[i] then max := a[i]; sum := !sum + a[i] done;

and finally returning the pair of the values contained in sum and max:

(!sum, !max)

This completes the code for function 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 !sum <= i * !max, since the postcondition only requires to prove sum <= n * max. The loop invariant is introduced with the keyword invariant, immediately after the keyword do.

for i = 0 to n - 1 do invariant { !sum <= i * !max } ... done

There is no need to introduce a variant, as the termination of a for loop is automatically guaranteed. This completes module MaxAndSum. The whole code is shown below.

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

We can now proceed to its verification. Running why3, or better why3ide, on file max_sum.mlw will show a single verification condition with name 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 why3ide) will typically leave a single, unsolved goal, which reduces to proving the following sequent:

  s ≤ i × max,   max < a[i] ⊢ s + a[i] ≤ (i+1) × a[i].

This is easily discharged using an interactive proof assistant such as Coq, and thus completes the verification.

3.2  Problem 2: Inverting an Injection

The second problem is stated as follows:

Invert an injective array A on N elements in the subrange from 0 to N − 1, i.e. the output array B must be such that B[A[i]] = i for 0 ≤ i < N.

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

for i = 0 to n - 1 do b[a[i]] <- i done

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:

module InvertingAnInjection use import int.Int use import array.Array

It is convenient to introduce predicate definitions for the properties of being injective and surjective. These are purely logical declarations:

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)

It is also convenient to introduce the predicate “being in the subrange from 0 to n−1”:

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

Using these predicates, we can formulate the assumption that any injective array of size n within the range 0..n−1 is also surjective:

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

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 b so far:

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

Here we chose to have array b as argument; returning a freshly allocated array would be equally simple. The whole module is given below. The verification conditions for function inverting are easily discharged automatically, thanks to the lemma.

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

3.3  Problem 3: Searching a Linked List

The third problem is stated as follows:

Given a linked list representation of a list of integers, find the index of the first element that is equal to 0.

More precisely, the specification says

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.

Since the list is not mutated, we can use the algebraic data type of polymorphic lists from Why3’s standard library, defined in theory list.List. It comes with other handy theories: list.Length, which provides a function length, and list.Nth, which provides a function nth for the n-th element of a list. The latter returns an option type, depending on whether the index is meaningful or not.

module SearchingALinkedList use import int.Int use import option.Option use export list.List use export list.Length use export list.Nth

It is helpful to introduce two predicates: a first one for a successful search,

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

and another for a non-successful search,

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

We are now in position to give the code for the search function. We write it as a recursive function search that scans a list for the first zero value:

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

Passing an index i as first argument allows to perform a tail call. A simpler code (yet less efficient) would return 0 in the first branch and 1 + search ... in the second one, avoiding the extra argument i.

We first prove the termination of this recursive function. It amounts to give it a 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 l itself:

let rec search (i: int) (l: list int) variant { l } = ...

It is worth pointing out that variants are not limited to values of algebraic types. A non-negative integer term (for example, 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 search. The postcondition expresses that either a zero value is found, and consequently the value returned is bounded accordingly,

i <= result < i + length l /\ zero_at l (result - i)

or no zero value was found, and thus the returned value is exactly i plus the length of l:

result = i + length l /\ no_zero l

Solving the problem is simply a matter of calling search with 0 as first argument. The code is given below. The verification conditions are all discharged automatically.

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

Alternatively, we can implement the search with a while loop. To do this, we need to import references from the standard library, together with theory list.HdTl which defines functions hd and tl over lists.

use import ref.Ref use import list.HdTl

Being partial functions, hd and 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 head is defined as follows:

let head (l: list 'a) requires { l <> Nil } ensures { hd l = Some result } = match l with Nil -> absurd | Cons h _ -> h end

The program construct absurd denotes an unreachable piece of code. It generates the verification condition false, which is here provable using the precondition (the list cannot be Nil). Function tail is defined similarly:

let tail (l : list 'a) requires { l <> Nil } ensures { tl l = Some result } = match l with Nil -> absurd | Cons _ t -> t end

Using head and tail, it is straightforward to implement the search as a while loop. It uses a local reference i to store the index and another local reference s to store the list being scanned. As long as s is not empty and its head is not zero, it increments i and advances in s using function tail.

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

The postcondition is exactly the same as for function search_list. The termination of the 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.

3.4  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 × 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:

module NQueens use import int.Int use import array.Array

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 pos and q do no attack each other:

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

Then it is possible to define the consistency of row pos with respect to all previous rows:

predicate is_consistent (board: array int) (pos: int) = forall q:int. 0 <= q < pos -> consistent_row board pos q

Implementing a function which decides this predicate is another matter. In order for it to be efficient, we want to return False as soon as a queen attacks the queen on row pos. We use an exception for this purpose and it carries the row of the attacking queen:

exception Inconsistent int

The check is implemented by a function check_is_consistent, which takes the board and the row pos as arguments, and scans rows from 0 to 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 False is returned. Whenever the end of the loop is reached, True is returned.

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

The assertion in the exception handler is a cut for SMT solvers. This first part of the solution is given below.

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

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 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:

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

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:

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

The search itself makes use of an exception to signal a successful search:

exception Solution

The backtracking code is a recursive function bt_queens which takes the chess board, its size, and the starting row for the search. The termination is ensured by the obvious variant n-pos.

let rec bt_queens (board: array int) (n: int) (pos: int) variant { n-pos }

The precondition relates board, pos, and n and requires board to be a solution up to pos:

requires { 0 <= pos <= n = length board } requires { solution board pos }

The postcondition is twofold: either the function exits normally and then there is no solution extending the prefix in board, which has not been modified; or the function raises Solution and we have a solution in board.

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:

We place a code mark ’Init immediately at the beginning of the program body to be able to refer to the value of 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 Solution:

if pos = n then raise Solution;

Otherwise we scan all possible positions for the queen on row pos with a for loop:

for i = 0 to n - 1 do

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 pos at a column below i:

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) }

Then we assign column i to the queen on row pos and we check for a possible attack with check_is_consistent. If not, we call bt_queens recursively on the next row.

board[pos] <- i; if check_is_consistent board pos then bt_queens board n (pos + 1) done

This completes the loop and function bt_queens as well. Solving the puzzle is a simple call to bt_queens, starting the search on row 0. The postcondition is also twofold, as for bt_queens, yet slightly simpler.

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

This second part of the solution is given below. With the help of a few auxiliary lemmas — not given here but available from Why3’s sources — the verification conditions are all discharged automatically, including the verification of the lemmas themselves.

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

3.5  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, front and rear. We push elements at the head of list rear and pop them off the head of list front. We maintain that the length of front is always greater or equal to the length of rear. (See for instance Okasaki’s Purely Functional Data Structures [6] for more details.)

We have to implement operations empty, head, tail, and enqueue over this data type, to show that the invariant over lengths is maintained, and finally

to show that a client invoking these operations observes an abstract queue given by a sequence.

In a new module, we import arithmetic and theory list.ListRich, a combo theory that imports all list operations we will require: length, reversal, and concatenation.

module AmortizedQueue use import int.Int use import option.Option use export list.ListRich

The queue data type is naturally introduced as a polymorphic record type. The two list lengths are explicitly stored, for better efficiency.

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

The type definition is accompanied with an invariant — a logical property imposed on any value of the type. Why3 assumes that any queue passed as an argument to a program function satisfies the invariant and it produces a proof obligation every time a queue is created or modified in a program.

For the purpose of the specification, it is convenient to introduce a function sequence which builds the sequence of elements of a queue, that is the front list concatenated to the reversed rear list.

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

It is worth pointing out that this function will only be used in specifications. We start with the easiest operation: building the empty queue.

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

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 queue ’a. It is required, for the type checker not to complain about an undefined type variable.

The next operation is head, which returns the first element from a given queue q. It naturally requires the queue to be non empty, which is conveniently expressed as sequence q not being Nil.

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

That the argument q satisfies the type invariant is implicitly assumed. The type invariant is required to prove the absurdity of the first branch (if q.front is Nil, then so should be sequence q).

The next operation is tail, which removes the first element from a given queue. This is more subtle than 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 enqueue, it is a good idea to introduce a smart constructor create which builds a queue from two lists, while ensuring the invariant. The list lengths are also passed as arguments, to avoid unnecessary computations.

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 }

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 f and the reversal of list r. The principle of this implementation is that the cost of this reversal will be amortized over all queue operations. Implementing function tail is now straightforward and follows the structure of function head.

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

The last operation is enqueue, which pushes a new element in a given queue. Reusing the smart constructor create makes it a one line code.

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)

The code is given below. The verification conditions are all discharged automatically.

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

Previous Up Next