To verify the correctness (the property of being correct) of a computer program, we often simply run it through a battery of tests—which is sufficient only if every possible case is tested! Before reaching that stage, it is better to build the program around its proof. In fact, the problem arises only with iterative or recursive loops.
References
La logique. Bibliothèque Tangente 15, 2004.
Mathématiques et informatique. Bibliothèque Tangente 52, 2014.
Les démonstrations. Bibliothèque Tangente 55, 2015.
Suite à 11 (18). Bernard Frize, 2006.
-
More challenging: iterative functions
------------------------------------
It is generally harder to prove that a program produces the expected result for an iterative function (that is, one structured around a loop such as "repeat," "while" or "for") than for a recursive function. Such proofs are based on the notion of a loop invariant.
Consider the calculation of the GCD (greatest common divisor) of two numbers using Euclid's algorithm. The brilliant idea attributed to Euclid is that the GCD of two numbers a and b is the same as that of a and b modulo a, namely the remainder d in the Euclidean division of a by b. This gives the following pseudocode:
Gcd(a,b)=
Introduce an additional variable d
Repeat
d:=a mod b
a:=b
b:=d
until d=0
return a
The loop invariant is: "The common divisors of a and b remain the same at every step." Furthermore, the values taken by d form a strictly decreasing sequence, guaranteeing termination. This algorithm can be written recursively:
GcdRec(a,b)=
If a=0, return b
Otherwise return GcdRec(b mod a, a)
The correctness of this program is then easily proved by induction on the integer a.
-
Programming is proving: recursive functions
-------------------------------------------
The body of a recursive function generally has two parts: the base case and the recursive step itself, mirroring a proof by induction. The classic example is calculating the factorial of a positive integer. Here is some pseudocode:
Factorial(n)=
If n=0, return 1
Otherwise return n\*Factorial(n-1)
The proof that the Factorial function does indeed return the product of all the integers from 1 to n (denoted by n!) for every natural number n proceeds by induction. The proof can be read directly from the preceding program. To formalize the argument, let P(n) be the property "Factorial(n) returns n!".
P(0) is true by the first line of the program. Now suppose that P(n–1) is true for an integer n ≥ 1, and consider P(n).
Factorial(n) calls Factorial(n-1), which returns (n–1)! by the induction hypothesis. The second line of the program therefore returns n×(n–1)!, which equals n!, so P(n) is true. Thus P(0) is true, and whenever P(n–1) is true, P(n) is also true. By the principle of induction, P(n) is therefore true for every natural number n.
In fact, this proof exactly mirrors the structure of the function. In this case, we can sum it up by saying that programming is proving!
