Previous: Induction, RecursionInduction, Recursion Up: Class notesClass notes Next: Analysis Of AlgorithmsAnalysis Of Algorithms
Document also available in PDF, Postscript, DVI, Text, LaTeX, LyX.

Proof Of Correctness

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
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?

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((0<=i) && (i<MAX));


Each assertion is automatically checked:
Assertion failed, line 35 of file foo.c
With C++, java and other languages, you can use exceptions instead of assert: 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) {


  if (n==0) return 1;

  return n*factorial(n-1);

The specification of a program can be formalized as follow:
Exemple 1   Program to compute of a square root
Définition 3   P is correct if (for all X) Q(X)-> R(X,P(X)).

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:




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








P is correct, if each step is correct, i.e. the following Hoare triples hold: 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:

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:

if condition B then




end if

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:

while condition B do



{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:

while condition B do



{S/\ B'}

1.3.5  A simple example

Consider this little program:

// Precondition: x and y are non-negative integers

// Postcondition: returns the product of x and y




  while ( (i=x)' ) do



  end while

  // Assertion: { j = x*y }


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:



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

A full proof of correctness needs also a proof of termination!

1.3.6  A more sophisticated example: The Euclidean algorithm



// 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



  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.


Exercice 1   Use the Euclidean algorithm to compute:

, 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: So, by the definition of the integer division, we have:
    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:

1.4.2  Check assertions in your programs!

Valid HTML 4.0! Previous: Induction, RecursionInduction, Recursion Up: Class notesClass notes Next: Analysis Of AlgorithmsAnalysis Of Algorithms
Proof Of Correctness / CSM MACS-358 / Nicolas M. Thiéry
Last modified: Fri Jan 19 13:12:17 2007