18.7 Examples

18.7.1 Computation of Xn

As a first example, we prove the correctness of a program computing Xn using the following equations:
ì
í
î
X2n = (Xn)2
X2n+1 = X × (Xn)2
If x and n are variables containing the input and y a variable that will contain the result (xn), such a program may be the following one:
8cm
m := !x ; y := 1 ;
while !n ¹ 0 do
if (odd   !n) then y := !y × !m ;
m := !m × !m ;
n := !n / 2
done

Specification part.
Here we choose to use the binary integers of ZArith. The exponentiation Xn is defined, for n ³ 0, in the module Zpower:
Coq < Require ZArith.

Coq < Require Zpower.

In particular, the module ZArith loads a module Zmisc which contains the definitions of the predicate Zeven and Zodd, and the function Zdiv2. This module ProgBool also contains a test function Zeven_odd_bool of type " n. $ b. if   b  then   (Zeven n)   else   (Zodd n) derived from the proof Zeven_odd_dec, as explained in section 18.2.3:

Correctness part.
Then we come to the correctness proof. We first import the Coq module Programs:
Coq < Require Programs.

Then we introduce all the variables needed by the program:
Coq < Parameter x : Z.

Coq < Global Variable n,m,y : Z ref.

At last, we can give the annotated program:
Coq < Correctness i_exp
Coq <   { `n >= 0` }
Coq <   begin
Coq <      m := x; y := 1;
Coq <      while !n > 0 do
Coq <        { invariant (Zpower x n@0)=(Zmult y (Zpower m n)) /\ `n >= 0`
Coq <          variant n }
Coq <        (if not (Zeven_odd_bool !n) then y := (Zmult !y !m))
Coq <           { (Zpower x n@0) = (Zmult y (Zpower m (Zdouble (Zdiv2 n)))) };
Coq <        m := (Zsquare !m);
Coq <        n := (Zdiv2 !n)
Coq <      done
Coq <    end
Coq <    { y=(Zpower x n@0) }
Coq < .
5 subgoals
  
  m : Z
  n : Z
  y : Z
  Pre3 : `n >= 0`
  phi0 : Z
  m1 : Z
  n0 : Z
  y1 : Z
  Variant1 : `phi0 = n0`
  Pre2 : `(Zpower x n) = y1*(Zpower m1 n0)`/\`n0 >= 0`
  resultb : bool
  Test2 : `n0 > 0`
  resultb0 : bool
  Test1 : (Zodd n0)
  ============================
   `(Zpower x n) = y1*m1*(Zpower m1 (Zdouble (Zdiv2 n0)))`
subgoal 2 is:
 `(Zpower x n) = y1*(Zpower m1 (Zdouble (Zdiv2 n0)))`
subgoal 3 is:
 (Zwf `0` (Zdiv2 n0) n0)
 /\`(Zpower x n) = y2*(Zpower (Zsquare m1) (Zdiv2 n0))`
   /\`(Zdiv2 n0) >= 0`
subgoal 4 is:
 `(Zpower x n) = 1*(Zpower x n)`/\`n >= 0`
subgoal 5 is:
 `y1 = (Zpower x n)`

The proof obligations require some lemmas involving Zpower and Zdiv2. You can find the whole proof in the Coq standard library (see below). Let us make some quick remarks about this program and the way it was written:

18.7.2 A recursive program

To give an example of a recursive program, let us rewrite the previous program into a recursive one. We obtain the following program:
8cm
let rec exp x n =
if n = 0 then
1
else
let y = (exp   x   (n/2)) in
if (even   n) then y× y else x× (y× y)

This recursive program, once it is annotated, is given to the tactic Correctness:
Coq < Correctness r_exp
Coq <   let rec exp (x:Z) (n:Z) : Z { variant n } =
Coq <     { `n >= 0` }
Coq <     (if n = 0 then
Coq <        1
Coq <      else
Coq <        let y = (exp x (Zdiv2 n)) in
Coq <        (if (Zeven_odd_bool n) then
Coq <           (Zmult y y)
Coq <         else
Coq <           (Zmult x (Zmult y y))) { result=(Zpower x n) }
Coq <     ) 
Coq <     { result=(Zpower x n) }
Coq < .
5 subgoals
  
  x0 : Z
  n : Z
  rphi1 : Z
  exp : (phi:Z)
         (Zwf `0` phi rphi1)
         ->(x,n:Z)
            `phi = n`->`n >= 0`->{result:Z | `result = (Zpower x n)`}
  x1 : Z
  n0 : Z
  Variant1 : `rphi1 = n0`
  Pre1 : `n0 >= 0`
  resultb : bool
  Test2 : `n0 = 0`
  ============================
   `1 = (Zpower x1 n0)`
subgoal 2 is:
 (Zwf `0` (Zdiv2 n0) n0)
subgoal 3 is:
 `(Zdiv2 n0) >= 0`
subgoal 4 is:
 `y*y = (Zpower x1 n0)`
subgoal 5 is:
 `x1*(y*y) = (Zpower x1 n0)`

You can notice that the specification is simpler in the recursive case: we only have to give the pre- and post-conditions --- which are the same as for the imperative version --- but there is no annotation corresponding to the loop invariant. The other two annotations in the recursive program are added for the recursive call and for the test inside the let in construct (it can not be done automatically in general, so the user has to add it by himself).

18.7.3 Other examples

You will find some other examples with the distribution of the system Coq, in the sub-directory tactics/programs/EXAMPLES of the Coq standard library. Those examples are mostly programs to compute the factorial and the exponentiation in various ways (on types nat or Z, in imperative way or recursively, with global variables or as functions, ...).

There are also some bigger correctness developments in the Coq contributions, which are available on the web page coq.inria.fr/contribs. for the moment, you can find: