Induction, Recursion
Class notes
Analysis Of Algorithms
Document also available in PDF, Postscript, DVI, Text, LaTeX, LyX.
Chapter 1 Proof Of Correctness (Sections 1.6, 2.3)
1.1 Introduction
``Beware of bugs in the above code; I have only proved it correct,
not tried it.''
Donald E. Knuth http://wwwcsfaculty.stanford.edu/~knuth/
How to check if a program is correct ?
Why checking if a program is correct ?
What is a correct program ?
Définition 1
Specification: precise description of how a program should
behave.
A program is correct, if it behaves in accordance with its
specifications.
How to check if a program is correct?

Testing
Designing good test data sets
You can prove there is a bug. No proof of no bug!
 Proof of Correctness
1.2 Correctness
1.2.1 Assertions

...
x=sqrt(r); // r should be >= 0 !
x=a[i]; // i should be in the correct range
...
Définition 2
Assertion: condition on the variables of a program that should
be verified at some given step, if the program is running correctly.
Using assert in C/C++:

#include <assert.h>
...
assert(r>=0);
x=sqrt(r);
assert((0<=i) && (i<MAX));
x=a[i];
...
Each assertion is automatically checked:

If the assertion is not verified, the program stops immediately with
a message like:

Assertion failed, line 35 of file foo.c

That's more informative for the user than a segmentation fault at
the following line.
 This can be deactivated by adding a #define NDEBUG preprocessor directive.
With C++, java and other languages, you can use exceptions
instead of assert:

More informative error messages
 Error recovery mechanisms
Static type checking also makes some kind of assertion checking.
One way or the other, check assertions in your programs.
1.2.2 Specification of a function:

int factorial(int n);
// Preconditions: n is a nonnegative integer
// Postcondition: returns n!
...
int factorial(int n) {
assert(n>=0);
if (n==0) return 1;
return n*factorial(n1);
}
The specification of a program can be formalized as follow:

P: program
 X: input
 P(X): output
 Q: precondition: predicate Q(X) on the input
 R: postcondition: predicate R(X,P(X)) on the input and the output
Exemple 1
Program to compute of a square root

P: y:=sqrt(x);
 X: x
 P(x): y
 Q(x): x>=0
 R(x,y): y^{2}=x
Définition 3
P is correct if (for all X) Q(X)> R(X,P(X)).
A Hoare triple is just a short hand notation: {Q} P
{R}
Exemple 2
{x>=0} y:=sqrt(x);; {y^{2}=x}
1.3 Proof of Correctness
1.3.1 Divide and Conquer
Let P be a big program:

s_{0}
s_{1}
s_{2}
...
s_{n1}
To prove {Q} P {R}, we break P into elementary steps,
and insert assertions that describes the state of the program at each
step:

{Q}
s_{0}
{R_{1}}
s_{1}
{R_{1}}
s_{2}
...
s_{n1}
{R}
P is correct, if each step is correct, i.e. the following Hoare
triples hold:

{Q} s_{0} {R_{1}},
 {R_{1}} s_{1} {R_{2}},
 ...
 {R_{n1}} s_{n1} {R}
To prove that the elementary steps are correct, we will use some syntactic
rules, exactly as we did in formal logic.
1.3.2 Assignment rule:
Consider the following Hoare triple: {Q} x:=e {R}
Théorème 1
If from Q you can derive R with x substituted everywhere
by e,
then the Hoare triple is valid.
Exemple 3
{x=2} y:=x+1 {y=3}
When substituting, y=3 becomes x+1=3.
From x=2, you can deduce x+1=3.
So this Hoare triple holds.
Exemple 4
{x>0} x:=x+1 {x>1}
Here it can be confusing.
The same name x stands for both the value of x before and after
the assignments.
If you get confused, just rename the variable:
{x_{0}>0} x_{1}:=x_{0}+1 {x_{1}>1}
When substituting, x_{1}>1 becomes x_{0}+1>1, which you can
deduce from x_{0}>0.
1.3.3 Conditional Rule
Consider the following Hoare triple:

{Q}
if condition B then
P_{1}
else
P_{2}
end if
{R}
Théorème 2
If the Hoare triples {Q/\ B} P_{1}{R} and {Q/\ B'}
P_{2} {R} hold,
then the Hoare triple above holds.
Exemple 5
[, Exercise 11 p. 78]
Consider the following Hoare triple:

{Q}
while condition B do
P
end_while
{R}
{Q} describes the state of the program before the loop.
We need to have a predicate which describes the state of the program
DURING the loop:
The loop invariant {S}
Most of the time, {Q} will do the job, but not always.
Théorème 3
If the Hoare triple {S/\ B} P {S} holds, then the
following Hoare triple will hold:

{S}
while condition B do
P
end_while
{S/\ B'}
1.3.5 A simple example
Consider this little program:

Product(x,y)
// Precondition: x and y are nonnegative integers
// Postcondition: returns the product of x and y
begin
i:=0;
j:=0;
while ( (i=x)' ) do
j=j+y;
i:=i+1;
end while
// Assertion: { j = x*y }
return(j);
end;
It's pretty clear that this algorithm it's correct.
Let's check it anyway to see how it works.
Proof.
We need a loop invariant, which will describe the state of the program
after k iterations.
A reasonable guess is S : j=iy
Let i_{k}, j_{k} and S_{k} be the value of i, j and
S after k iterations.
Base case: using the assignment rule, i_{0}=0 and j_{0}=0 so
S_{0} holds.
Induction step:
Assume the invariant holds after k1 iterations: j_{k1}=i_{k1}y
We need to prove that the invariant is preserved by the k th iteration.
Otherwise said, we have to check that the following Hoare triple holds:

{S_{k1}/\(i=x)'}
j_{k}:=j_{k1}+y;
i_{k}:=i_{k1}+1;
{S_{k}}
Let's applying the assignment rule.
By substituting i_{k} and j_{k} by the expressions they have
been assigned with, we get:

S_{k} 
<=> 
j_{k} 
= 
i_{k}y 


<=> 
j_{k1}+y 
= 
(i_{k1}+1)y 
(By the substitution rule) 

<=> 
i_{k1}y+y 
= 
(i_{k1}+1)y 
(By S_{k1}) 

<=> 
i_{k1}y+y 
= 
i_{k1}y+y 

So, S_{k} indeed holds.
By induction, after any number k of iterations, S_{k} still
hold.
At the end, both S_{k} and i=x hold, so, as expected: j=iy=xy
Remarque 1
We have proved that after the end of the execution the result is correct.
But what if the program does not terminate and loop forever?
This is not usually consider a proper behavior.
We only have spoken about partialcorrectness.
A full proof of correctness needs also a proof of termination!
1.3.6 A more sophisticated example: The Euclidean algorithm

GCD(a,b)
Begin
// Precondition: a and b are nonnegative integers
// with a>=b.
// Postcondition:
// returns gcd(a,b), the greater common divisor of
// a and b.
Local variables: i, j, q, r
i:=a;
j:=b;
while j>0 do
// Assertion:
// r is the rest of the integer division i/j
r:= i mod j;
i:= j;
j:= r;
end while
// Assertion: i is the gcd of a and b.
return(i);
end;
Exercice 1
Use the Euclidean algorithm to compute:
GCD(8,8), GCD(14,4), GCD(31,17).
Here the proof of correctness of the algorithm is nontrivial.
Proof.
Let i_{k} and j_{k} be the value of i and j after k
iterations.
We need to find an invariant which describes the state of the program
after each iteration.
Take S_{k}: gcd(i_{k}, j_{k})=gcd(a,b).

Base case:
Before the loop, i_{0}=a and j_{0}=b.
So the invariant S_{0} holds: gcd(i_{0}, j_{0})=gcd(a,b);
 Induction step:
Assume S_{k1} holds, that is gcd(i_{k1}, j_{k1})=gcd(a,b).
We just need to prove that gcd(i_{k}, j_{k})=gcd(i_{k1}, j_{k1}).
By the assignment rule, we have:

r is the rest of the division of i_{k1} by j_{k1},
 i_{k}=j_{k1},
 j_{k}=r.
So, by the definition of the integer division, we have:
i_{k1}=qj_{k1}+j_{k}
for some integer q.

Assume x divides both i_{k} and j_{k}.
Then, of course j_{k1}, since j_{k1}=i_{k}.
By the equation above, x also divides i_{k1}.
 Assume x divides both i_{k1} and j_{k1}.
Then of course x divides i_{k}.
Once again, using the equation above, x also divides j_{k}
Therefore, gcd(i_{k}, j_{k})=gcd(i_{k1}, j_{k1})=gcd(a,b),
as wanted.
 At the end:
By induction, the loop invariant S still holds: gcd(i, j)=gcd(a,b)
Moreover, the loop condition failed: j=0.
So, gcd(a,b)=gcd(i, j)=gcd(i, 0)=i,
as expected.
1.4 Conclusion
1.4.1 A note on automatic program proving:

There is no mechanical way to decide even if a program terminates
or not.
 Traditional imperative languages:

Automatic proving is very difficult because of side effects
 side effects needs to be considered as some form of output
 Functional languages (lisp, scheme, ML, caml):

Designed to make it easier to prove correctness
 Fun to program. Try them!
 Two difficulties:

Finding the correct assertions
 Checking that the implications holds
 Mixed approach:

The programmer gives the main assertions
 The prover derives the other assertions
1.4.2 Check assertions in your programs!

Use static type checking / assert / exceptions
 When debugging, you can ask for all assertions to be checked
 Documentation
 Help for the proof
Induction, Recursion
Class notes
Analysis Of Algorithms
Proof Of Correctness /
CSM MACS358 /
Nicolas M. Thiéry
Last modified: Fri Jan 19 13:12:17 2007