CHAPITRE 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. 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. 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 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. 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. P is correct if (∀X) Q(X) → R(X, P (X)).

A Hoare triple is just a short hand notation : {Q} P {R}

Exemple. {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_{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}

        {R_{1}}

s_{1}

        {R_{1}}

s_{2}

        ...

s_{n−1}

        {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_{n−1}} s_{n−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. If from Q you can derive R with x substituted everywhere by e,

then the Hoare triple is valid.

Exemple. {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. {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. If the Hoare triples {Q ∧ B} P_{1}{R} and {Q ∧ B′} P_{2} {R} hold, then the Hoare triple above holds.

Exemple. [?, 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. 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.

Démonstration. 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 k − 1 iterations : j_{k−1} = i_{k−1}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_{k−1} ∧ (i = x)′}

j_{k} := j_{k−1} + y;
i_{k} := i_{k−1} + 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_{k−1} + y = (i_{k−1} + 1)y (By the substitution rule)
⇔ i_{k−1}y + y = (i_{k−1} + 1)y (By S_{k−1})
⇔ i_{k−1}y + y = i_{k−1}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. 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.

Démonstration. 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).

(1) 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) ;

(2) Induction step : Assume S_{k−1} holds, that is gcd(i_{k−1}, j_{k−1}) = gcd(a, b). We just need to prove that gcd(i_{k}, j_{k}) = gcd(i_{k−1}, j_{k−1}). By the assignment rule, we have :

– r is the rest of the division of i_{k−1} by j_{k−1},

– i_{k} = j_{k−1},

– j_{k} = r. So, by the definition of the integer division, we have :

i_{k−1} = qj_{k−1} + j_{k}

for some integer q.

(a) Assume x divides both i_{k} and j_{k}. Then, of course j_{k−1}, since j_{k−1} = i_{k}. By the equation above, x also divides i_{k−1}.

(b) Assume x divides both i_{k−1} and j_{k−1}. 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_{k−1}, j_{k−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