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 many uses of the tool). We take a tour of Why3’s logic and programming languages and the ways in which they interact, and illustrate different ways to conduct inductive proofs. Finally, we also cover the refinement mechanism that is available through module cloning.

Insertion Sort as a logic function

We start by defining the insertion sort algorithm on integer lists as follows:

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

  function insert (i :int) (l :list int) : list int =
    match l with
    | Nil      -> Cons i Nil
    | Cons h t -> if i <= h then Cons i (Cons h t) else Cons h (insert i t)
    end

  function iSort (l :list int) : list int =
    match l with
    | Nil      -> Nil
    | Cons h t -> insert h (iSort t)
    end

The permutation and order properties can be expressed using predicates defined in the [list](http://why3.lri.fr/stdlib/list.html) library modules, imported as shown above. For instance the sorted inductive predicate is defined in the list.Sorted module as follows (and is in turn cloned by the list.SortedInt module) :

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

As defined above, insert and iSort functions are both logic functions, and we can write lemmas about them. For instance we require the following two about insert :

  lemma insert_sorted: forall a :int, l :list int. 
                       sorted l -> sorted (insert a l)

  lemma insert_perm: forall x :int, l :list int. 
                     permut (Cons x l) (insert x l)

Now, notice that insert has a structural recursive definition (the recursive call is performed on the tail of the list). This means that the above lemmas can both be proved using a simple induction principle; in Why3 they can be proved using the induction_ty_lex proof transformation.

With the above lemmas, we may now move to proving results about the sorting algorithm:

  lemma sort_sorted: forall l :list int.
                     sorted (iSort l)

  lemma sort_perm: forall l :list int.
                   permut l (iSort l)

iSort is also defined in a similar way, so both these lemmas can again be proved using induction_ty_lex.

We can state the final result about the algorithm by defining what a sorting function is, and then proving that iSort is such a function.

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

  goal insertion_sort_correct: is_a_sorting_algorithm iSort

end

The proof of the goal does not require induction (it results directly from the two previous lemmas).

Insertion Sort as a program function

[permalink]

An alternative possibility is to write the algorithm as a program (WhyML) function equipped with a contract, similarly to what would be done with an imperative program function.

Let us start with the helper function insert : its contract states that it should receive a sorted list, and it will also return a sorted list. Moreover, the result contains the same multiset of elements as the input list, extended with the inserted element.

module InsertionSortProgram
  use  ...

  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

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

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

A second remark is that, when compared with the logic version of the algorithm, no manual proof transformation is required now to make explicit the induction principle to be used: this is implicitly given by the function definition itself.

The same remarks apply to the iSort function, also proved correct using an auto strategy:

  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

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

  goal insertion_sort_correct: is_a_sorting_algorithm iSort

end

Observe also the final goal above, a logic statement involving the program function iSort. The fact that this can be written means that, in fact, iSort inhabits both namespaces: it is both a program function and a logic function. We remark the following:

This is optional! We could choose to make the function exist only at the program level, in which case it would not be possible to mention it in the logic (as in the above goal)
Only pure program functions, with no side effects, can be declared as function . When reasoning about functional programs it makes sense to do this, which will result in a particular kind of usage of Why3. In practice, functional programs can be used in the logic but specified and verified using contracts, which facilities inductive proofs ( AND TERMINATION ).

Mergesort as a program function

[permalink]

Let us move to a more complicated algorithm. The functional mergesort algorithm requires two helper functions, one to split the input list in two lists of the same size, and another to merge two sorted lists. We will write both as WhyML functions equipped with contracts; for split the contract merely says that together the result lists contain the same elements as the input; for merge we require the input lists to be sorted and in addition to the permutation aspect the contract states that the result is a sorted list:

module MergeSort
  use ...

  let rec function split (l :list int) : (list int, list int)
    ensures { let (l1,l2) = result in permut l (l1 ++ l2) } 
  =
    match l with
    | Nil -> (Nil, Nil)
    | Cons x Nil -> (Cons x Nil, Nil)
    | Cons x1 (Cons x2 l') -> let (l1, l2) = split l'
                              in (Cons x1 l1, Cons x2 l2)
    end

  let rec function merge (l1 l2 :list int) : list int
    requires { sorted l1 /\ sorted l2  }
    ensures { sorted result } 
    ensures { permut (l1 ++ l2) result } 
  =
    match l1, l2 with
    | Nil, _ -> l2
    | _, Nil -> l1
    | (Cons a1 l1'), (Cons a2 l2') -> if (a1 <= a2)                      
                                      then (Cons a1 (merge l1' l2))
                                      else (Cons a2 (merge l1 l2'))
    end

All the VCs generated for these functions are proved automatically with SMT solvers using an auto strategy. It is worth considering this for a moment, since both functions are quite different from what we had in insertion sort and its helper function.

The recursive call in split is not performed on the tail of the list, but rather on the “tail of the tail”
merge on the other hand takes two argument lists; the recursive call alternatively preserves one of them, and is structural in the other argument.
Why3 is still capable of proving the termination of both functions automatically

The main mergesort function implements the divide and conquer strategy using the above helpers:

  let rec function mergesort (l :list int)
    ensures { sorted result } 
    ensures { permut l result } 
    variant { length l } 
  =
    match l with
    | Nil -> Nil
    | Cons x Nil -> Cons x Nil
    | _ ->   let (l1,l2) = split l in merge (mergesort l1) (mergesort l2)
    end

end

The first thing to notice is the presence of a variant. The termination of this function cannot be proved automatically, and in fact Why3 will reject the definition if a variant is not provided as part of the contract.

The variant { length l } will however lead to the generation of a VC that cannot be proved: it is not possible to automatically establish that split produces two lists that are strictly shorter than its argument.

In order to allow for termination of mergesort to be proved, we then add the following postcondition in the contract of split :

  ensures { let (l1,l2) = result in length l < 2 \/ 
           (length l >= 2 /\ length l1 < length l /\ length l2 < length l) }

Mergesort as a logic function [ Optional Reading! ]

We started by seeing a logic version of insertion sort, followed by a WhyML definition of insertion sort and then of mergesort. It is only natural to ask whether the latter algorithm can also be defined in logic.

New difficulties arise, which we will take as opportunities to discuss additional features of Why3. Let us start by looking at the first helper function, split. It can be defined as follows:

  function split (l :list int) : (list int, list int) =
    match l with
    | Nil -> (Nil, Nil)
    | Cons x Nil -> (Cons x Nil, Nil)
    | Cons x1 (Cons x2 l') -> let (l1, l2) = split l'
                              in (Cons x1 l1, Cons x2 l2)
    end 

We would now like to prove the following lemma, meaning that the multiset of elements is preserved by splitting:

  lemma split_lm: forall l :list int. 
                  let (l1,l2) = split l in permut l (l1 ++ l2)

However, the induction_ty_lex proof transformation will not work, because unlike insert the split function is not defined by simple structural recursion.

Why3 offers a way out of this difficulty in the form of a lemma function. This borrows from the program level of Why3 the capability to perform inductive proofs based on contracts. We will define a WhyML function that takes a list as argument, and write a postcondition corresponding to the lemma we are trying to prove (so split is naturally mentioned in it). The definition of the function simply expresses the induction principle that is required for the proof, by following the definition of split.

  let rec lemma split_lm (l :list int) : () 
    ensures { let (l1,l2) = split l in permut l (l1 ++ l2) }
  = match l with
    | Nil -> ()
    | Cons _ Nil -> ()
    | Cons _ (Cons _ l') -> split_lm l'
    end 

The verification condition is proved, and the contract is inserted in the logic context as a lemma. The lemma function quite resembles the WhyML definition of split that we saw previously, but its only purpose is to provide a proof structure for its postcondition.

The same can be done for merge :

  function merge (l1 l2 :list int) : list int =
    match l1, l2 with
    | Nil, _ -> l2
    | _, Nil -> l1
    | (Cons a1 l1'), (Cons a2 l2') -> if a1 <= a2
                                      then (Cons a1 (merge l1' l2))
                                      else (Cons a2 (merge l1 l2'))
    end

  let rec lemma merge_lm (l1 l2 :list int) : ()
    requires { sorted l1 /\ sorted l2  }
    ensures { sorted (merge l1 l2) }
    ensures { permut (l1 ++ l2) (merge l1 l2) }
  = match l1, l2 with
    | Nil, _ -> ()
    | _, Nil -> ()
    | (Cons a1 l1'), (Cons a2 l2') -> if a1 <= a2
                                      then merge_lm l1' l2
                                      else merge_lm l1 l2'
    end

One would then be tempted to write mergesort as the following logic function:

  function mergesort (l :list int) : list int 
  = match l with 
    | Nil -> Nil
    | Cons x Nil -> Cons x Nil
    | _ ->   let (l1,l2) = split l
                  in  merge (mergesort l1) (mergesort l2)
    end

This will not work: termination cannot be established automatically (because the recursive calls are not being performed on sublists of the argument l), so it is not possible to define mergesort as a function .

There is a way out of this. Recall that we know how to define mergesort as a WhyML function that is also a logic function. What we were not able to do yet is to define it as a logic function that is not a program function. The difficulty is that, since automatic termination cannot be established, we would like to proved a variant, but variants can only be used in program functions.

This may sound a little confusing at first, but Why3 provides a way to define logic functions that are not program functions, using program constructs and contracts. Ghost functions are written as WhyML code that is only interpreted logically, not meant to be executed. Mergesort can be defined as follows in the logic namespace, with the length of the argument list used as variant:

  let rec ghost function mergesort (l :list int) : list int 
    variant { length l }
  = match l with 
    | Nil -> Nil
    | Cons x Nil -> Cons x Nil
    | _ ->   let (l1,l2) = split l
                  in  merge (mergesort l1) (mergesort l2)
    end

Its correctness is established through the following lemma function, where the assert statements act as intermediate lemmas:

  let rec lemma mergesort_lm (l :list int) : ()
    ensures { sorted (mergesort l) }
    ensures { permut l (mergesort l) } 
    variant { length l }
  =
    match l with 
    | Nil -> ()
    | Cons _ Nil -> ()
    | _ ->   let (l1,l2) = split l 
             in assert { permut l (l1 ++ l2) } ; 
                mergesort_lm l1 ; 
                mergesort_lm l2 ; 
                assert { permut l (mergesort l1 ++ mergesort l2) } 
    end

[permalink]

Consider the following alternative WhyML version of mergesort:

module MergeSort
  use ...

  val function split (l :list int) : (list int, list int)
    ensures { let (l1,l2) = result in length l < 2 \/ 
             (length l >= 2 /\ length l1 < length l /\ length l2 < length l) } 
    ensures { let (l1,l2) = result in permut l (l1 ++ l2) } 


  val function merge (l1 l2 :list int) : list int
    requires { sorted l1 /\ sorted l2  }
    ensures { sorted result } 
    ensures { permut (l1 ++ l2) result } 

  
  let rec function mergesort (l :list int)
    ensures { sorted result } 
    ensures { permut result l } 
    variant { length l }
  = match l with
    | Nil -> Nil
    | Cons x Nil -> Cons x Nil
    | _ ->   let (l1,l2) = split l
             in merge (mergesort l1) (mergesort l2)
    end

end

It differs from the previous version in the fact that no definitions are given for the helper functions. Instead, they are just declared (using val) with a signature and contract. The contracts contain all the necessary information to allow for the correctness of mergesort to be proved — its verification condition can be proved in the same way as in the previous version.

If we want to provide a concrete definition of mergesort, by giving definitions of split and merge, we must now clone the MergeSort module inside a new module, as follows:

module MergeSortRefnm
  use ...

  let rec function split (l :list int) : (list int, list int)
    ensures { let (l1,l2) = result in length l < 2 \/ 
             (length l >= 2 /\ length l1 < length l /\ length l2 < length l) } 
    ensures { let (l1,l2) = result in permut l (l1 ++ l2) } 
  = match l with
    | Nil -> (Nil, Nil)
    | Cons x Nil -> (Cons x Nil, Nil)
    | Cons x1 (Cons x2 l') -> let (l1, l2) = split l'
                              in (Cons x1 l1, Cons x2 l2)
    end

  let rec function merge (l1 l2 :list int) : list int
    requires { sorted l1 /\ sorted l2 }
    ensures { sorted result } 
    ensures { permut (l1 ++ l2) result } 
    variant { length (l1 ++ l2) }
  = match l1, l2 with
    | Nil, _ -> l2
    | _, Nil -> l1
    | (Cons a1 l1'), (Cons a2 l2') -> if (a1 <= a2)                        
                                      then (Cons a1 (merge l1' l2))
                                      else (Cons a2 (merge l1 l2'))
    end
  
  clone MergeSort with val split, val merge 

  goal thisReallyWorks : 
    forall l :list int. let ls = mergesort l 
                            in sorted ls /\ permut ls l

end

Cloning the MergeSort module inside MergeSortRefnm will copy the former into the latter, instantiating the elements mentioned after with : the functions split and merge are given a definition in the cloning module. Observe that this will generate verification conditions to establish that the refinement of the contracts declared in MergeSort with the definitions of MergeSortRefnm is correct, i.e. for each function, the contract in the cloning module is not weaker than the contract in the cloning module.

In the present example both functions have exactly the same contract in the defined function as in the cloned declaration, so these VCs are proved trivially. Together, the VCs generated for the two modules imply that we have a correct implementation of merge sort, because:

The validity of the MergeSort VCs implies that the mergesort implementation is correct if split and merge are implemented according to the specifications given in the module.
The validity of the MergeSortRefnm VCs implies that the implementations of split and merge are correct according to the specifications given in this module, and moreover (for the VCs generated by cloning) they are also correct with respect to the contracts in the MergeSort module (which happen to be the same).

Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

Why3: Verification of Functional Programs

Insertion Sort as a logic function

Insertion Sort as a program function

Mergesort as a program function

Mergesort as a logic function [ Optional Reading! ]

Refinement in Why3