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:
-
The name
n@0
is used to refer to the initial value of
the variable n
, as well inside the loop invariant as in
the post-condition;
- Purely functional expressions are allowed anywhere in the
program and they can use any purely informative Coq constants;
That is why we can use Zmult, Zsquare and
Zdiv2 in the programs even if they are not other functions
previously introduced as programs.
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:
-
A proof of insertion sort by Nicolas Magaud, ENS Lyon;
- A proof of quicksort and find by the author.