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). It also covers the refinement mechanism that is available through module cloning.

The Theory of Lists

The modules in this library contain the definition of lists as an inductive type, together with 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 list append 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

Functional Programming: Insertion Sort

[permalink]

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

1. Write the algorithm in WhyML
2. Write a specification for it using pre- and postconditions
3. Use the web interface or the Why3 IDE to generate verification conditions, export them to an SMT solver, and 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 defines when that function implements sorting, that is:

1. the output list is a permutation of the input list; and

2. 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 as well: 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).