Correctness of Algorithms

Correctness of algorithms: preconditions, postconditions, loop invariants, weakest precondition, structural rules, total correctness and partial correctness, halting problem.

Program state, condition (assertion), operations of logic (sentential calculus). Precondition and postcondition. External specification. Total correctness theorem. Weakest precondition method. Proof by structure of an algorithm. Deduction rules - empty program, superposition, assignment, if-clause. Partial correctness, halting problem. Loop invariant. While-clause.

Examples of proofs.

---

Define the state of a program (e.g. n-tuple of values of all variables, special value is needed for undefined variables).

Condition (assertion) is a proposition about the program state (true or false).

Conditions can be combined using logic operations of the sentential calculus  (negation, conjunction, disjunction, ,,,).

Precondition is a condition that holds before the execution of a program.

Postcondition is a condition that holds after the execution of a program.

External specification of a program is a pair  (Precondition, Postcondition).

Example

Theorem of total correctness: If the program starts the execution in a state that conforms to precondition, then the program finishes the execution in a state, that conforms to postcondition after finite number of steps (halting is important!).

Algorithm is (totally) correct (with regard to a given specification) if it is possible to prove the theorem of (total) correctness.

To prove the correctness w.r.t. specification (P, Q) we construct the weakest precondition Wp that is deducible from each precondition P.
We use the postcondition Q and structural rules for the algorithm to construct the Wp:  P => Wp && for the pair (Wp, Q) the (total) correctness can be proved.

Structural rules:

Empty algorithm - program state does not change.
Superposition (sequence of steps):  postcondition of the first step is precondition of the second step.
Assignment x:=e: replace all occurrences of the variable x in the postcondition Q by expression e (evaluation of e must be free from side-effects).
If-statement: branches have the same postconditon Q, precondition is combined from preconditions of the branches and if-condition.
if (t) A1 else A2; 
(t && Wp1|| !t  && Wp2, Q)

For loops we need a notion of partial correctness: if the program starts the execution in a state that conforms to precondition, then the program finishes the execution in a state, that conforms to the postcondition  or the execution does not stop at all (program does not halt).

Halting theorem: if the program starts the execution in a state that conforms to precondition, then the program finishes the execution after finite number of steps.

Total correctness = Partial correctness + Halting

Loop invariant: condition that holds before each step of the loop.

while-loop:  while(t) A;      loop invariant is R

1. for each step A: {t&&R}A{R}
2. !t && R  => Q   (after execution the postcondition Q holds)
3. P => R  (before execution the invariant holds)

To prove the total correcnes of a loop we need to construct the loop invariant and prove both partial correctness theorem and halting theorem.


Example: FPP prover  http://psc.informatik.uni-jena.de/fpp/fpp-main.htm

FPP (Frege Program Prover) University of Jena, Germany

--!pre       : (x + y = m);
 
--> wp       :     (x >= 1 + y AND y <= x AND x + y = m)
-->            OR (x < 1 + y AND x <= y AND x + y = m)
--> vc       :      (x + y = m)
-->            ==>     (x >= 1 + y AND y <= x AND x + y = m)
-->                 OR (x < 1 + y AND x <= y AND x + y = m)
--> Result: proved

IF x > y THEN 
   a := x;
   x := y;
   y := a;
END IF;

--!post      : (x <= y AND x + y = m);

--> wp       : (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)

IF x >= y THEN 
   y := x;
ELSE
   x := y - 2;
END IF;

--!post: (x + y = 0);

--!pre       : (x <= 0 AND y = 1 OR x = 0 AND y <= 0);
 
--> wp       : (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)
--> vc       :      (x <= 0 AND y = 1 OR x = 0 AND y <= 0)
-->            ==> (x >= y AND 2*x = 0 OR x < y AND -2 + 2*y = 0)
--> Result: proved

IF x >= y THEN 
   y := x;
ELSE
   x := y - 2;
END IF;

--!post: (x + y = 0);

s := 0;

--!pre       : (s = 0 AND n >= 1);
--!post      : (s = n*(1 + n)/2);
--!inv       : (s = i*(1 + i)/2);
 
-->functionality ---------------------------
-->func      : (initial AND induction AND final AND null loop)
-->initial   :(1 <= n AND s = 0 AND n >= 1 => s = 0)
--> Result    : proved
-->induction :(1 <= n AND s = (-1 + i)*i/2 => i + s = i*(1 + i)/2)
--> Result    : proved
-->final     :(1 <= n AND s = n*(1 + n)/2 => s = n*(1 + n)/2)
--> Result    : proved
-->null loop :(1 >= 1 + n AND s = 0 AND n >= 1 => s = n*(1 + n)/2)
--> Result    : proved

FOR i IN 1 .. n  LOOP
   s := s + i;
END LOOP;

--!pre       : (i >= 1 AND j >= 1 AND i = k1 AND j = k2);
--!post      : (i = j AND i = GGT(k1,k2));
--!inv       : (i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2));
--!term      : (j + i);

-->functionality ---------------------------
-->initial   :     (i >= 1 AND j >= 1 AND i = k1 AND j = k2)
-->            ==> (i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
--> Result    : proved
-->induction :     (i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==>          (i >= 1 + j)
-->                     AND (-j + i >= 1)
-->                     AND (j >= 1)
-->                     AND (GGT(i,j) = GGT(k1,k2))
-->                 OR (i < 1 + j AND i >= 1 AND j - i >= 1 AND GGT(i,j) = GGT(k1,k2))
--> Result    : proved
-->final     :     (i = j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==> (i = j AND i = GGT(k1,k2))
--> Result    : proved
-->termination ---------------------------
-->initial   :(i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2) => j + i >= 1)
--> Result    : proved
-->induction :     (i /= j AND i >= 1 AND j >= 1 AND GGT(i,j) = GGT(k1,k2))
-->            ==> (i >= 1 + j AND j + i >= 1 + i OR i < 1 + j AND j + i >= 1 + j)
--> Result    : proved

WHILE i /= j LOOP
   IF i > j THEN 
      i := i - j;
   ELSE
      j := j - i;
   END IF;
END LOOP;

--!pre       : (n >= 3);
 
--> wp       : (2 <= n)
--> vc       : (n >= 3 => 2 <= n)
--> Result: proved

f0 := 0;
f1 := 1;
i := 2;
fi := f0 + f1;

--!pre       :      (f0 + f1 = fi)
-->            AND (i <= n)
-->            AND (i = 2)
-->            AND (2**i/4 >= 1 + f0)
-->            AND (2**i/2 >= 1 + f1);
--!post      : (2**n >= 1 + fi);
--!inv       : (f0 + f1 = fi AND 2**i/4 >= 1 + f0 AND 2**i/2 >= 1 + f1);

-->functionality ---------------------------
-->func      : (initial AND induction AND final AND null loop)
-->initial   :          (3 <= n)
-->                 AND (f0 + f1 = fi)
-->                 AND (i <= n)
-->                 AND (i = 2)
-->                 AND (2**i/4 >= 1 + f0)
-->                 AND (2**i/2 >= 1 + f1)
-->            ==> (f0 + f1 = fi AND 1 >= 1 + f0 AND 2 >= 1 + f1)
--> Result    : proved
-->induction :     (3 <= n AND f0 + f1 = fi AND 2**i/8 >= 1 + f0 AND 2**i/4 >= 1 + f1)
-->            ==> (2**i/4 >= 1 + f1 AND 2**i/2 >= 1 + fi)
--> Result    : proved
-->final     :     (3 <= n AND f0 + f1 = fi AND 2**n/4 >= 1 + f0 AND 2**n/2 >= 1 + f1)
-->            ==> (2**n >= 1 + fi)
--> Result    : proved
-->null loop :          (3 >= 1 + n)
-->                 AND (f0 + f1 = fi)
-->                 AND (i <= n)
-->                 AND (i = 2)
-->                 AND (2**i/4 >= 1 + f0)
-->                 AND (2**i/2 >= 1 + f1)
-->            ==> (2**n >= 1 + fi)
--> Result    : proved

FOR i IN 3 .. n  LOOP
   f0 := f1;
   f1 := fi;
   fi := f0 + f1;
END LOOP;

Jaanus Pöial