Predicative Semantics of Loops

Theodore S. Norvell Faculty of Engineering Memorial University of Newfoundland St. John’s NF A1B 3X5 Canada theo@engr.mun.ca www.engr.mun.ca/∼theo/

Abstract

A predicative semantics is a mapping of programs to predicates. These predicates characterize sets of acceptable observations. The presence of time in the observations makes the obvious weakest fixed-point semantics of iterative constructs unacceptable. This paper proposes an alternative. We will see that this alternative semantics is monotone and implementable (feasible). Finally a programming theorem for iterative constructs is proposed, proved, and demonstrated. A novel aspect of this theorem is that it is not based on invariants.

Keywords

Predicative semantics, fixedpoint semantics, recursion, loops, refinement calculi.

0 FORMALIZATION

0.0 Specifications and refinement

Define xnat as the set of all natural numbers (nat) joined with an additional object ∞. We will suppose the following properties of ∞: it is larger than any natural number; ∞ + i = ∞ − i = ∞, for all natural numbers i; and ∞ − ∞ = 0.

I will use a ‘batch’ model for specifications borrowed, in most respects, from (Hehner 1993). Let Σ be any type (a nonempty set). I will call the members of Σ ‘states’, which is suggestive of imperative programming, but the actual contents of Σ will only be relevant in the examples. Specifications are functions of type

Σ → xnat → Σ → xnat → bool .

\begin{matrix}c \\ ◯ \end{matrix}IFIP 1996. Published by Chapman & Hall

For example, (λσ : Σ, τ : xnat, σ′ : Σ, τ′ : xnat · τ′ ≥ τ ∧ σ′ = σ) is a specification.

The variables σ, σ′ : Σ and τ, τ′ : xnat will be used in writing specifications follows: for any expression E, I write ⟨E⟩ for the abstraction of E with respect to these variables. For example, ⟨τ′ ≥ τ ∧ σ′ = σ⟩ is an abbreviation for the specification (λσ : Σ, τ : xnat, σ′ : Σ, τ′ : xnat · τ′ ≥ τ ∧ σ′ = σ). The variables are used as follows: σ and σ′ represent the initial and final states while τ, and τ′ represent the initial and final times. Thus the specification ⟨τ′ ≥ τ ∧ σ′ = σ⟩ specifies that the final time is no less than the initial time and the final state is the same as the initial state.

All boolean operators (⊤, ⊥, ∧, ∨, ¬, ≡, ≢, ⇒, ⇐)lift to the specification level; for example, if P and Q are specifications, P ⇒ Q is the specification

⟨P.σ.τ.σ′.τ′ ⇒ Q.σ.τ.σ′.τ′⟩ .

I use the symbols ⊤ and ⊥ as the boolean constants true and false. Refinement is defined as

(P ⊑ Q) ≡ (∀σ, τ, σ′, τ′ · P.σ.τ.σ′.τ′ ⇐ Q.σ.τ.σ′.τ′) .

Equality of specifications is extensional

(P = Q) ≡ (P ⊑ Q) ∧ (Q ⊑ P) .

0.1 Discussion

This formalization applies equally to imperative programming and to functional programming. In imperative programming Σ is a set of states and in functional programming Σ is a set of values.

The use of predicates as specifications follows (Hehner 1984), (Hoare 1985), (Hehner 1993), (Hoare 1994), and (v. Karger and Hoare 1994).

The treatment of time is based on (Hehner 1993) and (Hehner 1994). It is necessary to include the infinity value in the time domain in order to deal with infinite loops. Because a statement may sequentially follow an infinite loop, xnat is used both for the initial and final states. Time is considered a quantity orthogonal to state; this simplifies the writing of specifications, but as we will see, it complicates the theory somewhat. Using the algebra of xnat requires some care, as some laws of nat do not hold unconditionally.

The use of predicates is reminiscent of the Z method (Spivey 1989), but the notion of refinement in Z is quite different and much harder to work with. More relevant are refinement calculi based on predicate transformers (Back and von Wright 1990) and (Morgan 1990). Binary predicates ordered

Formalization 3

by refinement are order isomorphic to the universally conjunctive predicate transformers (Holt 1991).

0.2 Bounds and classes of specifications

A specification P is said to be progressive if

⟨τ′ ≥ τ⟩ ⊑ P , and to be implementable if

(∀σ, τ · (∃σ′, τ′ · P.σ.τ.σ′.τ′)) . The term feasible is also used in the literature —e.g. (Morgan 1990)— for this property of specifications.

A specification P is called a condition if it does not depend on its latter two arguments. An expression B is called a condition, if ⟨B⟩ is a condition.

A function g of type Σ → xnat → xnat is called a bound of a specification R if

⟨τ′ ≤ τ + g.σ.τ⟩ ⊑ R . A specification R is said to be strongly bounded if it has a natural bound:

(∃g : Σ → xnat → nat · ⟨τ′ ≤ τ + g.σ.τ⟩ ⊑ R) . Such a specification guarantees termination after a finite amount of time.

For a given specification R, we can consider the set of all bounds:

{g : Σ → xnat → xnat | ⟨τ′ ≤ τ + g.σ.τ⟩ ⊑ R} . This set may be ordered pointwise: (g ≤ h) ≡ (∀σ, τ · g.σ.τ ≤ h.σ.τ). For an implementable and progressive R, this set will have a minimum member m_{R} characterized by

m_{R}.σ.τ = (max σ′, τ′ | R.σ.τ.σ′.τ′ · τ′ − τ) . Henceforth the subscript on m will be omitted if it is the letter R. The key property of m is that a computation, starting in state σ at time τ, could take as long as m.σ.τ:

(∀σ, τ · (∃σ′, τ′ · R.σ.τ.σ′.τ′ ∧ τ′ = m.σ.τ + τ))  .  (0)

If m does not depend on its second argument, we say that R is time-insensitively bounded.

Specifications that make no demands about the final state, when the initial time is ∞ are called reasonable. We want to allow reasonable specifications to be progressive. Define

Z = ⟨τ = ∞ = τ′⟩

a specification R is said to be reasonable iff

R = Z ∨ R .

0.3 Semantics

The semantics of programming constructs is given by defining the simple constructs as specifications and compound constructs as functions from (one or more) specifications to specifications. A program can then be defined as a specification built using only the programing constructs.

Some straight-line programming constructs are defined by:

skip = ⟨σ′ = σ ∧ τ′ = τ⟩

tick = ⟨σ′ = σ ∧ τ′ = τ + 1⟩

P; Q = ⟨∃σ̂, τ̂ · P.σ.τ.σ̂.τ̂ ∧ Q.σ̂.τ̂.σ′.τ′⟩

if B then P else Q = (⟨B⟩ ∧ P) ∨ (¬ ⟨B⟩ ∧ Q) .

In the if-statement, it will be assumed that B is a condition. The tick construct is not really a programming construct, but is useful in defining the while loop.

It should be noted that these definitions hold for P and Q being any specifications, not only those formed from programming constructs.

For condition B and specification P define a function w_{B,P} by

w_{B,P} .Q = if B then(P; tick; Q) else skip (1)

Let W_{B,P} stand for while B do P. Henceforth the subscripts on w and W will be omitted where they are the letters B, P. As in (Norvell 1993) and (Norvell 1994) I define the while loop by three axioms

Progression: ⟨τ′ ≥ τ⟩ ⊑ W Post-fixed-point: w.W ⊑ W Induction: (⟨τ′ ≥ τ⟩ ⊑ Q) ∧ (w.Q ⊑ Q) ⇒ (W ⊑ Q) , for all Q.

This definition of the while-loop is called the weakest progressive post-fixed-point definition. The lattice of progressive specifications is complete and thus we may apply the Knaster-Tarski (Tarski 1955) theorem to tell us that W is well defined, that it is a fixed-point:

w.W = W  ,  (2)

and that it is the weakest of the fixed-points:

(⟨τ′ ≥ τ⟩ ⊑ Q) ∧ (w.Q = Q) ⇒ (W ⊑ Q) , for all Q.

As an alternative, but equivalent, definition, it is possible to replace the postfixed-point and the induction axioms with these last two formula.

0.4 Discussion

It should be noted that the only action among the statements presented so far that is considered to take any time at all is the backward jump of the while loop. The “time” calculated for programs under this model is not proportional to the actual time that an implementation would take. However it does give the correct order for time complexities if all primitive operations are O(1). This is not the only alternative, it is possible to use a semantics that keeps more careful track of time. Further discussion can be found in (Hehner 1994).

The importance of the progression axiom and the corresponding antecedent in the post-fixed-point axiom is that simply taking the weakest fixed-point of the equation

W = if B then(P; tick; W) else skip

would not result in a construct that is closed under progressiveness. For example, with the current definition we have

⟨τ′ = ∞⟩ ⊑ while ⊤ do skip .

However, with the weakest fixed-point semantics, such a loop would not even be progressive. The difference between these approaches is manifested for (potentially) infinite loops, and one may wonder if these are worth the trouble. With the limited notion of observations used in this paper (initial and final states only), the point is arguable. However, for communicating programs, which can be modeled using a slightly richer notion of observations, (potentially) infinite loops are of great importance.

It might seem that it would be easier to simply work within the lattice of progressive specifications or even the semilattice of progressive and implementable specifications. From a semantic point of view, this may be true. But from the point of view of specifying, it is simplest if specifications are simply predicates with no restrictions. Also the progressive specifications are not closed under negation, so this would restrict the ways in which specifications are composed.

1 ESSENTIAL THEOREMS

Compound programming constructs are generally monotonic with respect to refinement and preserve implementability and progressiveness. Both these properties hold for the while loop as defined above.

We start by showing monotonicity.

Theorem 0 For any condition B, and specifications P and Q, if P ⊑ Q, then

while B do P ⊑ while B do Q .

Monotonicity is not hard to prove and illustrates all three axioms at work.

W_{B,P} ⊑ W_{B,Q}
⇐  “ Induction axiom with Q instantiated by W_{B,Q}. ”
(⟨τ′ ≥ τ⟩ ⊑ W_{B,Q}) ∧ (w_{B,P} .W_{B,Q} ⊑ W_{B,Q})
≡  “ Progression axiom (τ′ ≥ τ ⊑ W_{B,Q}) and prop. calc. ”
w_{B,P} .W_{B,Q} ⊑ W_{B,Q}
⇐  “ Post-fixpoint axiom (w_{B,Q}.W_{B,Q} ⊑ W_{B,Q}) and

transitivity of ⊑ .” w_{B,P} .W_{B,Q} ⊑ w_{B,Q}.W_{B,Q}

≡  “ Definition of w (1). ”
if B then(P; tick; W_{B,Q}) ⊑ if B then(Q; tick; W_{B,Q})
⇐  “ Monotonicity of if and ; . ”
P ⊑ Q

Next we show that progressiveness and implementability are jointly preserved.

Theorem 1 For any condition B, and specification P, if P is progressive and P is implementable,

then while B do P is progressive and implementable.

The proof is given in appendix 0. This proof also shows that progressiveness is preserved on its own.

2 A PROGRAMMING THEOREM

Among the most useful of the theorems in a refinement calculus are those of the form “if ... then R ⊑ c.P_{0}.P_{1}. · · · .P_{n−1}” where c is a program constructor. For example, in the theory used in this paper R ⊑ if B then(⟨B⟩ ⇒ R) else(¬ ⟨B⟩ ⇒ R) is a useful theorem.

In order to derive programs involving while-loops, we would like to have theorems that conclude with R ⊑ while B do P. In most refinement calculi, such theorems are usually based on invariants. In (Hehner 1979) the idea of “recursive refinement” instead of invariants is suggested. In this section we propose a theorem based on recursive refinement.

A specification R is said to be recursively refined if

R ⊑ if B then(P; tick; R) else skip  .  (3)

It is often true that when (3) is true, it is also true that

R ⊑ while B do P  .  (4)

So the question arises of under what conditions (3) implies (4). The next theorem presents one possible set of conditions.

Theorem 2 For any condition B, and specifications P and R, if

P is progressive; R is implementable, strongly bounded, time insensitively bounded, and reasonable; and R is recursively refined:

R ⊑ if B then(P; tick; R) else skip (5)

then R ⊑ while B do P.

The proof of this is by induction and is given in appendix 1.

8 Predicative Semantics of Loops

2.0 Discussion

It is informative to look at why additional conditions are required beyond (5) are required.

Here is a simple counter example showing that (5) does not imply R ⊑ while B do P. Take P to be skip and B to be ⊤. We have

⊥ ⊑ if ⊤ then(skip; tick; ⊥) else skip . But it is certainly not the case that

⊥ ⊑ while ⊤ do skip as this would mean that the while loop is unimplementable. Yet we know from the Theorem 1 and the fact that skip is progressive and implementable that the while loop is also implementable.

In (Hehner 1993) it is suggested that recursive refinement is only a valid programming method for implementable specifications. What if we restrict R to be an implementable specification? Again we are disappointed. Consider the following ‘monster’. It is true that

⟨σ′ = 0⟩ ⊑ if ⊤ then(skip; tick; ⟨σ′ = 0⟩) else skip and that

⟨σ′ = 1⟩ ⊑ if ⊤ then(skip; tick; ⟨σ′ = 1⟩) else skip . Yet, if it were true both that

⟨σ′ = 0⟩ ⊑ while ⊤ do skip and

⟨σ′ = 1⟩ ⊑ while ⊤ do skip , we would have to conclude that

⊥ ⊑ ⟨σ′ = 0 ∧ σ′ = 1⟩ ⊑ while ⊤ do skip . Again this contradicts the implementability of while loops.

The problem illustrated in this example occurs basically because the loop is infinite. By adding the requirement of strong bounding, infinite loops are eliminated. The requirements that P be progressive and that the minimum bound is not sensitive to the starting time ensure that the induction goes through.

The requirement that R be reasonable is the most troubling, as it requires one to write specifications in a way that one otherwise would not. This requirement is necessary because the induction does not work when the initial time is ∞. One solution to this problem is to use the ordinal numbers as the time domain rather than xnat. The problem with this ‘solution’ is that the proof of Theorem 1 no longer goes through. Other solutions might involve changing the definitions of refinement or of the programming constructs, or removing the orthogonality of time and state (i.e. treat specifications as binary relations on (Σ × nat) ∪ {∞}). Such changes are rather undesirable as the simplicity of these definitions is an important attribute of the predicative programming approach.

A somewhat similar theorem appears in (Sekerinski 1993). However the definition of the programming connectives (e.g. sequential composition) is different and the theorem can only be used to show that a specification is a fixed-point. From a programming point of view, this is less satisfactory as one is not so much interested in whether a while loop equals a given specification, but rather whether it implements the specification at hand.

3 A PROGRAMMING EXAMPLE

In imperative programming, Σ consists of states, which may be considered functions from program variable names to values. This function can be extended to expressions. For any program variable name x, and expression E the assignment statement can be defined as

x := E = ⟨σ′.x = σ.E ∧ (∀y ∈ dom .σ | x ≠ y · σ′.y = σ.y) ∧ τ′ = τ⟩

where dom .σ is the set of variable names.

In this section, for any program variable name such as x, I will use the convention of writing x in specifications rather than σ.x and of writing x′ rather than σ′.x. With this convention the assignment is simply

x := E = ⟨x′ = E ∧ y′ = y ∧ ⋯ ∧ τ′ = τ⟩ .

where the ⋯ depends on what variables are in the domain of the states. We have the following useful substitution law

x := E; ⟨P ⟩ = ⟨P_{E}^{x}⟩  ,  (6)

10 Predicative Semantics of Loops

provided P is written with the convention. There is an analogous law for the time variable

tick; ⟨P ⟩ = ⟨P_{τ+1}^{τ}⟩ . (7) I will solve a trivial programming example in two ways, illustrating the

relationship of recursive refinement to the invariant method. The problem is that of finding the product of the elements in an array A of size N. The specification is

S = ⟨s′ = (Πi ∈ {0, ..N} · A.i) ∧ τ′ ≤ τ + N⟩ ∨ Z I will write {i, ..k} for the set of all integers j, such that i ≤ j < k and {i, .., k} for the set of all integers j, such that i ≤ j ≤ k. The “∨Z” part of the specification is required to satisfy the condition of ‘reasonableness’. The predicate Z was defined in Section 0.2.

3.0 A solution that does not use an invariant

We can refine S using the substitution law (supposing x is of type {0, .., N}):

S ⊑ s, x := 1, 0; R0 , where

R0 = ⟨s′ = s × (Πi ∈ {x, ..N} · A.i) ∧ τ′ ≤ τ + N − x⟩ ∨ Z . This is refined by cases

R0 ⊑ if x < N then(⟨x < N⟩ ⇒ R0) else skip . Now we can refine the remaining specification:

⟨x < N⟩ ⇒ R0

⊑  “ Splitting the product. ”

\left⟨{s′ = s × A.x × (Πi ∈ \{x + 1, ..N\} · A.i) \atop ∧ τ′ ≤ τ + 1 + N − (x + 1)}\right⟩ ∨ Z

=  “ Substitution (6) and (7). ”

s, x := s × A.x, x + 1; tick; R0 .

A programming example 11

Putting these results together (by the monotonicity of if) we get

R0 ⊑ if x < N then(s, x := s × A.x, x + 1; tick; R0) else skip . Since all the conditions of Theorem 2 are met, we may conclude

R0 ⊑ while x < N do s, x := s × A.x, x + 1 .

3.1 A solution using an invariant

It should be noted that nowhere in the above development, nor even in the thinking behind it, did the formula

s = (Πi ∈ {0, ..x} · A.i) appear. This is the invariant that would be used if the invariant method were used. Recursive refinement does not exclude the use of invariants and, in the development of many loops, it is the simplest method.

Using substitution, and some simplification, we could also refine S by S ⊑ s, x := 1, 0; R1

where R1 is

⟨s = (Πi ∈ {0, ..x} · A.i) ⇒ s′ = (Πi ∈ {0, ..N} · A.i) ∧ τ′ ≤ τ + N − x⟩ ∨ Z. As with R0 we can derive that

R1 ⊑ if x < N then(s, x := s × A.x, x + 1; tick; R1) else skip , although the reasoning is a little more involved. Again the Theorem 2 can be applied.

We can recognize that the R1 has the form of a precondition s = (Πi ∈ {0, ..x}·A.i) and a postrelation s′ = (Πi ∈ {0, ..N}·A.i)∧τ′ ≤ τ +N −x, and that the precondition is a loop invariant, but there is no real need to think in these terms.

3.2 Views and refinement by parts

It may seem unpleasant to carry the specification of the time bound around while deriving a recursive refinement. However, it is not necessary to consider

12 Predicative Semantics of Loops

all parts of a specification while deriving a refinement for it. If f is a monotone function of specifications, then

(T ∧ U ⊑ f.(V ∧ W)) ⇐ (T ⊑ f.V) ∧ (U ⊑ f.W) . In particular it may be useful to derive a recursive refinement for only the part of the specification that does not deal with time and then check that the same recursive refinement applies to the remainder of the specification.

For example R0 can be split into two ‘views’: R0 = T ∧ U

T = ⟨s′ = s × (Πi ∈ {x, ..N} · A.i⟩ ∨ Z
U = ⟨τ′ ≤ τ + N − x⟩ ∨ Z

We can then derive that

T ⊑ if x < N then(s, x := A.x, x + 1; tick; T) else skip and check that

U ⊑ if x < N then(s, x := A.x, x + 1; tick; U) else skip . This gives us that

R0 ⊑ if x < N then(s, x := A.x, x + 1; tick; R0) else skip .

4 CALCULATING THE LOOPS.

Weakest prespecification (Hoare and He 1987) is defined as

S↙U = ⟨∀σ̂, τ̂ · U.σ′.τ′.σ̂.τ̂ ⇒ S.σ.τ.σ̂.τ̂⟩ . (8) The key property of the weakest prespecification is this Galois connection:

(S↙U ⊑ T) ≡ (S ⊑ T; U) . (9) Suppose one has an R that is implementable, strongly bounded, time in-

sensitively bounded, and reasonable. The remaining condition on R, that of recursive refinement, is equivalent to the conjunction

(R ⊑ ⟨¬B⟩ ∧ skip)  (10)
∧  ((⟨B⟩ ⇒ R)↙(tick; R) ⊑ P)  (11)

So one can find a suitable loop implementation for R by first finding a B such that (10) (of course, the stronger this B is, the better) and then using as a loop body P = ⟨τ′ ≥ τ⟩ ∧ (⟨B⟩ ⇒ R)↙(tick; R), which is the weakest, progressive specification satisfying (11). Any refinement method can then be attempted to refine P by a program.

The first step, that of searching for a suitable B, can also be made more calculational. One can start with ¬R.σ.τ.σ.τ, which is the strongest solution of (10), and then weaken until a condition is found that is easily implemented.

5 CONCLUSION AND FUTURE WORK.

I have presented a semantics for iteration within a particular version of the refinement calculus. This semantics has been shown to enjoy the properties one would expect and also to give interesting results for infinite loops that suggest applications for communicating processes. From the semantics, I have proved a theorem that allows it to be used in the derivation of programs.

The proofs are done in a calculational and point-free style.

Although the notation used is suggestive of imperative programming, the results are equally applicable to functional programming — program variables are only introduced in the examples.

As mentioned above, one of the prime motivations for the weakest progressive post-fixed-point definition of while loops is to accommodate communicating processes. In this case observations would consist not only of an initial and final state, but also a history of communications. Thus generalizing these results to this more general setting is important.

Once processes may interact, potentially infinite loops become of greater interest and the restriction to strong bounding is too severe. The search for such programming theorems will be the subject of future research.

The work so far has concentrated on while loops, but the results should be extendible to any set of mutually recursive subroutines.

The relationship to (v. Karger and Hoare 1994) is intriguing. In that paper a very abstract calculus of specifications is presented. The principal difference between their calculus and relational calculus is the replacement of the converse operator by a relative converse operator. This prevents the formation of specifications that “undo”. This is the same motivation for restricting our attention to the lattice of progressive specifications and forming fixed-points within that lattice.

6 ACKNOWLEDGMENTS

Thanks are due to Eric Hehner for many discussions and comments, to the referees for helpful comments, to NSERC for funding, and to the Faculty of Engineering, Memorial University of Newfoundland, for equipment, location, and funding.

APPENDIX 0 PROOF OF THE IMPLEMENTABILITY THEOREM 1

(This appendix represents joint work with Eric Hehner.)

Given an implementable and progressive P we must show that

W = while B do P

too is implementable and progressive.

Throughout this appendix specification P will be assumed to be implementable and progressive. Rather than work with P, I will work with P 0 = P; tick. P 0 is also implementable and progressive.

By the progression axiom, we know that W = while B do P is progressive. The question remains whether it is implementable.

Suppose we can find an implementable Q that is also progressive and such that

if B then(P 0; Q) else skip ⊑ Q .

The induction axiom tells us that W ⊑ Q. Since any specification that is refined by an implementable specification must itself be implementable, this would imply that W is implementable. Thus the goal becomes: find a Q that is implementable, progressive, and a post-fixed-point.

There must be at least one progressive fixed-point. We know this because W is one example. In the following let S be any progressive fixed-point:

τ′ ≥ τ ⊑ S  (12)
S = if B then(P 0; S) else skip  .  (13)

S may or may not be implementable. We define a condition D to identify the initial states for which S accepts no final state:

D ≡ ¬(∃σ′, τ′ · S.σ.τ.σ′.τ′)  .  (14)

Now define Q as

Q = S ∨ (⟨D ∧ τ′ = ∞⟩)  .  (15)

It is clear that Q is implementable and progressive. We need only prove that it is a post-fixed-point.

To do this I will use two lemmata to be proved later:

⟨B⟩ ⊑ ⟨D⟩  (16)
⟨D⟩ ∧ P 0; X = ⟨D⟩ ∧ P 0; (⟨D⟩ ∧ X)  ,  (17)

for any X. Both follow from the fact that S is a fixed-point and will be proved later.

We prove that Q is a post-fixed-point by considering separately D true and D false. First for D true:

⟨D⟩ ∧ (if B then(P 0; Q) else skip)

=  “ (16) ⟨B⟩ ⊑ ⟨D⟩. ”

⟨D⟩ ∧ (P 0; Q)

=  “ Defn of Q. ”

⟨D⟩ ∧ (P 0; (S ∨ ⟨D ∧ τ′ = ∞⟩))

=  “ Distribute ; over ∨. ”

⟨D⟩ ∧ ((P 0; S) ∨ (P 0; ⟨D ∧ τ′ = ∞⟩))

=  “ Lemma (16) ⟨B⟩ ⊑ ⟨D⟩ ”

⟨D⟩ ∧ ((if B then(P 0; S) else skip) ∨ (P 0; ⟨D ∧ τ′ = ∞⟩))

=  “ S is a fixed-point. ”

⟨D⟩ ∧ (S ∨ (P 0; ⟨D ∧ τ′ = ∞⟩))

=  “ Lemma (17). ”

⟨D⟩ ∧ (S ∨ (P 0; ⟨τ′ = ∞⟩))

⊑  “ P 0 is implementable. ”

⟨D⟩ ∧ (S ∨ ⟨τ′ = ∞⟩)

=  “ Propositional calculus. ”

⟨D⟩ ∧ (S ∨ ⟨D ∧ τ′ = ∞⟩)

=  “ Defn of Q. ”

⟨D⟩ ∧ Q

Now for D false:

¬ ⟨D⟩ ∧ (if B then(P 0; Q) else skip)

=  “ Defn of Q. ”

¬ ⟨D⟩ ∧ (if B then(P 0; (S ∨ ⟨D ∧ τ′ = ∞⟩)) else skip)

⊑  “ Monotonicity. ”

¬ ⟨D⟩ ∧ (if B then(P 0; S) else skip)

=  “ S is a fixed-point. ”

16 Predicative Semantics of Loops

¬ ⟨D⟩ ∧ S

=  “ Propositional calculus .”

¬ ⟨D⟩ ∧ (S ∨ ⟨D ∧ τ′ = ∞⟩)

=  “ Defn of Q. ”

¬ ⟨D⟩ ∧ Q From

⟨D⟩ ∧ (if B then(P 0; Q) else skip ⊑ ⟨D⟩ ∧ Q and

¬ ⟨D⟩ ∧ (if B then(P 0; Q) else skip ⊑ ¬ ⟨D⟩ ∧ Q we can conclude

if B then(P 0; Q) else skip ⊑ Q . It remains to prove the two lemmata. We start with (16)

⟨B⟩ ⊑ ⟨D⟩

=  “ Contrapositive. ”

¬ ⟨D⟩ ⊑ ¬ ⟨B⟩

=  “ Definition of D. ”

⟨∃σ′, τ′ · S.σ.τ.σ′.τ′⟩ ⊑ ¬ ⟨B⟩

=  “ S is a fixed-point. ”

⟨∃σ′, τ′ · (if B then(P 0; S) else skip).σ.τ.σ′.τ′⟩ ⊑ ¬ ⟨B⟩

=  “ Definition of if . ”

⟨∃σ′, τ′ · skip.σ.τ.σ′.τ′⟩ ⊑ ¬ ⟨B⟩

=  “ skip is implementable. ”

⊤ It now remains only to prove (17). This follows easily from ⟨D′⟩ ⊑ P 0 ∧ ⟨D⟩

(D′ is D with σ and τ replaced by σ′ and τ′) which is proved by contradiction. Start with the negation:

∃σ, τ, σ′, τ′ · D ∧ P 0.σ.τ.σ′.τ′ ∧ ¬D′

≡  “ Rename variables. ”
∃σ, τ, σ′′, τ′′ · D ∧ P 0.σ.τ.σ′′.τ′′ ∧ ¬D′′
≡  “ Defn D. ”
∃σ, τ, σ′′, τ′′ · D ∧ P 0.σ.τ.σ′′.τ′′ ∧ (∃σ′, τ′ · S.σ′′.τ′′.σ′.τ′)
≡  “ Predicate calculus: ∃ over ∧ . ”
∃σ, τ, σ′, τ′, σ′′, τ′′ · D ∧ P 0.σ.τ.σ′′.τ′′ ∧ S.σ′′.τ′′.σ′.τ′
≡  “ Predicate calculus: ∃ over ∧ . ”
∃σ, τ, σ′, τ′ · D ∧ (∃σ′′, τ′′ · P 0.σ.τ.σ′′.τ′′ ∧ S.σ′′.τ′′.σ′.τ′)
≡  “ Definition of ; . ”
∃σ, τ, σ′, τ′ · D ∧ (P 0; S).σ.τ.σ′.τ′
≡  “ Lemma (16). ”
∃σ, τ, σ′, τ′ · D ∧ (if B then(P 0; S) else skip).σ.τ.σ′.τ′
≡  “ S is a fixed-point. ”
∃σ, τ, σ′, τ′ · D ∧ S.σ.τ.σ′.τ′
≡  “ Defn D. ”
∃σ, τ, σ′, τ′ · ¬(∃σ′, τ′ · S.σ.τ.σ′.τ′) ∧ S.σ.τ.σ′.τ′
≡  “ Predicate calculus: ∃ over ∧ . ”
∃σ, τ · ¬(∃σ′, τ′ · S.σ.τ.σ′.τ′) ∧ (∃σ′, τ′ · S.σ.τ.σ′.τ′)
≡  “ Contradiction. ”
⊥

APPENDIX 1 PROOF OF THE WHILE-LOOP THEOREM 2

We will assume

P is progressive; R is implementable, strongly bounded, time insensitively bounded, and reasonable; and R is recursively refined:

R ⊑ if B then(P; tick; R) else skip .

It must be shown that R ⊑ while B do P.

Throughout this appendix condition B and specification P will be assumed to have the properties stated in Theorem 2.

APPENDIX 1.0 ⟨τ = ∞⟩ or ⟨τ ∈ nat⟩

Ultimately I want to prove R ⊑ W. I will prove this by cases on ⟨τ = ∞⟩; i.e. by proving R ⊑ ⟨τ = ∞⟩ ∧ W and R ⊑ ⟨τ ∈ nat⟩ ∧ W. I start with the first

⟨τ = ∞⟩ ∧ W

⊒  “ Progression axiom ”

⟨τ = ∞⟩ ∧ ⟨τ′ ≥ τ⟩

=  “ xnat arithmetic”

⟨τ = ∞ = τ′⟩

⊒  “ Definition of Z and generalization”

Z ∨ R

=  “ R is reasonable ”

R

APPENDIX 1.1 B or ¬B

It remains to prove R ⊑ ⟨τ ∈ nat⟩ ∧ W. I will prove this by cases on ⟨B⟩. The easy case is when B is initially false. We do not need to use the fact that τ is finite.

¬ ⟨B⟩ ∧ W  (18)
=  “ W is a fixpoint of w (2). ”

¬ ⟨B⟩ ∧ w.W

=  “ Definition of w (1). ”

¬ ⟨B⟩ ∧ if B then(P; tick; W) else skip

=  “ Definition of if. ”

¬ ⟨B⟩ ∧ skip

=  “ Definition of if. ”

¬ ⟨B⟩ ∧ if B then(P; tick; R) else skip

=  “ Definition of w (1). ”

¬ ⟨B⟩ ∧ w.R

⊒  “ R is recusively refined (5) and monotonicity of ∧. ”

¬ ⟨B⟩ ∧ R

⊒  “ Specialization. ”

R .

On the other hand what about the case when B is initially true?

⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ W  (19)
=  “ W is a fixpoint of w (2). ”
⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ w.W
=  “ Definition of w (1). ”
⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ if B then(P; tick; W) else skip
=  “ Definition of if. ”
⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ (P; tick; W)
=  “ B ∧ ⟨τ ∈ nat⟩ is a condition. ”
(⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P); tick; W .

At this point we are a little stuck. It is time to bring out the heavy artillery...

APPENDIX 1.2 The repetend decreases the bound more than it spends time.

Here and below, I will write M for the expression m.σ.τ, and M′ for m.σ′.τ′. As R is strongly bounded, M is a natural number (i.e. not ∞); as R is timeinsensitively bounded, it does not depend on τ.

We now use our knowledge of R to conclude that P decreases the bound more than it spends time.

“ Recursive refinement (5) ”

R ⊑ w.R

=  “ Definition of w (1). ”

R ⊑ if B then(P; tick; R) else skip

⇒  “ Definition of if. ”

R ⊑ ⟨B⟩ ∧ (P; tick; R)

≡  “ B is a condition. ”

R ⊑ (⟨B⟩ ∧ P); tick; R

⇒  “ As M is a bound, ⟨τ′ ≤ τ + M⟩ ⊑ R; transitivity of ⊑ . ”

⟨τ′ ≤ τ + M⟩ ⊑ (⟨B⟩ ∧ P); tick; R

⇒ “ R could take as much time as M . ” (20)

⟨τ′ + M′ ≤ τ + M⟩ ⊑ (⟨B⟩ ∧ P); tick

≡  “ M does not depend on τ ”
⟨τ′ + M′ + 1 ≤ τ + M⟩ ⊑ ⟨B⟩ ∧ P  .  (21)

The hint at step (20) is an appeal to computational intuition, but can be fleshed out. To do so, we use the weakest prespecification (8).

It will be helpful to restate (0) using different variable names:

(∀σ′, τ′ · (∃σ̇, τ̇ · R.σ′.τ′.σ̇.τ̇ ∧ τ̇ = τ′ + M′))  .  (22)

We can now calculate:

⟨τ′ ≤ τ + M⟩ ↙R  (23)
=  “ Definition of weakest prespecification. ”
⟨∀σ̂, τ̂ · R.σ′.τ′.σ̂.τ̂ ⇒ τ̂ ≤ τ + M⟩
⊒  “ Specialize to any σ̇ and τ̇ that (22) says exist.

(These variables are dependant on σ′ and τ′.) ” ⟨R.σ′.τ′.σ̇.τ̇ ⇒ τ̇ ≤ τ + M⟩

=  “ From (22) we know R.σ′.τ′.σ̇.τ̇. ”
⟨τ̇ ≤ τ + M⟩
=  “ From (22) we know τ̇ = τ′ + M′. ”
⟨τ′ + M′ ≤ τ + M⟩  .

Now we can flesh out step (20):

⟨τ′ ≤ τ + M⟩ ⊑ (⟨B⟩ ∧ P); tick; R
≡  “ Galois connection (9). ”
⟨τ′ ≤ τ + M⟩ ↙R ⊑ (⟨B⟩ ∧ P); tick
⇒  “ Calculation (23) and transitivity. ”
⟨τ′ + M′ ≤ τ + M⟩ ⊑ (⟨B⟩ ∧ P); tick .

This completes the proof of (21). As a corollary we have:

“ P decreases the bound more than it consumes time (21). ”

⟨τ′ + M′ + 1 ≤ τ + M⟩ ⊑ ⟨B⟩ ∧ P
=  “ P is progressive. ”
⟨τ′ + M′ + 1 ≤ τ + M ∧ τ ≤ τ′⟩ ⊑ ⟨B⟩ ∧ P
⇒  “ Monotonicity of ∧ ”

⟨τ′ + M′ + 1 ≤ τ + M ∧ τ ≤ τ′ ∧ τ ∈ nat⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P

=  “ Both M and M′ are naturals ”

⟨τ′ + M′ + 1 ≤ τ + M ∧ τ ≤ τ′ ∧ τ, τ′ ∈ nat⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P

⇒  “ Transitivity of ≤ . ”

⟨τ′ + M′ + 1 ≤ τ′ + M ∧ τ ≤ τ′ ∧ τ, τ′ ∈ nat⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P

⇒  “ nat arithmetic. ”
⟨M′ + 1 ≤ M ∧ τ ≤ τ′ ∧ τ, τ′ ∈ nat⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P
⇒  “ Weakening the LHS of the refinement. ”
⟨M′ + 1 ≤ M⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P
⇒  “ M is natural. ”
⟨M′ < M⟩ ⊑ ⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P  .  (24)

APPENDIX 1.3 The induction

With these results in hand, we will prove that R ⊑ W. As we already have R ⊑ ¬ ⟨B⟩ ∧ W, and R ⊑ ⟨B⟩ ∧ ⟨τ = ∞⟩ ∧ W it remains to prove R ⊑ ⟨B⟩∧⟨τ ∈ nat⟩∧W. The proof is by complete induction on M, which, because of strong bounding, is a natural expression. Specifically we will prove, for any natural i,

R ⊑ ⟨M = i⟩ ∧ ⟨τ ∈ nat⟩ ∧ ⟨B⟩ ∧ W

follows from the induction hypothesis R ⊑ ⟨M < i⟩ ∧ ⟨τ ∈ nat⟩ ∧ ⟨B⟩ ∧ W. In light of calculation (18), we can see that the induction hypothesis implies

R ⊑ ⟨M < i⟩ ∧ ⟨τ ∈ nat⟩ ∧ W  .  (25)

Calculate

⟨M = i⟩ ∧ ⟨τ ∈ nat⟩ ∧ ⟨B⟩ ∧ W

=  “ Calculation (19). ”

⟨M = i⟩ ∧ (⟨B⟩ ∧ ⟨τ ∈ nat⟩ ∧ P); tick; W

⊒  “ (24). ”

(⟨B⟩ ∧ P); (⟨M < i⟩ ∧ ⟨τ ∈ nat⟩ ∧ tick); W

=  “ Time insensitivity. ”

(⟨B⟩ ∧ P); tick; (⟨M < i⟩ ∧ ⟨τ ∈ nat⟩ ∧ W)

⊒  “ Induction hypothesis (25). ”

(⟨B⟩ ∧ P); tick; R

=  “ B is a condition. ”

⟨B⟩ ∧ (P; tick; R)

⊒  “ Definition of if. ”

if B then(P; tick; R) else skip

=  “ Definition of w (1). ”
w.R
⊒  “ R is recursively refined (5). ”
R .

It is interesting that there is no need to break the proof into zero and non-zero cases. The reason is that one falls into the ¬B case before hitting zero.

REFERENCES

Back, R. J. R. and von Wright, J., (1990). Refinement calculus, part 1: Sequential nondeterministic programs. In de Backer, J. W., de Roever, W.- P., and Rosenberg, G., editors, Stepwise Refinement of Distributed Systems: Models Formalisms, Correctness, number 430 in Lecture Notes in Computer Science. Springer-Verlag, 1990. Hehner, Eric C. R., (1979). do considered od: A contribution to the programming calculus. Acta Informatica, 11:287–304, 1979. Hehner, Eric C. R., (1984). Predicative programming. Communications of the ACM, 27(2):134–151, 1984. Hehner, Eric C. R., (1993). A Practical Theory of Programming. Springer-Verlag, 1993. Hehner, Eric C. R., (1994). Abstractions of time. In Roscoe, A. W., editor, A Classical Mind, chapter 12, pages 195–214. Prentice-Hall International, 1994. Hoare, C. A. R and He, JiFeng, , (1987). The weakest prespecification. Information Processing Letters, 24:127–132, 1987. Hoare, C. A. R., (1985). Programs are predicates. In Hoare, C. A. R. and Shepherdson, J. C., editors, Mathematical Logic and Programming Languages, pages 141–155. Prentice Hall, 1985. Hoare, C. A. R., (1994). Mathematical models for computer science. Technical report, Oxford University Computing Laboratory, Oxford University, August 1994. Holt, Richard C., (1991). Healthiness versus realizability in predicate transformers. Technical Report CSRI-240, Computer Systems Research Institute, University of Toronto, 1991. Morgan, Carroll, (1990). Programming from Specifications. Prentice Hall International, 1990. Norvell, Theodore S., (1993). A Predicative Theory of Machine Languages and its Application to Compiler Correctness. PhD thesis, University of Toronto, December 1993. Norvell, Theodore S., (1994). Machine code programs are predicates too. In Till, David, editor, Sixth Refinement Workshop, Workshops in Computing, pages 188–204. Springer Verlag, 1994.

Sekerinski, Emil, (1993). A calculus for predicative programming. In Mathematics of Program Construction 1992, number 669 in LNCS, pages 302– 322. Springer-Verlag, 1993. Spivey, J. M., (1989). The Z Notation: A Reference Manual. Prentice-Hall, 1989. Tarski, Alfred, (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955. v. Karger, Burghard and Hoare, C. A. R, (1994). Sequential calculus. Information Processing Letters, 53:123–131, 1994.

BIOGRAPHY

A native of Halifax, Nova Scotia, Theodore Norvell obtained Master’s and Ph.D. degrees in Computing Science from the University of Toronto. He has worked in the software development industry and has done postdoctoral work both at the Programming Research Group of Oxford University and at the Software Engineering Research Group of McMaster University. He is currently a professor of engineering at Memorial University of Newfoundland.

His research interests include formal specification and derivation of programs, programming language design, and formal aspects of software and hardware engineering.