Why3: Verification of Imperative Programs

Example: Factorial

[permalink]

This example is included as an exercise in TryWhy3.

We already know how to write a recursive, functional implementation of the function that computes the nth. factorial number.

module FactRecursive

  use int.Int
  use int.Fact    (* contains a theory defining a LOGIC function fact *)

  let rec fact_rec (n: int) : int
    requires { n >= 0 }
    ensures  { result = fact n }
    variant  { n }
  =
    if n = 0 then 1 
    else n * fact_rec (n - 1)

end

Note that the postcondition is used as induction hypothesis in its own proof. There is no need for any additional invariants or assertions.

If, however, we write factorial using a loop, we will need to provide a loop invariant, as well as a loop variant for termination.

Note that in WhyML:

• mutable variables are declared and initialized as let ref m = 0 in …
• they are assigned with the <- operator

• immutable variables are initialized with =

  module FactWhile use int.Int, int.Fact

  let fact_loop (n: int) : int
    requires { n >= 0 }
    ensures  { result = fact n }
  = let ref m = 0 in
    let ref r = 1 in
    while m < n do
      invariant { 0 <= m <= n }
      invariant { r = fact m }
      variant   { n-m }
      m <- m + 1;
      r <- r * m
    done;
    r
  

  end

For bounded loops WhyML offers as an alternative for loops. We note that:

• for loops do not require variants
• it is also not necessary to include trivial invariants concerning the control variables (m in the above example)
• for loop variables are immutable
• unlike with while loops, invariants do not hold on loop exit — the final iteration of the loop must be taken into account

So factorial may alternatively be written as any of the following:

  let fact_loop (n: int) : int
    requires { n >= 0 }
    ensures  { result = fact n }
  = let ref r = 1 in
    for m = 0 to n-1 do
      invariant { r = fact m }
      r <- r * (m+1)
    done;
    r



  let fact_loop (n: int) : int
    requires { n >= 0 }
    ensures  { result = fact n }
  = let ref r = 1 in
    for m = 1 to n do
      invariant { r = fact (m-1) }
      r <- r * m
    done;
    r

Example: Insertion Sort

[permalink]

Recall the insertion sort imperative algorithm, written for instance as a C function:

void insertionSort(int A[], int N) {
    int i, j, key;    
    for (j=1 ; j<N ; j++) {
        key = A[j];
        i = j-1;        
        while (i>=0 && A[i] > key) {
            A[i+1] = A[i];
            i--;
        }
        A[i+1] = key;
    }
}

In order to verify this same algorithm with Why3 we create a module that starts by importing the required library modules, and write the algorithm in WhyML.

The Why3 array library, available at http://why3.lri.fr/stdlib/array.html, contains the modules array.IntArraySorted and array.ArrayPermut that not only define the relevant notions for specifying the notion of sorting, but also contain lemmas that will facilitate automated proofs.

module InsertionSort
  use int.Int
  use ref.Ref
  use array.Array, array.IntArraySorted, array.ArrayPermut

  let insertion_sort (a: array int) 
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = 
    . . . 
end

Note:

• the use of library predicates sorted and permut_all to specify the sorting and permutation properties
• the expression old a refers to the array a in its initial state. This is crucial in a language with state: since the array is passed by reference and modified by the function, the postcondition (and possibly loop invariants) must be able to refer to the value of any variable / expression in the pre-state of the function

We will write the complete algorithm following step by step the C version, but adding also annotations that are required to prove its correctness: loop invariants and variants.

The outer loop is bounded and can be written as a + for :

  let insertion_sort (a: array int) 
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
    for j = 1 to length a - 1 do
      invariant { sorted_sub a 0 j }
      invariant { permut_all (old a) a }
      ... 
    done

As in many other languages (but not C), arrays contain length information: length a is the length of array a. Array accesses are valid within their length.

Its invariants state that

• The initial segment of the array is already sorted (j first elements)

  sorted_sub a x y means that the range between indices x and y-1 is sorted.

• The array contains a permutation of the initial values

The loop body mimics the C code:

      let key = a[j] in
      let ref i = j-1 in      

      while i >= 0 && a[i] > key do
          invariant { -1 <= i <= j-1 }
          invariant { sorted_sub a 0 j }
          variant { i }
          a[i+1] <- a[i];
          i <- i - 1
      done;
      a[i+1] <- key

Notice that unlike i the variable key is immutable. The annotations in the while loop are quite natural, framing the possible values of i , which acts as loop variant, and stating also that this sorted insertion loop does not violate the order already established in the first j elements of the array.

But two more subtle annotations are required. The first invariant states properties about the values of a[j-1] , a[j], key , and a[i+1] that only hold after the first iteration, i.e. when i = j-1 is no longer true. We write it as follows:

          invariant { i <> j-1 -> (a[j-1] <= a[j] /\ key < a[i+1]) }

Additionally, note that inside the while loop the array does not contain a permutation of the initial values: one of the values is stored in the key variable, and two positions of the array contain the same value. But it is possible to write a logic expression referring to a modified version of the current array using <- syntax as follows:

          invariant { permut_all (old a) a[i+1 <- key] }

a[k <- e] refers to the array a updated by setting the value stored at index k to e.

With these, the algorithm can be proved correct using a single SMT solver (Alt-Ergo).