On the axiomatic definition of semantics

(The following is heavily influenced by the work of C.A.R.Hoare.)

Program testing can be used very effectively to show the presence of bugs, but is hopelessly inadequate for showing their absence and a convincing correctness proof seems the only way to reach the required confidence level.

In order that such a convincing correctness proof may exist, two conditions must be satisfied by such a correctness proof:

1) it must be a proof and that implies that we need a set of axioms to start with 2) it must be convincing and that implies that we must be able to write, to check, to understand and to appreciate the proof.

This essay deals with the first of these two topics.

We are considering finite computations only; therefore we can restrict ourselves to computational processes taking place in a finite state machine -although the possible number of states may be very, very large- and take the point of view that the net effect of the computation can be described by the transition from initial to final state. The computation is assumed to take place under control of an algorithm, a program, and what we want to do is to make assertions about all possible computations that may be evoked under control of such a program. And we want to base these assertions on the program text!

This implies that we must have a formal definition of the semantics of the programming language in which the program has been expressed.

The earliest efforts directed towards such definition of semantics that I am aware of have been what I call "mechanistic definitions": they gave a definition (or "a description") of the steps that should be carried out in executing a program, they gave you "the rules of the game", necessary to carry out any given computation (as determined by program and initial state!) by hand (or by machine). The basic shortcoming of this approach was that the semantics of an algorithm were expressed in terms of "the rules of the game", i.e. in terms of another algorithm. The game can only be played for a chosen

initial state, and as a result it is as powerless as program testing! A mechanistic definition as such is not a sound basis for making assertions about the whole class of possible computations associated with a program. It is this shortcoming, that the axiomatic method seeks to remedy.

We consider predicates $P, Q, R, \ldots$ on the set of states; for each possible state a given predicate will be either true of false and if we so desire, we can regard the predicate as characterizing the subset of states for which it is true. There are two special predicates, named $T$ and $F$ : $T$ is true for all possible states (characterizes the universe), $F$ is false for all possible states (characterizes the empty set). We call two predicates $P$ and $Q$ equal (" $P = Q$ ) when the sets of states for which they are true are the same. (Note that $P ≠ T$ or $non(P = T)$ does not allow us to conclude $P = F$ .)

We consider the semantics of a program S fully determined when we can derive for any set of final states, as characterized by a predicate P (called in this connection "the post-condition") the complete set of corresponding initial states, a set characterizes by the predicate that we denote by fS(P) and that in this connection is called "the weakest pre-condition" or "the pre-condition" for short. Here we regard the fS as a "predicate transformer", as a rule for deriving the weakest pre-condition from the post-condition to which it corresponds.

The semantics of a program $S$ are defined when the corresponding predicate transformer fS is given, the semantics of a programming language are defined when the rules are given how to construct the predicate transformer fS corresponding to a program $S$ written in that language.

As most programming languages are defined recursively, we can expect such construction rules for the predicate transformer of the total program to be expressed in terms of predicate transformers associated with components. But, as we shall see in a moment, we must observe some restrictions, for if we allow ourselves too much freedom in the construction of predicate transformers we may arrive at predicate transformers f5 such that $f5(P)$ can no longer be interpreted as the weakest pre-condition corresponding to the post-condition P for a possible deterministic machine.

Our construction rules for predicate transformers fS must be such that, whatever fS we construct, it must have the following four basic properties

1) $P = Q$ implies $fS(P) = fS(Q)$ 2) $fS(F) = F$ 3） $fS(Pand Q) = fS(P)and fS(Q)$ 4) $fS(P \underline{or} Q) = fS(P) \underline{or} fS(Q)$

Predicate transformers enjoying those four properties we call "healthy".

Property 1 assures that we are justified in regarding the predicates as characterizing our true subject matter, viz. sets of states: it would be awkward if $fS(x > 0)$ would differ from $fS(0 < x)$ .

Property 2 is the so-called "Law of the Excluded Miracle" and does not need any further justification.

The justification for properties 3 and 4 becomes fairly obvious when we consider, for instance $P = (0 ≤ x ≤ 2)$ and $Q = (1 ≤ x ≤ 3)$ and require that each initial state satisfying fS(P) is mapped into a single state satisfying $P$ and similarly for $Q$ . Conversely it can be shown that each healthy predicate transformer fS can be interpreted as describing the net effect of a deterministic machine, whose actions are fully determined by the initial state.

From our 1st and 4th property we can derive a conclusion. Let $P ⇒ Q$ ; from this is follows that there exists a predicate $R$ such that we can write $Q = P \underline{or} R$ ; our 1st and 4th property then tell us that

f S (Q) = f S (P \underline {{o r}} R) = f S (P) \underline {{o r}} f S (R)

from which we deduce that

5) P ⇒ Q implies f S (P) ⇒ f S (Q).

The simplest predicate transformer enjoying the four basic properties is the identity transformation:

f S (P) = P;

the corresponding statement is well known to programmers, they usually call it "the empty statement".

But it is very hard to build up very powerful programs from empty statements alone, we need something more powerful. We really want to transform a given predicate $P$ into a possibly different predicate fS(P) .

One of the most basic operations that can be performed upon formal expressions is substitution, i.e. replacing all occurrences of a variable by (the same) "something else". If in the predicate P all occurrences of the variable "x" are replaced by (E), then we denote the result of this transformation by

\begin{array}{c}\mathbb {P} _ {\mathrm {E}} \rightarrow x.\end{array}

Now we can consider statements $S$ such that

f S (P) = P _ {E \rightarrow x} ;

this is a whole class of statements, they are given by three things

a) the identity of the variable $x$ to be replaced b) the fact that the substitution is the corresponding rule for predicate transformation c) the expression E which is to replace every occurrence of $\mathbf{x}$ in P.

The usual way to write such a statement is

\times := E

and such a statement is known under the name of an "assignment statement". We can formulate the

Axiom of Assignment. When the statement S is of the form $x := E$ , then its semantics are given by the predicate transformer fS that is such that for all P $fS(P) = P_{E \to x}$ .

The substitution process leads to predicate transformers that are healthy.

Although from a logical point of view unnecessary -we can take this predicate transformer to give by definition the semantics of what we call assignment statements-- it is wise to confront this axiomatic definition with our intuitive understanding of the assignment statement --if we have one!-- and it is comforting to discover that indeed it captures the assignment statement as we (may) know it, as the following examples -written in the format: ${fS(P)} S{P}-$ show:

\begin{array}{l} {a > 0 } x := 1 {a > 0 } \ \left{ \begin{array}{l} (1) < 2 \end{array} \right} x := 1 \left{x < 2 \right} \ {a > 0 and (x + 1) < 9 } x := x + 1 {a > 0 and x < 9 }. \ \end{array}

The above rules enable us to establish the semantics of the empty program and of the program consisting of a single assignment statement. In order to be able to compose more complicated predicate transformers, we observe that the functional composition of two healthy predicate transformers is again healthy. So this is a legitimate way of constructing a new one and we are lead to the

Axiom of Concatenation. Given two statements S1 and S2 with (healthy) predicate transformers fS1 and fS2 respectively, the predicate transformer fS, given for all P by

f S (P) = f S 1 (f S 2 (P))

is healthy and taken as the semantic definition of the statement 5 that we denote by S1; S2

Functional composition is associative and we are therefore justified in the use of the term "concatenation": it makes no difference if we parse "S1 ; S2 ; S3" either as "(S1 ; S2); S3" or as "S1 ;(S2 ; S3)".

Relating the axiomatic definition of the concatenation operator ";" to our intuitive understanding of a sequential computation, it just means that each execution of S1 (when completed) will immediately be followed by an execution of S2 and, conversely, that each execution of S2 has immediately been preceded by an execution of S1. The functional composition identifies the initial state of S2 with the final state of S1.

Looking for new programming language constructs implies looking for new ways of constructing predicate transformers, but all this, of course, subject to the restriction that the ensuing predicate transformer must be healthy. And a number of obvious suggestions must be rejected on that grounds, such as: $fS(P) = \underline{non} fS1(P)$

for that would violate the Law of the Excluded Miracle.

Also

f S (P) = f S 1 (P) \underline {{and}} f S 2 (P)

must be rejected as such a fS violates the basic property 4:

fS(P or Q) = fS1(P or Q) and fS2(P or Q) = {fS1(P) or fS1(Q)} and {fS2(P) or fS2(Q)} while

fS(P) or fS(Q) = {fS1(P) and fS2(P)} or {fS1(Q) and fS2(Q)}

and they are in general different, as the first of the two leads to the additional terms in the disjuction

{f S 1 (P) \underline {{and}} f S 2 (Q) } \underline {{or}} {f S 1 (Q) \underline {{and}} f S 2 (P) }.

Similarly, if we choose

f S (P) = f S 1 (P) \underline {{or}} f S 2 (P)

property 3 is violated, because

f S (P and Q) = f S 1 (P and Q) or f S 2 (P and Q) = {f S 1 (P) and f S 1 (Q) } or {f S 2 (P) and f S 2 (Q) }

while

f S (P) and f S (Q) = \left{f S 1 (P) or f S 2 (P) \right} and \left{f S 1 (Q) or f S 2 (Q) \right}

and here the second one leads to the additional terms in the disjunction

\left{f S 1 (P) \underline {{and}} f S 2 (Q) \right} \underline {{or}} \left{f S 1 (Q) \underline {{and}} f S 2 (P) \right}.

This leads to the suggestion that we look for fS1 and fS2 (in general $fS_{i}$ ) such that for any P and Q

i ≠ j implies f S _ {i} (P) \underline {{and}} f S _ {j} (Q) = F.

Doing it only for a pair leads to the

Axiom of Binary Selection. Given two statements S1 and S2 with healthy predicate transformers fS1 and fS2 respectively and a (computable) predicate B, the predicate transformer fS, given for all P by

f S (P) = {B and f S 1 (P)) } or (non B and f S 2 (P) }

is healthy and taken as the semantic definition of the statement S that we denote by if B then S1 else S2 fi

(This is readily extended to a choice between three, four or any explicitly enumerated set of mutually exclusive alternatives, leading to the so-called case-construction.)

For an arbitrary given sequence $fS_{i}$ we can not hope, that $i ≠ j$ implies $fS_{i}(P)$ and $fS_{j}(Q) = F$ for any $P$ and $Q$ , but we may hope to achieve this if we can generate the $fS_{i}$ by a recurrence relation. Before we embark upon such a project, however, we should derive a useful property of the predicate transformers we have been willing to construct thus far.

If two predicate transformers fS and $fS'$ satisfy the property that for all $P: fS(P) ⇒ fS'(P)$ , then we call "fS as strong as $fS''$ " and "fS' as weak as $fS''$ ".

(The predicate transformer given for all $P$ by $fS(P) = F$ is as strong as any other, the predicate transformer given by $fS(P) = T$ would be as weak as any other if it were admitted, but it is not, because it is not healthy: it violates the Law of the Excluded Miracle.)

We can now formulate and derive our

Theorem of Monotony. Whenever in a predicate transformer fS , formed by concatenation and/or selection, one of the constituent predicate transformers is replaced by one as weak (strong) as the original one, the resulting predicate transformer $fS'$ is as weak (strong) as fS .

Obviously we only need to show this for the elementary transformer constructions.

Concatenation, case 1:

Let S be: 51 ; S2

let S' be: 51'; 52

let S1' be as weak as S1, then

$fS(P) = fS1(Q)$ and $fS'(P) = fS1''(Q)$ , with $Q = fS2(P)$ ; as $fS1(Q) ⇒ fS1''(Q)$ for any $Q$ , $fS(P) ⇒ fS'(P)$ for any $P$ . QED.

Concatenation, case 2:

Let S be: 51 ; 52

let S8 be: S1 ; S2'

let $\mathbf{S2}^{\prime}$ be as weak as S2, then

$fS(P) = fS1(Q)$ and $fS'(P) = fS1(R)$ where $Q = fS2(P)$ and $R = fS2'(P)$ . Because for any $P$ , $Q ⇒ R$ , it follows from the healthiness of $fS1$ , that $fS(P) ⇒ fS'(P)$ . QED.

Binary selection, case 1:

Let S be: if B then S1 else S2 fi

let S! be: if B then S1' else S2 fi

let S1' be as weak as S1, then

\begin{array}{l} f S (P) = {B and f S 1 (P) } or {non B and f S 2 (P) } \ ⇒ {B \underline {{a n d}} f S 1 ^ {\prime} (P) } \underline {{o r}} {\underline {{n o n}} B \underline {{a n d}} f S 2 (P) } = f S ^ {\prime} (P). Q E D. \ \end{array}

Binary selection, case 2 can be left to the industrious reader.

Let us now consider a predicate transformer $G$ constructed by means of concatenation and selection, out of a number of healthy predicate transformers, among which $fH$ . (This predicate transformer may be used "more than once": then it corresponds to a program text in which the corresponding statement $H$ occurs more than once.) We wish to regard this predicate transformer as a function of $fH$ and indicate that by writing $G(fH)$ , i.e. $G$ derives by concatenation and/or selection with other, in this connection fixed predicate transformers, a new predicate transformer. We now consider the recurrence relation

f H _ {i} = G \left(f H _ {i - 1}\right) \tag {1}

which is a tractable thing in the sense that if $fH_{0}$ is as strong (weak) as $fH_{1}$ , it follows via mathematical induction from the Theorem of Monotony that $fH_{i}$ is as strong (weak) as $fH_{i+1}$ for all $i$ . We should like to start the recurrence relation with a constant transformer $fH_{0}$ , that is either as strong or as weak as any other. We can do this for a predicate transformer as strong as any other by choosing $fH_{0} = fSTOP$ , given by

f S T O P (P) = F \text {f o r a n y} P.

(The predicate transformer fSTOP satisfies all the requirements for healthiness.) And so we find ourselves considering the sequence of predicate transformers,

\begin{array}{l} \text {g i v e n b y} f H _ {0} = f S T O P \ \text {a n d f o r} i > 0: \mathrm {f H} _ {i} = G \left(\mathrm {f H} _ {i - 1}\right) \tag {2} \ \end{array}

with the property that

1) all $fH_{i}$ are healthy (by induction) 2) for $i ≤ j$ and any $P$ : $\mathsf{fH}{i}(\mathsf{P}) ⇒ \mathsf{fH}{j}(\mathsf{P})$ .

Because all $fH_{i}$ are healthy and any $P ⇒ T$ , we also know that for any $P$

f H _ {i} (P) ⇒ f H _ {i} (T).

We now recall that we were looking for $fS_{i}$ such that for any $P$ and $Q$ and $i ≠ j$ we would have $fS_{i}(P)$ and $fS_{j}(Q)$ .

f S _ {i} (P) \underline {{and}} f S _ {j} (Q) = F.

We can derive such predicate transformers from the $fH_{i}(P)$ . As each $fH_{i}(P)$ implies the next one in the sequence we could try for $i ≥ 0$

f S _ {i} (P) = f H _ {i} (P) \underline {{and}} \underline {{non}} f H _ {i - 1} (P)

i.e. the $fS_{i}(P)$ is the "incremental tolerance", but -both on account of the conjunction and on account of the negation- it is not obvious that such a construction is a healthy predicate transformer.

Therefore we proceed a little bit more carefully, first deriving a result that is independent of the post-condition. Each $fH_{i}(P)$ implies the next one in the sequence for any $P$ and therefore also for $P = T$ . We now

define

K _ {i} = f H _ {i} (T) \underline {{and}} \underline {{non}} f H _ {i - 1} (T) \text {f o r} i > 0 \tag {3}

and derive about the $K_{i}$ the following properties. (If we so desire, we can define $K_{0} = F$ .)

i ≠ j implies K _ {i} \underline {{and}} K _ {j} = F \tag {4}

This is proved by a reduction ad absurdum. Let $i < j$ and suppose $K_i$ and $K_j ≠ F$ ; then there exists a point $x$ in state space such that

K _ {i} (x) \underline {{and}} K _ {j} (x) = \underline {{\text {t r u e}}}

However, $K_{i}(x)$ implies $fH_{i}(T)(x)$ which implies $fH_{j-1}(T)(x)$ because $j-1 ≥ i$ which implies $K_{j}(x) = \text{false}$ and this is the contradiction we were after. In words: in each point in state space at most one $K_{i}$ is true.

f H _ {i} (T) = \left(\underline {{E}} j: 1 ≤ j ≤ i: K _ {j}\right) \tag {5}

From $fH_0(T) = f$ , we derive $K_1 = fH_1(T)$ so (5) holds for $i = 1$ . For the induction step we observe that

f H _ {i} (T) =

f H _ {i} (T) \underline {{and}} (\underline {{non}} f H _ {i - 1} (T) \underline {{or}} f H _ {i - 1} (T)) =

K _ {i} \underline {{or}} \left{f H _ {i} (T) and f H _ {i - 1} (T) \right} = K _ {i} \underline {{or}} f H _ {i - 1} (T).

The healthiness of $fH_{i}$ allows another conclusion.

f H _ {i} (P) \underline {{\underline {{\operatorname {o r}}}}} f H _ {i} (\underline {{\underline {{\operatorname {n o n}}}}} P) = f H _ {i} (P \underline {{\underline {{\operatorname {o r}}}}} \underline {{\underline {{\operatorname {n o n}}}}} P) = f H _ {i} (T) \tag {6}

f H _ {i} (P) \underline {{and}} f H _ {i} (\underline {{non}} P) = f H _ {i} (P \underline {{and}} \underline {{non}} P) = f H _ {i} (F) = F \tag {7}

Taking in (6) at both sides the conjunction with non $fH_{\pm}(P)$ we reach

f H _ {i} (non P) \text {a n d n o n} f H _ {i} (P) = f H _ {i} (T) \text {a n d n o n} f H _ {i} (P);

taking in the last two formulae at both sides the disjunction, we find

f H _ {i} (non P) = f H _ {i} (T) and non f H _ {i} (P)

and as $fH_{i}(\underline{non} P) ⇒ fH_{j}(\underline{non} P)$ for $j ≥ i$

we conclude for $j≥ i$

f H _ {i} (T) \underline {{and}} \underline {{non}} f H _ {i} (P) ⇒ f H _ {j} (T) \underline {{and}} \underline {{non}} f H _ {j} (P)

or

\underset {i} {\mathrm {K}} and \underset {i} {\mathrm {n o n}} f H _ {i} (P) ⇒ \underset {j} {\mathrm {n o n}} f H _ {j} (P) \tag {8}

Now, at last, we are ready to prove the theorem I have been driving at all the time, viz.

f H _ {i} (P) = \left(E j: 1 ≤ j ≤ i: K _ {j} \underline {{and}} f H _ {j} (P)\right) \tag {9}

In one direction the proof is easy. Consider a point $x$ in state space, such that $fH_{i}(P)(x) = \underline{false}$ ; on account of the monotony of the $fH_{i}$ we can conclude that then $j ≤ i$ implies $fH_{j}(P)(x) = \underline{false}$ , therefore the right-hand side is false as well.

Consider now a point $x$ , such that $fH_{i}(P)(x) = \underline{true}$ . Then $fH_{i}(T)(x) = \underline{true}$ and according to (4) and (5) there is exactly one value $m$ in the range $1 ≤ m ≤ i$ such that $K_{m}(x) = \underline{true}$ . Furthermore, on account of the monotony of the $fH_{i}$ , there is a unique value $k$ in the range $1 ≤ k ≤ i$ such that

j ≥ k implies f H _ {j} (P) (x) = \underline {{\text {t r u e}}}

j < k implies f H _ {j} (P) (x) = \underline {{\text {f a l s e}}}

Now relation (8) excludes the case $m < k$ , for then we would have

K _ {m} (x) \underline {{and}} \underline {{non}} f H _ {m} (P) (x) = \underline {{\text {t r u e}}}

implying (as $i ≥ m$ ) non $fH_{i}(P)(x)$ , contradicting our assumption. Therefore $m ≥ k$ , implying $K_{m}$ and $fH_{m}(P)(x) = \underline{true}$ , which leads to the conclusion that the right-hand side is true as well. And thus relation (9) has been proved.

And now most of the hairy work has been done. Because $fH_{i}$ is a healthy predicate transformer, $fS_{i}$ , given by

f S _ {i} (P) = K _ {i} and f H _ {i} (P) \tag {10}

is healthy as well. (Because $K_{i}$ is a predicate independent of $P$ , it is the predicate transformer associated with

i then H _ {i} \text {e l s e} \text {S T O P} f i.)

But on account of (4) we now have: $i ≠ j$ implies $fS_{i}(P)$ and $fS_{j}(Q) = F$ and this false conjunction was exactly what we were looking for! With the aid of our infinite sequence of $fS_{i}$ we can now form two new healthy predicate transformers, firstly

f H (P) = (\underline {{A}} i: 1 ≤ i: f S _ {i} (P)) ,

but that one, although healthy, is not interesting because on account of (11) it is identically F, and secondly

f H (P) = \left(E i: 1 ≤ i: f S _ {i} (P)\right). \tag {12}

this one is not identically $F$ and we call it a predicate transformer

"composed by recursion". In formula (12), for each point $x$ in state space, such that $fH(P)(x) = \text{true}$ , the existential quantifier singles out a unique value of $i$ .

Alternatively we may write

\begin{array}{l} f H (P) = \left\lfloor E, j: 1 ≤ j: \left(E i: 1 ≤ i ≤ j: f S _ {j} (P)\right)\right) \ = (E j: 1 ≤ j: f H _ {j} (P)) . \tag {13} \ \end{array}

As formula (9) is equivalent to

f H _ {i} (P) = (\underline {{E}} j: 1 ≤ j ≤ i; f S _ {i} (P))

we see, on account of (11) that, as we guessed

f S _ {i} (P) = f H _ {i} (P) \underline {{\text {a n d n o n}}} f H _ {i - 1} (P)

but in the mean time its healthyness has been established.

I apologize most sincerely for the last few pages of formal labour, which took me a few days to write down, while a greater expert in the propositional calculus probably could have done it much more efficiently. It is by now most urgent that we relate the above to our intuitive understanding of the recursive procedure: then all our formulae become quite obvious (and the painfulness of my formal proofs becomes frustrating!)

First a remark about the Theorem of Monotony: it just states that if we replace a component of a structure by a more powerful one, the modified structure will be at least as powerful as the original one. (Consider, for instance, an implementation of a programming language that leads to program abortion when integer overflow occurs, i.e. when an integer value outside the range $[-M, +M]$ is generated. When we modify the machine by increasing $M$ , all computations that were originally feasible, remain so, but possibly we can do more.)

Now for the recursion. All we have been talking about is a recursive procedure (without local variables and without parameters) that could have been declared by a text of the form

proc H: .H. .H. .H. .corp

i.e. a procedure $H$ that may call itself from various places in its body.

Mentally we are considering an infinite sequence of procedures $H_{i}$ with

proc H: STOP corp

proc H: ...H i-1 ...H i-1 ...H i-1 ... corp

Our rules

f H _ {0} = f S T O P \text {a n d f o r} i > 0: f H _ {i} = G (f H _ {i - 1})

are such that the proposition transformer $fH_{i}$ corresponds to our intuitive understanding of the call of procedure $H_{i}$ . In terms of the procedure $H_{i}$ , $fH_{i}$ describes what a call of the procedure $H$ can do under the additional constraint that the dynamic recursion depth will not exceed i. In particular, $fH_{i}(T)$ characterizes the initial states such that the procedure call will terminate with a dynamic recursion depth not exceeding i, while $K_{i}$ characterizes those initial states such that a call of $H$ will give rise to a maximum recursion depth exactly = i. This intuitive interpretation makes our earlier formulae quite obvious, $fH(T)$ is the weakest precondition that the call will lead to a terminating computation.

The Theorem of Monotony was proved for predicate transformers formed by concatenation and/or selection. If in the body of $H$ one of the predicate transformers fS is replaced by $fS'$ , as weak(strong) as fS , then $G'(fH)$ will be as weak (strong) as $G(fH)$ , giving rise to an $fH'$ as weak (strong) as $fH_i$ ; as a result the Theorem of Monotony holds also for predicate transformers constructed via recursion.

Our axiomatic definition of the semantics of a recursive procedure

f H _ {0} = f S T O P

and for $i > 0$ : $fH_{i} = G(fH_{i-1})$

and $\mathsf{fH}(\mathsf{P}) = (\underline{\mathsf{E}}\mathsf{i};\mathsf{i}≥ 1:\mathsf{fH}_{\underline{\mathbf{i}}}(\mathsf{P}))$ (14)

is nice and compact, in actual practice it has one tremendous disadvantage: for all but the simplest bodies, it is impossible to use it directly. $fH_{1}(P)$ becomes a line, $fH_{2}(P)$ becomes a page, etc. and this circumstance makes it often very unattractive to use it directly. We cannot blame our axiomatic definition of the recursive procedure for this unattractive state of affairs: recursion is such a powerful technique for the construction of new predicate transformers, that we can hardly expect a recursive procedure "chosen at random" to turn out to be a mathematically manageable object. So we had better

discover which recursive procedures can be managed intellectually and how. This is nothing more nor less than asking for useful theorems about the semantics of recursive procedures.

Du intuitive understanding of the $K_{i}$ -i.e. the initial states, such that a call will lead to a maximum recursion depth = i- suggests a theorem: if $i > 1$ , it can only achieve its maximum recursion depth by primarily generating at least one call that gives rise to a maximum recursion depth = i-1. Therefore we conjecture

f o r 1 ≤ i ≤ j: K _ {i} = F implies K _ {j} = F. \tag {15}

On account of the assumption

K _ {i} = f H _ {i} (T) \underline {{and}} \underline {{non}} f H _ {i - 1} (T) = F

we have

T = \underline {{non}} K _ {i} = \left{\underline {{non}} f H _ {i} (T) \underline {{or}} f H _ {i - 1} (T) \right} = \left{f H _ {i} (T) ⇒ f H _ {i - 1} (T) \right};

on the other hand we have $fH_{i-1}(T) ⇒ fH_{i}(T)$ and therefore $fH_{i}(T) = fH_{i-1}(T)$ . We would like to conclude

f H _ {i} = f H _ {i - 1} \tag {16}

or, more explicitly,

f H _ {i} (P) = f H _ {i - 1} (P) \text {f o r a n y P}. \tag {17}

The latter relation is true, if it is true for any point $x$ in state space. If $fH_{i}(T)(x) = \underline{false}$ , so are $fH_{i}(P)(x)$ and $fH_{i-1}(P)(x)$ , and we are left with the points $x$ , such that $fH_{i}(T)(x) = \underline{true}$ .

Because $fH_{i}$ is healthy we have for any $P$

\begin{array}{l} f H _ {i} (P) (x) \underline {{a r}} f H _ {i} (\underline {{n o n}} P) (x) = f H _ {i} (T) (x) = \underline {{t r u e}} \ f H _ {i} (P) (x) \underline {{and}} f H _ {i} (\underline {{non}} P) (x) = f H _ {i} (F) (x) = \underline {{\text {f a l s e}}} , \ \end{array}

from which it follows that

f H _ {i} (P) (x) = \underline {{non}} f H _ {i} (\underline {{non}} P) (x)

and similarly for the same arbitrary P and the same point x

f H _ {i - 1} (P) (x) = \underline {{non}} f H _ {i - 1} (\underline {{non}} P) (x).

If $fH_{i-1}(P)(x) = \underline{true}$ , we see that $fH_{i}(P)(x) = \underline{true}$ , because $fH_{i-1}(P) \Leftrightarrow fH_{i}(P)$ ;

if $fH_{i-1}(P)(x) = \text{false}$ , $fH_{i-1}(non P)(x) = \text{true}$ and so is $fH_i(non P)(x)$ , because $fH_{i-1}(non P) ⇒ fH_i(non P)$ , and thus $fH_i(P)(x) = \text{false}$ as well.

Therefore (17) and (16) as well have been established. But on account of the recurrence relation for the $fH_{i}$

f H _ {i} = f H _ {i - 1} implies f H _ {i + 1} = f H _ {i}

and via mathematical induction $fH_{j} = fH_{j-1}$ for any $j ≥ i$ , in particular $fH_{j}(T) = fH_{j-1}(T)$ and (15) has been established. (Whether in the sequel we can make good use of (15) is still an open question; for the time being we can regard its proof as an exercise.)

Now we are going to prove the Fundamental Invariance Theorem for Recursive Procedures.

Consider a text, xalled H", of the form

H"：. .H' . .H' . .H' . .

to which corresponds a predicate transformer $fH"$ , such that for two specific predicates $Q$ and $R$ , the assumption $Q ⇒ fH'(R)$ is a sufficient assumption about $fH'$ to prove $Q ⇒ fH''(R)$ .

In that case, the recursive procedure $H$ given by

proc H: .H. .H. .H. .comp

(where we get this text by removing the dashes and enclosing the resulting text between the brackets proc and corp) enjoys the property that

Q and f H (T) ⇒ f H (R). \tag {18}

(The tentatice conclusion $Q ⇒ fH(R)$ is wrong, as is shown by the counter-example proc H: H corp.)

We show this by showing that then $\mathbb{Q}$ must be such that for all $i$

Q \underline {{and}} f H _ {i} (T) ⇒ f H _ {i} (R) \tag {19}

and from (19), (18) follows trivially.

Relation (19) holds for $i = 0$ , mathematical induction is the tool and we propose to demonstrate that if (19) holds for $i = j-1$ , it will hold for $i = j$ as well.

Let us consider first, for the sake of simplicity, the case that the text H22 contains a single reference to H'. In the evaluation of fH''(R), let P1 be the argument supplied to fH'; with

P 2 = f H (P 1)

we can write $fH''(R) = E(P2)$ .

We can regard E as a predicate transformer operating on its argument P2, but considered as predicate transformer it is not necessarily healthy: it may violate the Law of the Excluded Miracle. It enjoys, however, the other three properties:

\begin{array}{l} P = Q implies E (P) = E (Q) \ E (P and Q) = E (P) and E (Q) \ E (P \underline {{o r}} Q) = E (P) \underline {{o r}} E (Q) \ \end{array}

and therefore also the fifth:

P ⇒ Q implies E (P) ⇒ E (Q).

The statement that the conditions A and B are such that the assumption $A ⇒ fH'(R)$ is a sufficient assumption about $fH'$ , such that we can prove $B ⇒ fH''(R)$ is, in terms of P1 and E, equivalent to the two implications

\begin{array}{l} R ⇒ P 1 \ B ⇒ E (A) \ \end{array}

In our particular case, it has been given, that this holds for $A = Q$ and $B = Q$ , i.e. we know

Q ⇒ E (Q).

When we are now able to show that

r H _ {j} (T) ⇒ E \left(r H _ {j - 1} (T)\right) \tag {20}

then $\mathbb{Q}$ and $fH_{j}(T) = E(Q$ and $fH_{j - 1}(T))$

and as a result $\mathsf{Q}$ and $fH_{j-1}(T) ⇒ fH'(R)$ is then a sufficient assumption about $fH'$ to conclude that $\mathsf{Q}$ and $fH_j(T) ⇒ fH''(R)$ . As $fH_j$ depends on $fH_{j-1}$ as $H''$ on $H'$ , this would conclude the induction step and (18) would have been proved.

We have two holes to fill: we have to show (20) and we have to extend the line of reasoning to texts of H2, containing more than one reference to H'. Let us first concentrate on (20).

We have defined $fH_{j} = G(fH_{j-1})$ , but because for any $P$ , we have $fH_{j-1}(P) ⇒ fH_{j-1}(T)$ , an identical definition would have been

f H _ {j} = G \left(f H _ {j - 1} (T) \underline {{and}} f H _ {j - 1}\right)

i.e. each predicate formed by applying $fH_{j-1}$ is replaced by its conjunction with $fH_{j-1}(T)$ . And therefore, instead of

\begin{array}{l} P 1 = f S (T) \text {(i . e .} P 1 \text {i s t h e a r g u m e n t s u p p l i e d t o f H ^ {\prime}} \text {i n t h e e v a l u -} \ P 2 = f H _ {j - 1} (P 1) \text {a t i o n o f} f H ^ {\prime \prime} (T). \ f H _ {j} (T) = E (P 2) \ \end{array}

we could have written equally well

P 1 = f S (T)

P 2 = f H _ {j - 1} (P 1)

f H _ {j} (T) = E (P 2 \underline {{a n d}} f H _ {j - 1} (T)).

But ${P2and fH_{j-1}(T)} ⇒ fH_{j-1}(T)$ and therefore, because the transformer E enjoys the fifth property, we are entitled to conclude

f H _ {j} (T) ⇒ E \left(f H _ {j - 1} (T)\right) i. e. r e l a t i o n (2 0).

To fill the second hole, viz. that in the text called $H^{\prime \prime}$ more than one reference to $H^{\prime}$ may occur, is easier. Working backwards in the evaluation of $fH''(R)$ means that we first encounter the innermost evaluation(s) of $fH'$ , whose argument does not contain $fH'$ . For those proposition transformers we apply our previous argument, showing that for them the weaker assumption $Q$ and $fH_{j-1}(T) = fH'(R)$ is sufficient. Then its value is replaced by $Q$ and we start afresh. In this way the sufficiency of the weaker assumption about $fH'$ can be established for all occurrences of $fH'$ only a finite number! in turn.

For the recursive routines of the particularly simple form

proc H: if B then S1; H else fi

we can ask ourselves what must be known about B and S1, when we take for R the special form Q and non B. Then

fH"(Q and non B) = {B and fS1(fH'(Q and non B))} or{Q and non B}.

In order to be able to conclude $\mathbb{Q} ⇒ fH''(\mathbb{Q}$ and non B) on account of $\mathbb{Q} ⇒ fH'(\mathbb{Q}$ and non B), the necessary and sufficient assumption about f51 is

{Q \underline {{a n d}} B } ⇒ f 5 1 (Q). \tag {21}

Procedures of this simple form are such useful elements that it is generally felt justified to introduce a specific notation for it, in which the recursive procedure remains anonymous: it should contain as "parameters" the B and the S1 and we usually write

while \mathrm {B} \underline {{do}} \mathrm {S 1} \underline {{od}} \tag {22}

When the statement 5 is of the form (22), we have now proved that

{Q and B } ⇒ f S 1 (Q) implies {Q and f S (T) ⇒ f S (Q and non B).

This is called "The Fundamental Invariance Theorem for Repetition".

The extension to a set of recursive procedures should not present any essential new difficulty. Given the texts

\operatorname {p r a c} H 1: \dots \dots . H 1 \dots \dots . H 2 \dots \dots . H 1 \dots \dots . H 2 \dots \dots . c o r p

\text {p r o c} H 2: \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots

the combined semantics are given by

f H _ {0} = f S T O P and f H _ {2 0} = f S T O P, \text {w h i l e f o r} \times \times \times i > 0:

f H _ {i} = G 1 \left(f H _ {i - 1}, f H _ {2 i - 1}\right) and f H _ {2 i} = G 2 \left(f H _ {i - 1}, f H _ {2 i - 1}\right). A l l

our arguments can then be repeated, only twice as complicated. The Theorem of Invariance for the Recursive procedures is then as follows:

When there exist specific predicates Q1, R1, Q2 and R2, such that $\mathsf{Q1} ⇒ \mathsf{fH1}'(\mathsf{R1})$ and $\mathsf{Q2} ⇒ \mathsf{fH2}'(\mathsf{R2})$ are sufficient assumptions about $\mathsf{fH1}'$ and $\mathsf{fH2}'$ to prove $\mathsf{Q1} ⇒ \mathsf{fH1}''(\mathsf{R1})$ and $\mathsf{Q2} ⇒ \mathsf{fH2}''(\mathsf{R2})$ , then we are allowed to conclude that ${\mathsf{Q1} and \mathsf{fH1}(\mathsf{T})} ⇒ \mathsf{fH1}(\mathsf{R1})$ and ${\mathsf{Q2} and \mathsf{fH2}(\mathsf{T})} ⇒ \mathsf{fH2}(\mathsf{R2})$ .

This extension we gladly leave to the over-industrious reader. Among other things it implies that our results concerning bodies composed via concatenation and selection carries over to bodies also composed via repetition.