Why3: Verification of Functional Programs

This note is an introduction to the use of Why3 for the specific purpose of verifying functional programs (just one of the possible uses of the tool).

The Theory of Lists

The modules in this library contain the definition of lists as an inductive (algebraic) type, together with many related useful definitions. We show below the defined membership predicate mem and the inductive predicate sorted. Inductive predicates allow for inference rule-based definitions, and are free from termination requirements.

type list 'a = Nil | Cons 'a (list 'a)

predicate mem (x: 'a) (l: list 'a) = 
    match l with
    | Nil      -> false
    | Cons y r -> x = y \/ mem x r
    end

inductive sorted (l: list t) =
    | Sorted_Nil:
        sorted Nil
    | Sorted_One:
        forall x: t. sorted (Cons x Nil)
    | Sorted_Two:
        forall x y: t, l: list t.
        le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))

On the other hand the List library also contains definitions of basic program functions, written in the WhyML programming language. We show two examples, the length and append polymorphic functions:

let rec function length (l: list 'a) : int =
    match l with
    | Nil      -> 0
    | Cons _ r -> 1 + length r
    end

let rec function (++) (l1 l2: list 'a) : list 'a =
    match l1 with
    | Nil -> l2
    | Cons x1 r1 -> Cons x1 (r1 ++ l2)
    end

Program functions may have specification contracts. Consider for instance the Quant module of the list library:

module Quant
  use List  use Mem

  let rec function for_all (p: 'a -> bool) (l:list 'a) : bool
    ensures { result <-> forall x. mem x l -> p x }
  = match l with
    | Nil -> true
    | Cons x r -> p x && for_all p r
    end

  let rec function for_some (p: 'a -> bool) (l:list 'a) : bool
    ensures { result <-> exists x. mem x l /\ p x }
  = match l with
    | Nil -> false
    | Cons x r -> p x || for_some p r
    end

  let function mem (eq:'a -> 'a -> bool) (x:'a) (l:list 'a) : bool
    ensures  { result <-> exists y. mem y l /\ eq x y }
  = for_some (eq x) l

end

Note that:

The above three functions are higher-order, taking as parameter a predicate on type 'a.
Their definitions include a postcondition (**ensures**) where the **result** keyword refers to the return value of the function.
Since all 3 functions have return type bool , the postconditions are equivalence formulas involving the result (and some quantified formula).
The library contains two membership predicates!
- The first (**predicate** mem ...) is part of the logic language and cannot be called by program functions.
  - It uses the logic equality predicate
- The second (**let** ```function mem …`) is a program function
  - It uses an equality predicate passed as argument
  - Its postcondition uses the logic predicate mem !

Functional Programming: Insertion Sort

[permalink]

As an example of how to verify the behavior of functional programs with Why3, we will consider the insertion sort algorithm. We will:

Write the algorithm in WhyML
Write a specification for it using pre- and postconditions
Use the web interface or the Why3 IDE to
1. generate verification conditions,
2. export them to an SMT solver, and
3. discharge them, thus proving that the algorithm is correct w.r.t. the specification

We create a module and start by importing the integer and lists library modules, as well as specific modules containing definitions involving list permutations and sorting.

We then define a higher-order predicate is_a_sorting_algorithm that takes a function on integer lists and describes when that function implements sorting, that is:

the output list is a permutation of the input list; and
the output list is sorted

module InsertionSort use int.Int use list.List use list.Permut use list.SortedInt

predicate is_a_sorting_algorithm (f: list int -> list int) = forall al :list int. permut al (f al) /\ sorted (f al)

To define the sorting algorithm we start by writing an ordered insertion function insert. Its specification states that

it should receive a sorted list (the requires keyword introduces a precondition)
it will also return a sorted list (the ensures keyword introduces a postcondition)

moreover, the result contains the same multiset of elements as the input list, extended with the inserted element. In other words, the output list is a permutation of the elements in the input list, together with the inserted element

let rec function insert (i: int) (l: list int) : list int
  requires { sorted l } 
  ensures  { sorted result } 
  ensures  { permut result (Cons i l) } 
=
  match l with
  | Nil -> Cons i Nil
  | Cons h t -> if i <= h then Cons i l 
                else Cons h (insert i t)
  end

There are several observations to be made here. First of all, note that whereas for a typical iterative algorithm you would have to provide one or more loop invariants that allow for the function’s contract to be established, in a recursive function the contract itself plays the role of invariant: the very contract of the function that is being verified is used to generate a verification condition regarding the recursive call.

The verification conditions generated by Why3 for this function are all easily proved with the help of an SMT solver, using one of the auto strategies (depending on your setup this may not even require splitting the VC). This means that the function is correct: if you feed it any sorted list and an integer, the function will indeed insert it in the list and return a sorted list.

The same remarks apply to the iSort function. Its specification states that the result is a sorted list that is a permutation of the input list, and the algorithm itself is well-know:

  let rec function iSort (l: list int) : list int
    ensures { sorted result } 
    ensures { permut result l } 
  =
    match l with 
    | Nil -> Nil
    | Cons h t -> insert h (iSort t ) 
    end

This is equally proved correct using an auto strategy.

We may now prove that iSort implements sorting. The proof of the following goal results immediately from its specification of iSort .

  goal correctness: is_a_sorting_algorithm iSort

Finally, we note that Why3 also contains an interpreter. We can run iSort on as input list by including the following main function in the module:

  let main () =
      let l = Cons 2 (Cons 3 (Cons 1 Nil)) in 
      iSort l
end

This complete program could now be extracted as an OCaml program (this is outside the scope of this course).

TryWhy3 The online version of Why3 has limitations (in particular a single solver is available). So some developments may need additional lemmas and/or asserts that are not required if the standalone tool is used.

For example, the following version of insert may well be easier to verify automatically than the previous one. The assert helps establishing that Consing h with insert i t results in a sorted list.

let rec function insert (i: int) (l: list int) : list int
    requires { sorted l } 
    ensures  { sorted result } 
    ensures  { permut result (Cons i l) } 
=
  match l with 
  | Nil -> Cons i Nil
  | Cons h t -> if i <= h then Cons i l 
                          else let t' =  insert i t in 
                          assert { forall x :int. mem x t' -> h<=x } ; 
                          Cons h t'
  end

Exercise

Consider the functional quicksort algorithm. It is written in WhyML as follows, using a helper function partition.

  let rec function partition (x:int) (l:list int) : (l1:list int, l2:list int)
    ensures  { true }
  =
    match l with
    | Nil -> (Nil, Nil)
    | Cons y ys -> let (ll, lr) = partition x ys in
                   if y<=x then (Cons y ll, lr) 
                   else (ll, Cons y lr)
  end


  let rec function quicksort (l :list int) : list int
    ensures { true }
    variant { length l }
  =
    match l with
    | Nil -> Nil
    | Cons x t -> let (l1, l2) = partition x t in
                  let l1' = quicksort l1 in
                  let l2' = quicksort l2 in
                  l1'++(Cons x l2')
    end

[permalink]

Note the inclusion of a variant in the contract of the quicksort function. Why3 can automatically establish the termination of functions defined using basic structural induction (e.g. on the tail of a list). This is not the case above, where l1 and l2 are obtained by partitioning the tail of the argument list l .

We thus need to include a variant. The length of the list is an adequate measure, since l1 and l2 are both guaranteed to be shorter than l (since they result from partitioning t and not l).

Complete the contracts that capture the expected behaviour of both functions
Prove the correctness of both functions using Why3
If required, place appropriate asserts in the above definitions to facilitate the automatic proofs.

Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

Why3: Verification of Functional Programs

The Theory of Lists

Functional Programming: Insertion Sort

Exercise