 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://www-cs-faculty.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:
• 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 non-negative integer

// Postcondition: returns n!

...

int factorial(int n) {

assert(n>=0);

if (n==0) return 1;

return n*factorial(n-1);

}
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): y2=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);; {y2=x}

## 1.3  Proof of Correctness

### 1.3.1  Divide and Conquer

Let P be a big program:
s0

s
1

s
2

...

s
n-1
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

{R1}

s
1

{R1}

s
2

...

s
n-1

{R}
P is correct, if each step is correct, i.e. the following Hoare triples hold:
• {Q} s0 {R1},
• {R1} s1 {R2},
• ...
• {Rn-1} sn-1 {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} x1:=x0+1 {x1>1}

When substituting, x
1>1 becomes x0+1>1, which you can deduce from x0>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} P1{R} and {Q/\ B'} P2 {R} hold,

then the Hoare triple above holds.
Exemple 5   [, Exercise 11 p. 78]

### 1.3.4  Loop Rule

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 non-negative 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 ik, jk and Sk be the value of i, j and S after k iterations.

Base case: using the assignment rule, i0=0 and j0=0 so S0 holds.

Induction step:

Assume the invariant holds after k-1 iterations: jk-1=ik-1y

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:
{Sk-1/\(i=x)'}

j
k:=jk-1+y;

i
k:=ik-1+1;

{S
k}
Let's applying the assignment rule.

By substituting ik and jk by the expressions they have been assigned with, we get:
 Sk <=> jk = iky <=> jk-1+y = (ik-1+1)y (By the substitution rule) <=> ik-1y+y = (ik-1+1)y (By Sk-1) <=> ik-1y+y = ik-1y+y

So, Sk indeed holds.

By induction, after any number k of iterations, Sk still hold.

At the end, both Sk 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
partial-correctness.

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 non-negative 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 non-trivial.

Proof. Let ik and jk 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 Sk: gcd(ik, jk)=gcd(a,b).
1. Base case:

Before the loop, i0=a and j0=b.

So the invariant S0 holds: gcd(i0, j0)=gcd(a,b);

2. Induction step:

Assume Sk-1 holds, that is gcd(ik-1, jk-1)=gcd(a,b).

We just need to prove that gcd(ik, jk)=gcd(ik-1, jk-1).

By the assignment rule, we have:
• r is the rest of the division of ik-1 by jk-1,
• ik=jk-1,
• jk=r.
So, by the definition of the integer division, we have:
ik-1=qjk-1+jk
for some integer q.
1. Assume x divides both ik and jk.

Then, of course jk-1, since jk-1=ik.

By the equation above, x also divides ik-1.

2. Assume x divides both ik-1 and jk-1.

Then of course x divides ik.

Once again, using the equation above, x also divides jk

Therefore, gcd(ik, jk)=gcd(ik-1, jk-1)=gcd(a,b), as wanted.

3. 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 MACS-358 / Nicolas M. Thiéry
Last modified: Fri Jan 19 13:12:17 2007