CS217 Day 26 Friday, May 26, 2000

Program Correctness

We have had a lot of experience with recursively defined programs, where the correctness of a program is argued from
• its correctness on base cases, and
• its conditional correctness on inductive cases.
The foundation for this argument is (structural) mathematical induction for inductively specified programs, as discussed on Day 2.

And there is a large literature on reasoning about programs with no side effects (the state or environment is not mutated) based on the evaluation rule

let p = proc(x) E
in (p a)

=>

E[x = a]

where E[x = a] denotes the result of substituting a for each free occurrence of x in E.

But computer programs generally operate by

• initializing an environment or state, and
• modifying the state by successive assignment.
The result of a program is its final state.

A program S is correct if it

• begins in a state where the program variables satisfy a given (pre)condition P, and
• terminates in a state satisfying a given (post)condition Q.

The correctness of programs is formalized in the notion of Hoare triples

{P} S {Q}

(In the following, we will use % for comments, as used in our defined language.)

The formal theory of program correctness was developed, starting in the late 1960's by Peter Naur, Robert Floyd, Tony Hoare, David Gries, Edsger Dijkstra and others. (See Gries, The Science of Programming, 1981, pp297-301 for an early history.)

In the following, we define Hoare triples and state the axioms or rules from which the correctness of a program can be formally deduced.

Most striking are

• the Rule for Assignment, where the weakest precondition for any postcondition is obtained by simple substitution in the postcondition, and
• the Rule for While, where correctness is defined in terms of loop invariants and bounding functions.
• Hoare Triples

  The triple

  % P
  S
  % Q
  

  holds, and is said to be a Hoare triple, if
  • P, Q are boolean expressions and S is a program.
  • If P holds for values of program variables (initial state)
    and S is executed,
    then Q will hold for the resulting values of program variables (terminal state).

  Given a Hoare triple, program S is correct, in the sense that

  • if precondition P holds before executing S, then
  • postcondition Q holds after executing S.

• Rules for establishing Hoare triples
  • Rule for Assignment

    % Q[x = E]
    set x = E
    % Q
    

    and

    P => Q[x = E]
    -----------
    % P
    set x = E
    % Q
    

    Q[x = E] is the weakest precondition for the postcondition Q
    -- any condition that implies it is a precondition.

    Establishing

    % P
    set x = E
    % Q
    

    is reduced to proving the validity of P => Q[x = E].
    • Example.
      Since

           (x > a)[x = x + y]
      =
           x + y > a
      

      the Rule for Assignment asserts

      % x + y > a
      set x = +(x, y)
      % x > a
      

      Let's check this.
      • Suppose the program state is [x -> X, y -> Y].
      • If x + y > a holds, then X + Y > a.
      • After executing set x = +(x, y), the state is [x -> X + Y, y -> Y].
      • The postcondition x > a holds then holds because X + Y > a.

    • In general

      Suppose Q[x = E] holds in a state [x -> X, y -> Y, ...].
      I.e,

      Q[x = E][x -> X, y -> Y, ...]
      

      holds. This is the same as

      (Q[x = E[x -> X, y -> Y, ...]])[x -> X, y -> Y, ...]
      

      or

      (Q[x = X1])[x -> X, y -> Y, ...]
      

      where

      X1 = E[x -> X, y -> Y, ...]
      

      That is,

      Q[x -> X1, y -> Y, ...]
      

      But, after executing set x = E,
      the state is [x -> X1, y -> Y, ...],
      where X1 = E[x -> X, y -> Y, ...].

      Thus, Q holds in the resulting state, and

      % Q[x = E]
      set x = E
      % Q
      

      is a Hoare triple.

  • Rule for Begin

    % P
    S1
    % Q
    
    % Q
    S2
    % R
    --------------
    % P
    begin
      S1;
      S2
    end
    % R
    

  • Rule for Sequential Assignment

    % Q[y = E2][x = E1]
    begin
      set x = E1;
      set y = E2;
    end
    % Q 
    

    Note: This rule is counter-intuitive and is easily misapplied.
    The postcondition is backed up through a sequence of substitutions -- last to first.
    • For example (Swap),

      % x = X and y = Y
      begin
        tmp = x;
        x = y;
        y = tmp
      end
      % x = Y and y = X
      

      because

           (x = Y and y = X)[y = tmp][x = y][tmp = x]
      =
           (x = Y and tmp = X)[x = y][tmp = x]
      =
           (y = Y and tmp = X)[tmp = x]
      =
           (y = Y and x = X)
      

  • Rule for If

    % P and Q
    S1
    % R
    
    % P and ~Q
    S2
    %R
    ---------------
    % P
    if Q then S1 else S2
    % R
    

  • Rule for While -- assuming termination

    For a loop while B do S that terminates, the rule asserts that

    • if P is an invariant for S with guard B,
    • then P and ~B holds upon termination.
    Formally,

    % P and B
    S
    % P
    ----------
    % P
    while B 
    do S
    % P and ~B
    

    The postcondition P and ~B holds at termination because
    • P holds after every iteration, and
    • at termination, B is false.

  • Rule for While -- concluding termination

    A bounding function for while B do S is an integer expression that

    • decreases when S is executed, and
    • is positive whenever B holds

    A while loop with a bounding function terminates. Formally,

    % T = T0
    S
    % T < T0
    
    B => (T > 0)
    
    % P and B
    S
    % P
    -------------------
    % P
    while B 
    do S
    % P and ~B
    

    The loop terminates because after a finite number of iterations, T will no longer be positive, and B will be false.

• Examples
  • The sum of consecutive integers 0 + 1 + ... + n-1

    begin
      % n > 0
      set s = 0;
      set i = 0;
      % P: s = i*(i-1)/2
      % B: i < n
      % T = n - i is a bounding function
      while less(i, n) do
        begin
          set s = s + i;
          set i = i + 1
        end;
      % post: s = n*(n-1)/2
    

    This program is correct.
    • T is a bounding function.
      T decreases by 1 with each iteration and B => T > 0.

    • P is an invariant of the loop body.
      By the Rule for Sequence, we simply have to verify

      P[i = i + 1][s = s + i] => P
      

      This follows from the logical equivalences

           (s = i*(i-1)/2)[i = i + 1][s = s + i]
      =         
           (s = (i+1)*i/2)[s = s + i]
      =
           s + i = (i+1)*i/2
      =
           s = i*i/2 + i/2 - i = i*i/2 - i/2
      =
           s = i*(i-1)/2
      

    • At termination, s = n*(n-1)/2
      When the loop terminates, P still holds and n = i.

  • The sum of consecutive integers 1 + ... + n

    begin
      % n > 0
      set s = 0;
      set i = 0;
      % P: s = i*(i+1)/2
      % B: i < n
      % T = n - i is a bounding function
      while less(i, n) do
        begin
          set i = i + 1
          set s = s + i;
        end;
      % post: s = n*(n+1)/2
    

    This program is correct.

    The only difference in this program and the previous is the order of the assignments and the resulting changes in the loop invariant and post conditions.

    This time we need to prove

    P[s = s + i][i = i + i] => P
    

    Don't Forget: The order of substitution is the reverse of the order of assignment!!

  • Peasant or Egyptian Multiplication

    To multiply a and b, have available a big pile of stones and make space for piles x, y and p.

    • Put a stones in pile x.
    • Put b stones in pile y.
    • Clear out all the stones in pile p.

    • Separate the stones in pile y into two equal piles with possibly one left over.

      If there is none left over,

      • throw half the stones in y back into the big pile, and
      • add as many more stones to pile x as there were before.
      Otherwise,
      • toss the extra stone from y into the big pile, and
      • add as many stones to pile p as are in pile x.

      Keep doing this until there are no stones left in pile y.
      Then the number of stones in pile p will be a*b.

      E.g.,

      x              y           p
      27             13          0
      27             12          27
      54              6          27
      108             3          27
      108             2          135
      216             1          135
      216             0          351
      

      Here is a program:

      let x = a
          y = b
          p = 0
      in begin
           % P: p + x*y = a*b
           % B: y > 0
           % T = y, a bounding function
           while greater(y, 0) do
             begin
               if even?(y) then
                 begin
                   set x = +(x, x);
                   set y = /(y, 2)
                 end
               else
                 begin
                   set p = +(p, x);
                   set y = sub1(y)
                 end
             end;
           % post: p = a*b
           p
         end
      

      To show this program is correct, the main step is showing P is an invariant of the loop body. Using the axioms, we just have to show we can back up P by making the assignment substitutions in reverse order.

      There are two cases, y even and y odd.

      • Assume y is even

             (p + x*y = a*b)[y = y/2][x = 2x]
        =
             (p + x*(y/2) = a*b)[x = 2x]
        =
             (p + (2x)*(y/2) = a*b)
        =
             p + x*y = a*b
        

      • Assume y is odd

             (p + x*y = a*b)[y = y - 1][p = p + x]
        =
             (p + x*(y - 1) = a*b)[p = p + x]
        =
             ((p + x) + x*(y - 1) = a*b)
        =
             p + x*y = a*b
        

  • Peasant multiplication in Scheme

    Here is essentially the same program in Scheme, using a named let to implement the loop.

    (define peasantmult
      (lambda (a b)
        (let pm ((p 0) (x a) (y b))
          ;; Invariant: p + x*y = a*b
          (if (zero? y)
    	  ;; Post condition: p = a*b
    	  (if (not (= p (* a b)))
    	      (error 'pm "post condition error")
    	      (if (not (= (+ p (* x y)) (* a b)))
    		  (error 'pm "loop invariant error")))
    	  (begin
    	    (if (even? y)
    		(begin
    		  (set! x (* 2 x))
    		  (set! y (/ y 2)))
    		(begin
    		  (set! p (+ p x))
    		  (set! y (- y 1))))
    	    (pm p x y))))))
    

    E.g, (peasantmult 27 13) => 351

    The invariant and postconditions are commented.
    Error traps ensure the invariant and post conditions.

    This example was inspired by an ISETL example of Richard Nau.

  Done!