The axiomatic approach to semantics takes a rather unusual view of the meaning of "meaning", i.e., that the meaning of a program is the set of true statements about it. The idea is that the semantic definition of a language should allow true properties (and only true properties) to be proved about programs of the language. For example, one might wish to prove that a program has certain outputs given certain inputs, or that a program always runs to completion (terminates).

Assertions and Pre-Post Formulas

In order to prove properties about programs axiomatic semantics deals in assertions about the values of program variables. Allowable assertions include all the standard operators of mathematics and logic. For example, \(x < 5\) is an assertion that the variable \(x\) has a value less than 5, and \(y = 0 \vee x/y > 2\) asserts that either \(y\) has the value 0 or the ratio of \(x\) to \(y\) is greater than 2. In addition to these standard types of assertion, axiomatic semantics has one special form of assertion called a Hoare triple or pre-post formula which has the form \[\lbrace P \rbrace \mathrm{S} \lbrace Q\rbrace\] where \(P\) and \(Q\) are simple logical assertions as above and \(S\) is a statement of the programming language. The meaning of such an assertion is that if \(P\) is true before execution of \(\mathrm{S}\) and \(\mathrm{S}\) executes to completion, then \(Q\) is true after execution of \(\mathrm{S}\). \(P\) and \(Q\) are called, respectively, the precondition and postcondition of the assertion.

Assignment Axiom (A1)

The axiomatic semantics of the language is defined by specifying, for each type of statement S of the language, the conditions under which pre-post formulas involving S can be assumed to be true. For example, the rule for assignment statements (typically) is that all assertions of the form \[\lbrace P[x \leftarrow t] \rbrace \mbox{$x$ := $t$} \lbrace P \rbrace\] are true, where \(P[x \leftarrow t]\) means the assertion obtained by substituting the expression \(t\) for all occurrences of \(x\) in the assertion \(P\). According to this rule, the following assertions are true. \[\lbrace y = 7 \rbrace {\mbox{\(x\) := \(x\) + 1}} \lbrace y = 7 \rbrace \] \[\lbrace x + 1 = 8 \rbrace {\mbox{ \(x\) := \(x\) + 1}} \lbrace x = 8 \rbrace \]

In the first case, the postcondition does not involve \(x\) , so no substitutions have to be made to derive the precondition. In the second case, a substitution is required: \(x\) in the postcondition is replaced by \(x + 1\) in the precondition. Both of these assertions correspond with what we expect to be true about assignment statements. The rule \[\lbrace P[x \leftarrow t] \rbrace \mbox{$x$ := $t$} \lbrace P \rbrace\] is called the assignment axiom.

Weakest Precondition

The condition \(P[x \leftarrow t]\) is called the weakest precondition for the statement \(\mbox{$x$ := $t$}\) and the postcondition \(P\). In general, the weakest precondition is the one which places the fewest restrictions on program variables and still gives the validity of a given postcondition. Consider, for example, the statement \(\mbox{$x$ := $y + 3$}\) and the postcondition \(x > 0\). This postcondition is true with the precondition \(y > 0\), and also with the weakest precondition \(y + 3 > 0\). \[\lbrace y > 0 \rbrace {\mbox{\(x\) := \(y\) + 3}} \lbrace x > 0 \rbrace \] \[\lbrace y + 3 > 0 \rbrace {\mbox{\(x\) := \(y\) + 3}} \lbrace x > 0 \rbrace \] Note, however, that \(y > 0\) makes a stronger statement about the value of \(y\) than does \(y + 3 > 0\), since the former excludes the values -2 and -1 for \(y \), whereas the latter allows those values.

Finding the weakest precondition allows proofs for the most general case (fewest restrictions on input values) to be found. In general, the axiomatic definition of programming languages seeks to provide rules for determining the weakest precondition given any language statement S and any postcondition \(Q\).

Composition Rule (R1)

Many of the rules in axiomatic semantics require that the truth of one pre-post formula be based on the truths of other pre-post formulas. For example, the truth of \[\lbrace P \rbrace \mathrm{S1; S2} \lbrace Q\rbrace\] follows if and only if there is an assertion \(R\) such that \[\lbrace P \rbrace \mathrm{S1} \lbrace R\rbrace\] \[\lbrace R \rbrace \mathrm{S2} \lbrace Q\rbrace\] are both true. A rule of this type is known as a rule of inference and is usually expressed using the following notation.

\[\lbrace P \rbrace \mathrm{S1} \lbrace R\rbrace , \lbrace R \rbrace \mathrm{S2} \lbrace Q\rbrace\ \over \lbrace P \rbrace \mathrm{S1; S2} \lbrace Q\rbrace \]

If each of the conditions listed above the line holds, it is then valid to infer the truth of the assertion below the line. This particular rule is usually called the composition rule and describes how proofs about sequences of statements can be derived from proofs about individual statements (in this formulation, a sequence of statements is treated as a type of statement itself).

Example 1

Using the assignment axiom and the rule of composition, prove that the following sequence of statements exchanges the values of variables x and y.

\[ \begin{array}{l} x := x - y; \newline y := x + y; \newline x := y - x; \end{array} \]

In order to do the proof, we must first establish appropriate pre- and postconditions. The precondition is simply that \(x\) and \(y\) have some particular values, say \(A\) and \(B\): \[x=A \wedge y=B\] The postcondition is that these values are exchanged: \[x=B \wedge y=A\] The problem is thus to prove the validity of the following pre-post formula.

\[ \begin{array}{l} \lbrace x=A \wedge y=B \rbrace \newline x := x - y; \newline y := x + y; \newline x := y - x; \newline \lbrace x=B \wedge y=A \rbrace \end{array} \]

A standard strategy in such proofs is to work backwards from the desired result. Start with the final statement and the given postcondition and derive a valid pre-post formula involving that statement, i.e., find \(P_1\) in the following.

\[ \begin{array}{l} \lbrace P_1 \rbrace \newline x := y - x; \newline \lbrace x=B \wedge y=A \rbrace \end{array} \]

Using the assignment axiom, the desired precondition is derived by back substitution of \(y-x\) for \(x\) in the postcondition, giving the following.

\[ \begin{array}{lr} \lbrace y-x=B \wedge y=A \rbrace &\newline x := y - x; & \mathrm{(A1)}\newline \lbrace x=B \wedge y=A \rbrace & \end{array} \]

A similar process is then carried out using the newly derived precondition of the last statement as the postcondition for the penultimate (second last) statement. Using the assignment axiom once more, the precondition is again found by back substitution, this time of \(x+y\) for \(y\).

\[ \begin{array}{lr} \lbrace x+y-x=B \wedge x+y=A \rbrace \newline y := x + y; & \mathrm{(A1)}\newline \lbrace y-x=B \wedge y=A \rbrace &\newline x := y - x; & \mathrm{(A1)}\newline \lbrace x=B \wedge y=A \rbrace & \end{array} \]

Here lines 1 through 3 are one pre-post formula and lines 3 through 5 are another valid pre-post formula. By the rule of composition, lines 1, 2, 4 and 5 are another valid pre-post formula. With a logical simplification of the precondition this yields.

\[ \begin{array}{lr} \lbrace y=B \wedge x+y=A \rbrace \newline y := x + y; & \mathrm{(R1)}\newline x := y - x; & \newline \lbrace x=B \wedge y=A \rbrace & \end{array} \]

For convenience, then, we can simply insert assertions between consecutive statements and chain all of the results together.

Extending this process one more time, the precondition of the final two statements now becomes the postcondition of the first. Again, the assignment axiom lets us derive the weakest precondition.

\[ \begin{array}{lr} \lbrace y=B \wedge x-y+y = A\rbrace & \newline x := x - y; & \mathrm{(A1)}\newline \lbrace y=B \wedge x+y=A \rbrace &\newline y := x + y; & \newline x := y - x; & \newline \lbrace x=B \wedge y=A \rbrace & \end{array} \]

With simplification and reordering of the precondition, and applying the composition rule, we then establish the validity of the desired pre-post formula.

\[ \begin{array}{lr} \lbrace x = A \wedge y = B\rbrace & \newline x := x - y; & \newline y := x + y; & \mathrm{(R1)} \newline x := y - x; & \newline \lbrace x=B \wedge y=A \rbrace & \end{array} \]

This completes the proof.

The Consequence Rule (R2)

In addition to the rules for assignment and composition, there are also some general purpose rules of inference that are often needed for axiomatic proofs. These rules are not related to any particular language constructs and apply in general to axiomatic proofs in any language. The consequence rule allows us to make substitutions of stronger preconditions and/or weaker postconditions, as follows. \[ P \implies P_1, \lbrace P_1 \rbrace \mbox{S} \lbrace Q_1 \rbrace, Q_1 \implies Q \over \lbrace P \rbrace \mbox{S} \lbrace Q \rbrace \] This rule states that, for any given pre-post formula \(\lbrace P_1 \rbrace \mbox{S} \lbrace Q_1 \rbrace \) , \(P_1\) can be replaced by any condition \(P\) from which \(P_1\) can be inferred (\(P \implies P1\)) and \(Q_1\) can be replaced by any condition \(Q\) which it implies. This rule just allows us to formally make the substitutions that we informally recognize as valid.

The And Rule (R3) and the Or Rule (R4)

The And rule and the Or rule are also general purpose rules that are used for logical reasoning. \[ \lbrace P_1 \rbrace \mbox{S} \lbrace Q_1 \rbrace, \lbrace P_2 \rbrace \mbox{S} \lbrace Q_2\rbrace \over \lbrace P_1 \wedge P_2 \rbrace \mbox{S} \lbrace Q_1 \wedge Q_2 \rbrace \]

\[ \lbrace P_1 \rbrace \mbox{S} \lbrace Q_1 \rbrace, \lbrace P_2 \rbrace \mbox{S} \lbrace Q_2\rbrace \over \lbrace P_1 \vee P_2 \rbrace \mbox{S} \lbrace Q_1 \vee Q_2 \rbrace \]

In practice, the latter two rules are infrequently used, but the consequence rule is often applied.

The If-Then-Else Rule (R5)

In addition to assignment and statement sequencing, there are two other common types of control structure in programming languages, namely conditional statements and repetitive statements.

As a typical representative for the conditional constructs of many languages, the if statement can be specified by the following rule of inference. (Here, the fi keyword is used to mark the end of the if statement in the style of Algol 68.) \[\lbrace P \wedge E \rbrace \mbox{S1} \lbrace Q \rbrace, \lbrace P \wedge \neg E \rbrace \mbox{S2} \lbrace Q \rbrace \over \lbrace P \rbrace \mathtt{if {\rm \,E\,} then {\rm \,S1\,} else {\rm \,S2\,} fi} \lbrace Q \rbrace\]

This rule states the conditions under which an assertion about an if statement can be inferred from assertions for the then and else branches of the statement. It can be used in the proof of an if-then-else asserted program by breaking the proof into two subsidiary proofs, one each for the then and else branches. Note that along the then branch, the precondition is augmented to include the statement predicate (the if part); this reflects the fact that the then branch is not executed unless the predicate is true. Similarly, the precondition along the else branch includes the logical negation of the predicate.

The While Rule (R6)

The axiomatic treatment for iterative constructs can be illustrated by the rule for while loops. \[\lbrace P \wedge E \rbrace \mbox{S} \lbrace P \rbrace, \over \lbrace P \rbrace \mathtt{while {\rm \,E\,} do {\rm \,S\,} od} \lbrace P \wedge \neg E \rbrace\] Note that, in this rule, the precondition \(P\) is also part of the postcondition; \(P\) is said to be a loop invariant.

Finding an appropriate loop invariant is often the critical step in proofs. Of course, there are many conditions which are trivially invariant through the execution of a loop, for example, any condition which does not depend on any loop variables. In general, however, such conditions are of no use in doing axiomatic proofs; what is needed is a condition which is some sort of invariant relationship between various loop variables. Such a condition must be true of the initial values of loop variables and true after each execution of the loop body. The nature of such loop invariants will be better illustrated in the example below.

The simple language defined to include only assignments, compound statements, if-then-else statements and while loops is called SLINT. It is not a real language, but is useful to demonstrate basic axiomatic techniques without the complexities in larger languages. Its axiomatic semantics consist exactly of the rules introduced above, i.e., the assignment axiom and composition, if-then-else and while rules plus the three general purpose rules R2, R3 and R4. Although the SLINT is simple in nature it can be used to illustrate nontrivial proofs of program correctness.

Example 2

Consider the following program S for performing integer division of the natural numbers x and y.

\[ \begin{array}{l} q := 0; \newline r := x; \newline \mathtt{while {\rm \,r >= y\,} do} \newline \text{ } r := r - y; \newline \text{ } q := q + 1; \newline \mathtt{od} \end{array} \]

Show that \(\lbrace P_0 \rbrace \mathrm{S} \lbrace Q_0 \rbrace \) holds where \(P_0\) is \(x \geq 0 \wedge y \geq 0\) and \(Q_0\) is \(q \times y + r = x \wedge 0 \leq r < y\). That is, if \(x\) and \(y\) are nonnegative integers and the program runs to completion then \(q\) and \(r\) are respectively the quotient and remainder of \(x\) divided by \(y\).

Following the normal approach in axiomatic proofs, we work backwards from the desired result. By the composition rule, the proof is complete if we can find an assertion \(P_1\) that is both the precondition of the while loop and the post condition of the two initial assignments.

\[ \begin{array}{l} \lbrace P_0 \rbrace \newline q := 0; \newline r := x; \newline \lbrace P_1 \rbrace \newline \mathtt{while {\rm \,r >= y\,} do} \newline \text{ } r := r - y; \newline \text{ } q := q + 1; \newline \mathtt{od} \newline \lbrace Q_0 \rbrace \end{array} \]

Now \(P_1\) can be analyzed as the precondition of the while loop, based on the while rule and the given postcondition. \(P_1\) is, in fact, the loop invariant, and its determination is the essential step in doing the proof.

The nature of \(P_1\)can be discovered by looking at the general form of pre-post formulas for while loops as taken from the while rule. \[\lbrace P \wedge E \rbrace \mbox{S} \lbrace P \rbrace, \over \lbrace P \rbrace \mathtt{while {\rm \,E\,} do {\rm \,S\,} od} \lbrace P \wedge \neg E \rbrace\] By matching \(P \wedge \neg E\) against the postcondition \(Q_0\), i.e,. \(q \times y + r = x \wedge 0 \leq r < y\), we might guess that \(P_1\) should be taken as \(q \times y + r = x \wedge 0 \leq r\), since the assertion \(r < y\) corresponds to \(\neg E\). Informally, we note that this condition is true before the loop is executed, since \(q \times y + r = 0 \times y + r = r = x\) and \(x \geq 0\) is given implying \(r \geq 0\). Also note that each time through the loop the value of \(q \times y\) increases by \(y\), while the value of \(r\) decreases by \(y\), so their sum, which is initially \(x\) , remains invariant. The value of \(r\) always remains greater than 0 since it is only decremented by \(y\) each time and the loop is not entered if \(r <y\). Thus, our guess looks correct and the condition \[q \times y + r = x \wedge 0 \leq r\] should be the desired loop invariant \(P_1\). Now we just need to prove it using formal steps.

With this determination of \(P_1\), then, we can restate our proof goal as follows. \[ \begin{array}{l} \lbrace x \geq 0 \wedge y \geq 0 \rbrace \newline q := 0; \newline r := x; \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace \newline \mathtt{while {\rm \,r >= y\,} do} \newline \text{ } r := r - y; \newline \text{ } q := q + 1; \newline \mathtt{od} \newline \lbrace q \times y + r = x \wedge 0 \leq r < y \rbrace \end{array} \]

Focussing on the while loop, we establish the conditions for the while rule. \[ \begin{array}{l} \lbrace q \times y + r = x \wedge 0 \leq r \rbrace \newline \mathtt{while {\rm \,r >= y\,} do} \newline \lbrace q \times y + r = x \wedge 0 \leq r \wedge r \geq y \rbrace \newline \text{ } r := r - y; \newline \text{ } q := q + 1; \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace \newline \mathtt{od} \newline \lbrace q \times y + r = x \wedge 0 \leq r < y \rbrace \end{array} \]

Note that we have added the condition \(r \geq y\) to the precondition of the loop body as specified by the while rule. Working backwards, we know that the following assertion is valid by the assignment axiom. \[ \begin{array}{lr} \lbrace (q+1) \times y + r = x \wedge 0 \leq r \rbrace & \newline \text{ } q := q + 1; & \mbox{(A1)} \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace & \end{array} \]

Using the assignment axiom one more time we get the following valid assertion. \[ \begin{array}{lr} \lbrace (q+1) \times y + (r-y) = x \wedge 0 \leq (r-y) \rbrace\newline \text{ } r := r - y; & \mbox{(A1)} \newline \lbrace (q+1) \times y + r = x \wedge 0 \leq r \rbrace &\newline \end{array} \] Using simplification and the rule of composition on these last two pre-post formulas gives us the following. \[ \begin{array}{lr} \lbrace q \times y + r= x \wedge r \geq y \rbrace\newline \text{ } r := r - y; & \mbox{(R1)} \newline \text{ } q := q + 1; & \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace& \end{array} \]

Because we have established the pre-post formula required for the loop body, we can now conclude that our pre-post formula for the entire while loop is correct, using the while rule.

To complete the proof, it now just remains to work through the initialization statement to show the validity of the following pre-post formulas. \[ \begin{array}{l} \lbrace x \geq 0 \wedge y \geq 0 \rbrace \newline q := 0; \newline r := x; \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace \newline \end{array} \]

Two applications of the assignment axiom gives. \[ \begin{array}{lr} \lbrace 0 \times y + x = x \wedge 0 \leq x \rbrace & \newline q := 0; & \mbox{(A1)} \newline \lbrace q \times y + x = x \wedge 0 \leq x \rbrace & \newline r := x; & \mbox{(A1)} \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace &\newline \end{array} \]

The precondition here reduces to \(x \geq 0\). But since \(x \geq 0 \wedge y \geq 0\) implies \(x \geq 0\), we can also determine the following pre-post formula is correct via the consequence rule. \[ \begin{array}{lr} \lbrace x \geq 0 \wedge y \geq 0\ \rbrace & \newline q := 0; & \newline \lbrace q \times y + x = x \wedge 0 \leq x \rbrace & \mbox{(R2)}\newline r := x; & \newline \lbrace q \times y + r = x \wedge 0 \leq r \rbrace &\newline \end{array} \]

This completes the proof.

In this example, note that the division is performed correctly whenever \(x >= 0\) and \(y > 0\), but that the program does not terminate if \(y = 0\). Nevertheless, the pre-post formula is valid in both cases. In general, proving a pre-post formula means that if the program terminates, it gives the correct result. Proving such a pre-post-formula is often said to be a proof of partial correctness; a proof of total correctness also requires a proof that the program terminates. Such proofs require additional axiomatic techniques that we will not go into here.

Viewpoint on Axiomatic Semantics

We have introduced axiomatic semantics for a simple programming language with a small number of constructs. Researchers in the area have also developed techniques for handling more difficult sorts of language constructs such as procedure calling with parameters, recursion and subscripted variables. Unfortunately, axiomatic semantics cannot be practically applied to most current programming languages, however, as these languages generally violate certain necessary assumptions for the validity of axiomatic semantics.

From an axiomatic viewpoint, the biggest problems with most current languages are the possibilities of side-effects in expressions and aliasing of variables. Side-effects in expressions typically arise when a function call within the expression results in the value of a global variable being changed. Such a possibility would invalidate the assignment axiom and the rules of inference for if-then-else statements and while loops. Aliasing of variables refers to the possiblity that two different names may be used to denote the same memory location. This typically happens using call-by-reference parameter passing (var parameters in Pascal). Aliasing invalidates the assignment axiom; the precondition under aliasing would have to be modified to substitute the expression for all variables that named the same location as the variable to which the assignment was being made.

The problems of applying axiomatic semantics to current languages suggest new language design principles to support axiomatic definitions. Two positive steps would be to prohibit side effects in expressions and eliminate aliasing. This, coupled with ongoing research into automated program verification systems, could lead to programming languages and environments supporting the development of highly reliable programs.