A Three-Valued Hoare Calculus

Viviana Bono

Manfred Kerber

If we consider programs on concrete computers then physical limitations have to be taken into account. The implemented integers, for instance, can form only a subset of all (mathematical) integers. This can be done (and is done in many programming languages) in the form that two integers MININT and MAXINT are defined and any integer computation that leads outside this range of integers leads to an error state. We will introduce a Hoare calculus that can deal with this phenomenon in an adequate way.

As soon as we consider concrete computers, functions are typically partial. Even addition is no longer total, since in a finite subset of INT, the sum of two big enough numbers will exceed any given bound (assumed addition in the subset is a restriction of standard addition). Let us assume that we have in our programming language integers which are defined as INT_f =INT intersection [MININT,MAXINT], where INT is the mathematical (infinite) set of all integers. Let us define MAXINT = 32768 and MININT = -32767, for instance. With this setting + is partial, since MAXINT + 1 is not defined and leads to a crash.

If we want to reason about crash as well, we have to consider how a Hoare triple (|precondition|) P (|postcondition|) should read. We keep the original reading: If the precondition holds and the program terminates then the postcondition holds. We could also have given a Hoare triple a weaker meaning, namely: " If the precondition holds, the program does not crash and terminates, then the postcondition holds." We don't follow this possible reading, since we want to be able to prove that the program does not crash and don't want to assume it.

Our programming language is a minimal language that has two types, the usual constructs of a Turing complete language, and the possibility of crash.

• The program that does not do anything: skip.

• The program that just crashes: crash.

• Assignment: x:= t assigns the term t of type INT to the variable x.

• Sequencing: P; Q means execute first P then Q.

• Conditional: IF C THEN P ELSE Q FI means that if the boolean expression C (of type BOOL) is true then P will be executed. If C is false then Q will be executed. To build conditional expressions we make use of the primitive binary predicates =, <, and <=, which result with terms s and t of type INT in boolean expressions of type BOOL. Note that a conditional expression may crash, e.g., for MAX<MAX+1.

• Loop: WHILE C DO P OD means that if the boolean expression C (of type BOOL) is true the program fragment P will repeatedly be executed until either C is false or crashes, or P itself crashes.

• The last construct is a finite version for a loop traversed at most k times (for a natural number k with a new counter nc, which must not occur in the program P). We write: WHILEF(nc k) C DO P OD . We are not interested in programs which make use of this construct, but use it only as a vehicle to reason about crashes of while loops.

An example program P is:

WHILE i < n DO
  i   := i + 1;
  sum := sum + i
OD

Logic

We define the semantics of the connectives as follows:

Note that the connective  &  is not symmetric (but associative). This is made in order to mirror the behaviour of the lazy boolean function and in the programming language (and the ones that can be defined like or). If the A in A and B is false the whole expression is false indiscriminately of the B. Likewise, if the evaluation of A crashes, the whole expression crashes. Only if the A evaluates to true, the second, the B, is evaluated and its value will be the value of the conjunction.

Quantification will always be guarded by a type T (or sort), FORALL x_T A and EXISTS x_T A. We assume a simple type system of (non-empty) disjoint types (we consider only T=INT).

We define I_phi( Q x_S A) := * Q({I_phi,[a/x](A) | a in A_S}) where Q in {FORALL,EXISTS} and furthermore ] From the semantics we can directly construct a tableau calculus analogously to the work in [KeKo96-KGS].

The Hoare calculus that can deal with crash makes use of the assignment schema:

(|D^t(t) &  A^t_x|) x:= t (|D^t(x) &  A|) with
A^t_x=A[x->t] replace all free x in A by t; and an axiom schema which says that we can't recover from crash: (|CRASH|) P (|CRASH|)

The rules consider the possibilities how a crash can be avoided or obtained, for instance, for an implication this means:

The second rule reads: if the precondition A of a rule implies that the condition C will crash, then the whole if-then-else expression will crash. The first rule is almost the traditional rule with the extension, however, that from the precondition A follows that the condition C will not crash. Note that for the first rule the postcondition B can also be CRASH.

Likewise we can build rules which characterise the behaviour of loops.

We have proved the soundness of the rules relative to an operational semantics following the approach outlined in [Mitchell96]. Proving a relative completeness property is left as future work.

With the calculus it is possible to establish:
(|D^t(n) & D^t(i) & D^t(sum) &  0<= n<= 255 &  i== 0 &  sum== 0|) P (|D^t(n) & D^t(i) & D^t(sum) &  sum == ½ n(n+1)|)
and (|D^t(n) & D^t(i) & D^t(sum) &  n== 256 &  i== 0 &  sum== 0|) P (|CRASH|)

Summary

References

• [KeKo96-KGS] Manfred Kerber and Michael Kohlhase. A tableau calculus for partial functions. Collegium Logicum - Annals of the Kurt-Gödel-Society, 2: 21-49, 1996.

• [Mitchell96] John C. Mitchell. Foundations of Programming Languages. MIT Press, Cambridge, Massachusetts, USA, 1996.