Idealized Algol and its Specification Logic^{1}

John C. Reynolds School of Computer and Information Science Syracuse University Syracuse, New York

1. Introduction^{2}

Specification logic is a new formal system for program proving that is applicable to programming languages, such as Algol, whose procedure mechanism can be described by the copy rule. The starting point of its development is the recognition that, in the presence of an Algol-like procedure mechanism, specifications, such as the Hoare triple {P } S {Q} [1], must be regarded as predicates about environments (in the sense of Landin [2, 3]). The logic provides additional kinds of specifications describing an interference relation (#) between variables and other entities, and permits specifications to be compounded using the operations of implication (⇒), conjunction (&), and universal quantification (∀). The result is a system in which one can infer universal specifications, i.e., specifications that hold in all environments.

To see why the introduction of procedures makes a specification depend upon an environment (which is a mapping from the free identifiers of the specification into appropriate meanings), it is enough to consider any nontrivial Hoare triple involving a procedure call. For example, the truth of

{x = 3}x := double(x){x = 6}

clearly depends upon the meaning into which double is mapped by the relevant environment.

More surprisingly, since procedures introduce the phenomenon of interference (of which the simplest case is aliasing between variables), even specifications that do not refer to procedures overtly can still depend upon the environment. For example,

{x = 3}y := 4{x = 3}

(which is provable from Hoare’s axiom of assignment and is universally true in the absence of a procedure mechanism) depends upon whether x and y are aliases, i.e., whether they are mapped by the environment into the same storage location, so that assignment to one will change the value of the other.

1Work supported by National Science Foundation Grant MCS-8017577 and U.S. Army Contract DAAK80-80-C-0529. First appeared in D. Néel, editor, Tools and Notions for Program Construction, pages 121–161, Cambridge University Press 1982. Reprinted in Algol-like Languages, ed. P. W. O’Hearn and R. D. Tennent, vol. 1, pp. 125–156, Birkhäuser, 1997.

2The first part of this section was extended by the author in 1996.

In fact, to obtain universal specifications about commands in Algol-like languages, it is necessary to extend the language of specifications well beyond Hoare triples. A simple example of a universal specification is

y # x ⇒ {x = 3}y := 4{x = 3} ,

which specifies that, if the meaning of y does not interfere with the meaning of x, then assigning 4 to y will preserve the assertion x = 3. Another example is

{(∀n) double(n) = n + n} & gv_{int}(x) ⇒ {x = 3}x := double(x){x = 6} ,

which specifies that, if the meaning of double is a function procedure that doubles any integer, and if the meaning of x is a “good variable” (a technical condition described in Section 7), then executing x := double(x) in a state where x = 3 will produce a state where x = 6.

It is important to distinguish specifications from assertions, which are the first and last members of Hoare triples (i.e., the phrases enclosed in braces). While the truth of a specification depends only upon an environment, which maps identifiers into their meanings, the truth of an assertion depends upon both an environment and a storage state, which maps locations into values.

Although proof methods for procedures have been the subject of considerable research [4, 5, 6, 7], this work has focused on call by reference and call by value, and had led to extremely complex inference rules that are incapable of dealing with interference, call by name, statement parameters, or higher-order procedures. In contrast, specification logic is both simpler and more general. It assumes that the procedure mechanism is based upon a typed lambda calculus that encompasses the logic for program proving as well as the programming language.

In [8], a version of specification logic is given for the sublanguage of Algol W [9] that represents a refinement of Algol 60. In this report, we develop specification logic for a subset of the language described in [10], which is an idealization of Algol that makes the underlying (typed) lambda calculus explicit.

The advantage is that this language desugars well, i.e., many of its constructs can be defined as abbreviations in terms of a simpler “base” language. As a consequence, one can begin with simple inference rules for the base language and then derive more complex rules for the abbreviationally defined constructs. In particular, the complex aspects of inference that arise from binding can be encapsulated in the process of beta-reduction, which is applicable to specifications as well as programs.

In this report we will avoid formulating the semantics of specifications. Although a semiformal semantics is given in [8], there is some doubt that it is the “right” semantics. As we will see in Section 11, there are useful and apparently noncontradictory rules of inference that are not valid in this semantics.

It should be emphasized that this is a preliminary report of ongoing research. Both the programming language and logic described in it can be expected to change considerably in the future.

2. Syntax

The programming language we consider is basically a sublanguage of that described in [10], with the following restrictions:

(1) Recursive definition is permitted for commands, acceptors, and proper procedures, but not for expressions or function procedures.

This limitation is an inevitable (though regrettable) consequence of using the predicate calculus for assertions, along with the vital assumption that any expression of the programming language can occur as a term in such assertions. Recursive definition of expressions or function procedures would impose a domain structure upon their meanings that would be incompatible with the free use of quantifiers, because of their lack of continuity. In other words, we cannot deal with nonterminating expressions and function procedures because we cannot deal with nonterminating assertions.

Since nontermination is meaningless for certain phrase types, we must also abandon the phrase type univ(ersal).

(2) Multiple declarations (including mutual recursion), case statements, arrays, and labels are not treated.

These topics are simply omitted for brevity; none of them appear to raise fundamental difficulties in specification logic. (Arrays, labels, and also for statements are treated in [8].)

(3) Products and sums of data types are not treated.

Here our experience is too limited to say much; we have yet to explore the treatment of these topics in specification logic.

The following productions describe the various kinds of type we will use:

⟨data type⟩ ::= integer | real | Boolean

⟨ordinary phrase type⟩ ::= ⟨data type⟩ exp | ⟨data type⟩ acc | ⟨data type⟩ ⟨data type⟩ var | comm | ⟨ordinary phrase type⟩ → ⟨ordinary phrase type⟩ ⟨recursive phrase type⟩ ::= ⟨data type⟩ acc | comm

| ⟨ordinary phrase type⟩ → ⟨recursive phrase type⟩

⟨bindable phrase type⟩ ::= ⟨ordinary phrase type⟩ | commlike | explike

⟨phrase type⟩ ::= ⟨bindable phrase type⟩ | spec

A data type denotes a set of values appropriate for some kind of variable or expression, while a phrase type denotes a set of meanings appropriate for some kind of phrase. Among phrase types in general, bindable phrase types are those that can be denoted by identifiers, ordinary phrase types are those that can be denoted by identifiers that are bound by lambda expressions, and recursive phrase types are those for which recursive definition is permitted.

(Notice that variables are classified separately by the data types they accept and produce, i.e., τ_{1}τ_{2} var means τ_{1}-accepting τ_{2}-producing variable. The rationale for this complication is given in [10].)

Throughout this paper we will use the following metavariables to range over various kinds of type:

τ: data types

ρ: recursive phrase types

θ: ordinary phrase types

ω: bindable phrase types

γ: phrase types.

For both data and phrase types, there is a partial ordering called the subtype relation. For data types, it is the least partial ordering such that integer ≤ real. For phrase types, it is the least partial ordering such that:

τ ≤ τ′ implies τ exp ≤ τ′ exp

τ′ ≤ τ implies τ acc ≤ τ′ acc

τ′_{1} ≤ τ_{1} and τ_{2} ≤ τ′_{2} implies τ_{1}τ_{2} var ≤ τ′_{1}τ′_{2} var

τ_{1}τ_{2} var ≤ τ_{1} acc

τ_{1}τ_{2} var ≤ τ_{2} exp θ′_{1} ≤ θ_{1} and θ_{2} ≤ θ′_{2} implies θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}

τ acc ≤ commlike

comm ≤ commlike

θ_{2} ≤ commlike implies θ_{1} → θ_{2} ≤ commlike

τ exp ≤ explike

θ_{2} ≤ explike implies θ_{1} → θ_{2} ≤ explike.

When γ ≤ γ′ we say that γ is a subtype of γ′; the intent is that there is an implicit conversion from the meanings for γ to the meanings for γ′, so that any phrase of type γ can be used in any context requiring a phrase of type γ′.

A type assignment is a function from a finite set of identifiers to bindable phrase types. Throughout this paper, we use the metavariable ι to range over identifiers and the metavariable π to range over type assignments.

The subtype relation is extended to type assignments as follows:

π ≤ π′ if and only if dom(π′) ⊆ dom(π) and (∀ι ∈ dom(π′)) π(ι) ≤ π′(ι)

where dom(π) denotes the domain of the function π.

To describe the syntax of both our programming language and the language of specifications, we will use phrase class names of the form ⟨γ, π⟩, where γ is a phrase type and π is a type assignment. The intent is that ⟨γ, π⟩ denotes the set of phrases P such that

(1) The identifiers occurring free in P belong to the domain of π.

(2) When its free identifiers are given the bindable phrase types indicated by π, P has phrase type γ.

We will only describe abstract syntax, ignoring considerations of parenthesization and precedence, and using production schemas containing the metavariables τ, ρ, θ, ω, γ, ι, and π (with occasional sub- and superscripts) whose ranges have been described above. First, we describe the “generic” part of the language, i.e., constructs that are applicable to a variety of phrase types:

⟨γ′, π⟩ ::= ⟨γ, π⟩ when γ ≤ γ′
⟨ω, π⟩ ::= ι when ι ∈ dom(π) and π(ι) = ω
⟨θ_{2}, π⟩ ::= ⟨θ_{1} → θ_{2}, π⟩ (⟨θ_{1}, π⟩)
⟨θ_{1} → θ_{2}, π⟩ ::= λι: θ_{1}. ⟨θ_{2}, [π | ι: θ_{1}]⟩

⟨ρ, π⟩ ::= rec ⟨ρ → ρ, π⟩

⟨ρ, π⟩ ::= ⊥_{ρ}

⟨θ, π⟩ ::= if ⟨Boolean exp, π⟩ then ⟨θ, π⟩ else ⟨θ, π⟩

⟨θ_{2}, π⟩ ::= let ι be ⟨θ_{1}, π⟩ in ⟨θ_{2}, [π | ι: θ_{1}]⟩

⟨θ, π⟩ ::= letrec ι: ρ be ⟨ρ, [π | ι: ρ]⟩ in ⟨θ, [π | ι: ρ]⟩

The first schema shows the purpose of the subtype relation. The second shows that an identifier assigned some bindable phrase type can be used as a phrase of that type.

The next two schemas describe procedure application (i.e., call) and lambda abstraction. We limit ourselves to procedures with a single parameter, since multiple parameters can be eliminated by Currying [10].

In the fourth schema [π | ι: θ_{1}] denotes the type assignment such that

dom([π | ι: θ_{1}]) = dom(π) ∪ {ι}

[π | ι: θ_{1}] (ι) = θ_{1}

[π | ι: θ_{1}] (ι′) = π(ι′) when ι′ ≠ ι.

Later we will use the following extensions of this notation:

[π | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}] = [⋯ [π | ι_{1}: θ_{1}] ⋯ | ι_{n}: θ_{n}]

[ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}] = [[ ] | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}],

where [ ] is the type assignment with empty domain.

The fifth and sixth schemas describe the least-fixed-point operator rec and the leastelement constant ⊥, both of which are limited to recursive phrase types.

The seventh schema describes a generic conditional construction that is applicable to all ordinary phrase types.

The last two schemas introduce Landin’s notation [2, 3] for nonrecursive and recursive declarations (limited to recursive phrase types in the latter case). For simplicity, we avoid the multiple declarations considered in [10].

Notice that, quite aside from our neglect of parenthesization and precedence, this syntax is ambiguous with regard to phrase types. For example,

if ⟨Boolean exp, π⟩ then ⟨real real var, π⟩ else ⟨real real var, π⟩ can be derived from ⟨real exp, π⟩ by either

[figure: ⟨real exp, π⟩; if; ⟨Boolean exp, π⟩; then; ⟨real exp, π⟩; else; ⟨real exp, π⟩; ⟨real real var, π⟩; ⟨real real var, π⟩]

or

[figure: ⟨real exp, π⟩; ⟨real real var, π⟩; if; ⟨Boolean exp, π⟩; then; ⟨real real var, π⟩; else; ⟨real real var, π⟩]

Similarly, ⟨real exp → comm, π⟩(⟨integer exp, π⟩) can be derived from ⟨comm, π⟩ by either

[figure: ⟨comm, π⟩; ⟨real exp → comm, π⟩; (; ⟨real exp, π⟩; ); ⟨integer exp, π⟩]

or

[figure: ⟨comm, π⟩; ⟨integer exp → comm, π⟩; (; ⟨integer exp, π⟩; ); ⟨real exp → comm, π⟩]

We assume that this kind of ambiguity does not lead to ambiguous meaning.

Next we give more specific production schemas describing expressions and commands. The schemas for expressions are obviously incomplete; the inclusion of additional constants and operations would be straightforward though uninteresting.

⟨integer exp, π⟩ ::= 0 | 1 | ⟨integer exp, π⟩ + ⟨integer exp, π⟩

⟨real exp, π⟩ ::= 0.5 | ⟨real exp, π⟩ + ⟨real exp, π⟩

⟨Boolean exp, π⟩ ::= true | false | ⟨τ exp, π⟩ = ⟨τ exp, π⟩ | ⟨Boolean exp, π⟩ and ⟨Boolean exp, π⟩ | (∀ι) ⟨Boolean exp, [π | ι: integer exp]⟩ | (∃ι) ⟨Boolean exp, [π | ι: integer exp]⟩

⟨comm, π⟩ ::= skip | ⟨τ acc, π⟩ := ⟨τ exp, π⟩ | ⟨comm, π⟩; ⟨comm, π⟩ | while ⟨Boolean exp, π⟩ do ⟨comm, π⟩ | new τ var ι in ⟨comm, [π | ι: τ τ var]⟩

Notice that we permit Boolean expressions to contain quantifiers, at least over the set of integers. This will permit us to simplify our presentation by equating assertions with Boolean expressions. Of course, one cannot actually implement the evaluation of quantifiers, but semantically, quantified expressions have exactly the same kind of meaning as other logical expressions. It should be noted, however, that this view is tenable only because we have prohibited recursive functions and other constructs that would impose on the meaning of expressions a domain structure for which quantification would not be a continuous operation.

Finally, we give the syntax of specifications:

⟨spec, π⟩ ::= {⟨Boolean exp, π⟩}⟨comm, π⟩{⟨Boolean exp, π⟩} | {⟨Boolean exp, π⟩} | ⟨commlike, π⟩ # ⟨explike, π⟩ | ⟨spec, π⟩ & ⟨spec, π⟩ | ⟨spec, π⟩ ⇒ ⟨spec, π⟩ | (∀ι: ω)⟨spec, [π | ι: ω]⟩ | gv_{τ}( ⟨τ τ var, π⟩ )

A specification of the form {P } C {Q} is true if and only if, for all states of the store in which P is true executing C either does not terminate or terminates with a state for which Q is true. This differs from Hoare’s definition [1] in being implicitly quantified over states of the store but not over environments, since in our formalism {P } C {Q}, like any other kind of specification, is a predicate about environments.

A specification of the form {P } is true if and only if P is true for all states of the store; in this case we say that P is a static assertion.

A specification of the form C # E is true if and only if C does not interfere with E. When C is a command and E is an expression this means that for any state of the store, executing C will not, at any time during the execution, affect the value of E. The meaning of this specification for other command-like and expression-like phrases will be clarified by equivalences in Sections 5 and 6.

The operators &, ⇒, and ∀ denote conjunction, implication, and universal quantification of specifications. (In contrast to [8], we do not combine & and ⇒ into a single operation.) Notice that quantification is over meanings of a particular phrase type (not values of a particular data type).

A specification of the form gv_{τ}(V) means that V is a “good” variable, i.e., a variable that will always possess the last value assigned to it. This will be clarified by an equivalence in Section 7.

In conclusion, we state without proof a global property of our syntax. If π′ ≤ π and γ′ ≤ γ′ then ⟨γ, π⟩ ⊆ ⟨γ′, π′⟩. (When a phrase class name ⟨γ, π⟩ is used as a set, it denotes the set of all phrases derivable from ⟨γ, π⟩.) When π′ = π this is an immediate consequence of the production schema describing the subtype relation; however, the general case requires a structural induction argument involving the entire syntax.

3. Equivalences

Basically, two phrases are equivalent if they possess the same meaning in every environment or, more abstractly, if they possess the same semantics. However, this concept is complicated by the possibility that a phrase may belong to more than one phrase class ⟨γ, π⟩, and possess a distinct semantics for each phrase class to which it belongs.

For this reason we must qualify equivalences with phrase class names. When P and Q belong to ⟨γ, π⟩ and have the same semantics for ⟨γ, π⟩, we write P ≡_{γ,π} Q and say that P and Q are equivalent for ⟨γ, π⟩.

Suppose π′ ≤ π and γ ≤ γ′. If P ≡_{γ,π} Q holds then P ≡_{γ′,π′} Q will also hold. We will call this kind of deduction “type broadening.”

Although types can be broadened, they cannot always be “narrowed.” For example,

k > 4 ≡_{Boolean exp, [k: integer exp]} k ≥ 5

is true, but

k > 4 ≡_{Boolean exp, [k: real exp]} k ≥ 5

is false.

However, there is a special case in which type assignments can be narrowed: if P ≡_{γ,π} Q holds and π′ is a restriction of π whose domain includes all identifiers that occur free in P or Q, then P ≡_{γ,π′} Q.

We will usually describe sets of equivalences schematically. For example, to express the validity of beta reduction, suppose P ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩ and Q ∈ ⟨θ_{1}, π⟩. Then

(λι: θ_{1}. P)(Q) ≡_{θ_{2},π} P |_{ι→Q} .  (3.1)

Here P |_{ι→Q} denotes the result of substituting Q for the free occurrences of ι in P, with appropriate renaming of bound identifiers in P. More generally, if ι_{1}, …, ι_{n} are distinct identifiers, P ∈ ⟨γ, [π | ι_{1}: ω_{1} | ⋯ | ι_{n}: ω_{n}]⟩, and Q_{1} ∈ ⟨ω_{1}, π⟩,…,Q_{n} ∈ ⟨ω_{n}, π⟩, then

P |_{ι_{1},...,ι_{n}→Q_{1},...,Q_{n}}

denotes the phrase in ⟨γ, π⟩ obtained by substituting each Q_{i} for the free occurrences of ι_{i} in P, with appropriate renaming.

To express the validity of eta reduction, suppose P ∈ ⟨θ_{1} → θ_{2}, π⟩ and ι ∉ dom(π) (so that ι does not occur free in P). Then

λι: θ_{1}. (P (ι)) ≡_{θ_{1}→θ_{2},π} P .  (3.2)

Further equivalences describe the operator rec, the constant ⊥, and the conditional construction. If P ∈ ⟨ρ → ρ, π⟩ then

rec P ≡_{ρ,π} P (rec P) .  (3.3)

If P ∈ ⟨θ, π⟩ then

⊥_{θ→ρ} (P) ≡_{ρ,π} ⊥_{ρ} .  (3.4)

On the other hand,

λι: θ. ⊥_{ρ} ≡_{θ→ρ,π} ⊥_{θ→ρ} .  (3.5)

If P ∈ ⟨Boolean exp, π⟩, Q_{1}, Q_{2} ∈ ⟨θ_{1} → θ_{2}, π⟩, and R ∈ ⟨θ_{1}, π⟩, then

(if P then Q_{1} else Q_{2})(R) ≡_{θ_{2},π} if P then Q_{1}(R) else Q_{2}(R) .  (3.6)

On the other hand, if P ∈ ⟨Boolean exp, π⟩, Q_{1}, Q_{2} ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩ and ι ∉ dom(π), then

λι: θ_{1}. if P then Q_{1} else Q_{2} ≡_{θ_{1}→θ_{2},π} if P then λι: θ_{1}. Q_{1} else λι: θ_{1}. Q_{2} .  (3.7)

The let and letrec constructions are described by equivalences that can be regarded as definitions of these constructions in terms of application, abstraction, and rec. If P ∈ ⟨θ_{1}, π⟩ and Q ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩ then

let ι be P in Q ≡_{θ_{2},π} (λι: θ_{1}. Q)(P) .  (3.8)

If P ∈ ⟨ρ, [π | ι: ρ]⟩ and Q ∈ ⟨θ, [π | ι: ρ]⟩ then

letrec ι: ρ be P in Q ≡_{θ,π} (λι: ρ. Q)(rec λι: ρ. P) .  (3.9)

Next, we give more specific equivalences describing commands. Suppose C, C′, C′′ ∈ ⟨comm, π⟩, P ∈ ⟨Boolean exp, π⟩, A, A′ ∈ ⟨τ acc, π⟩, and E, E′ ∈ ⟨τ exp, π⟩. Then

C; skip ≡_{comm,π} C  (3.10)
skip; C ≡_{comm,π} C  (3.11)
C; (C′ ; C′′) ≡_{comm,π} (C ; C′); C′′  (3.12)
A := if P then E else E′ ≡_{comm,π} if P then A := E else A := E′  (3.13)
(if P then A else A′) := E ≡_{comm,π} if P then A := E else A′ := E  (3.14)
(if P then C else C′); C′′ ≡_{comm,π} if P then (C; C′′) else (C′; C′′)  (3.15)
while P do C ≡_{comm,π} if P then (C; while P do C) else skip.  (3.16)

There are also obvious equivalences describing the conjunction and implication of specifications. Suppose S, S′, S′′ ∈ ⟨spec, π⟩. Then

{true} & S ≡_{spec,π} S  (3.17)
{false} & S ≡_{spec,π} {false}  (3.18)
(S & S′) & S′′ ≡_{spec,π} S & (S′ & S′′)  (3.19)
S & S′ ≡_{spec,π} S′ & S  (3.20)
S & S ≡_{spec,π} S  (3.21)
{true} ⇒ S ≡_{spec,π} S  (3.22)
{false} ⇒ S ≡_{spec,π} {true}  (3.23)
S ⇒ {true} ≡_{spec,π} {true}  (3.24)
S ⇒ S ≡_{spec,π} {true}  (3.25)
S ⇒ (S′ ⇒ S′′) ≡_{spec,π} S & S′ ⇒ S′′  (3.26)
S ⇒ S′ & S′′ ≡_{spec,π} (S ⇒ S′) & (S ⇒ S′′).  (3.27)

Finally, there are an indefinite number of equivalences of the form

P ≡_{Boolean exp,π} true  (3.28)

that describe the mathematics of data types. When the above equivalence holds, we say that P ∈ ⟨Boolean exp, π⟩ is a mathematical fact for π. For example, k > 4 implies k ≥ 5 is a mathematical fact for [k: integer exp].

4. Universal Specifications and Their Inference

Roughly speaking, a specification is said to be universal if it is true for all environments. However, much as with equivalences, the situation is complicated by the fact that a specification can belong to ⟨spec, π⟩ for several type assignments π, and that its universality can depend upon π. To be precise, when S ∈ ⟨spec, π⟩ and the semantics of S for ⟨spec, π⟩ maps all environments in its domain into true, we write S : : π and say that S is universal for π.

For example,

{k > 4} ⇒ {k ≥ 5} : : [k: integer exp] ,

but not

{k > 4} ⇒ {k ≥ 5} : : [k: real exp] .

Specification logic is a formal system for inferring universal specifications. Its rules of inference are schemas with the form “If S_{1} : : π_{1} and ⋯ and S_{n} : : π_{n} then S : : π,” usually prefaced by restrictions on metavariables. The n ≥ 0 specifications S_{1}, …, S_{n} are called premisses and S is called the conclusion.

Our first rule of inference captures the idea that a specification will remain universal when any subphrase is replaced by another subphrase to which it is equivalent. To state this precisely, we must characterize “subphrase” syntactically:

(4.1) Inference by Equivalence. Suppose S ∈ ⟨spec, π⟩, P ≡_{γ,π′} Q, and there is a derivation of S from ⟨spec, π⟩ containing a subderivation of P from ⟨γ, π′⟩. Let S′ be the specification derived from ⟨spec, π⟩ by the derivation obtained from the derivation of S by replacing the subderivation of P by a subderivation of Q. If

S : : π

then

S′ : : π .

Next, we have two rules for broadening and narrowing type assignments in much the same way as for equivalences:

(4.2) Broadening Type Assignments. If S ∈ ⟨spec, π⟩ and π′ ≤ π and

S : : π

then S : : π′ .

(4.3) Narrowing Type Assignments. If S ∈ ⟨spec, π⟩ is a restriction of π whose domain includes all identifiers occurring free in S, and

S : : π

then

S : : π′ .

Three more rules are needed to capture the properties of & and ⇒. In these rules we assume S_{1}, S_{2}, S_{3} ∈ ⟨spec, π⟩:

(4.4) Truth.

{true} : : π .

(4.5) Adding Assumptions. If

S_{2} : : π

then

S_{1} ⇒ S_{2} : : π .

(4.6) Modus Ponens. If

S_{1} ⇒ S_{2} : : π

and

S_{2} ⇒ S_{3} : : π

then

S_{1} ⇒ S_{3} : : π .

Since they are so similar to ordinary logic, we will often omit the details of applying these rules, as well as applying (4.1) for equivalences (3.17) to (3.27).

Two more rules deal with quantification:

(4.7) Quantifier Introduction. Suppose S_{1} ∈ ⟨spec, π⟩, S_{2} ∈ ⟨spec, [π | ι: ω]⟩ and ι ∉

dom(π). If

S_{1} ⇒ S_{2} : : [π | ι: ω]

then

S_{1} ⇒ (∀ι: ω)S_{2} : : π .

(4.8) Quantifier Removal. Suppose S ∈ ⟨spec, [π | ι_{1}: ω_{1} | ⋯ |ι_{n}: ω_{n}]⟩, and P_{1} ∈ ⟨ω_{1}, π⟩, …, P_{n} ∈ ⟨ω_{n}, π⟩, where ι_{1}, …, ι_{n} are distinct identifiers. Then

(∀ι_{1}: ω_{1}) ⋯ (∀ι_{n}: ω_{n})S ⇒ S|_{ι_{1},...,ι_{n}⟶P_{1},...,P_{n}} : : π .

From these rules we can derive the fact that universality is preserved by substitution:

(4.9) Free Substitution. Suppose S ∈ ⟨spec, [π | ι_{1}: ω_{1} | ⋯ | ι_{n}: ω_{n}]⟩, P_{1} ∈ ⟨ω_{1}, π⟩, …, P_{n} ∈ ⟨ω_{n}, π⟩, ι_{1}, …, ι_{n} are distinct, and

S : : [π | ι_{1}: ω_{1} | ⋯ | ι_{n}: ω_{n}] .

From (4.5),

{true} ⇒ S : : [π | ι_{1}: ω_{1} | ⋯ | ι_{n}: ω_{n}] ,

and by repeated application of (4.7),

{true} ⇒ (∀ι_{n}: ω_{n})S : : [π | ι_{1}: ω_{1} | ⋯ | ι_{n−1}: ω_{n−1}]
⋮
{true} ⇒ (∀ι_{1}: ω_{1}) ⋯ (∀ι_{n}: ω_{n})S : : π .

Then (4.8), with modus ponens, gives

{true} ⇒ S|_{ι_{1},...,ι_{n}⟶P_{1},...,P_{n}} : : π ,

and equivalence (3.22), via (4.1), gives the conclusion

S|_{ι_{1},...,ι_{n}⟶P_{1},...,P_{n}} : : π .

The derivation of this rule typifies the form of such derivations that will be used in most of this report: it simply consists of a statement of the rule with an appropriate argument inserted between premisses and conclusion.

Next, we derive a rule that permits any mathematical fact to be used as a static assertion:

(4.10) Mathematical Fact Introduction. Suppose P is a mathematical fact for π. Then applying equivalence (3.28) to {true} : : π gives the conclusion

{P } : : π .

Finally, we give a collection of rules which contain neither premisses nor metavariables, and are therefore simply axioms, i.e., particular specifications that are universal. The first of these rules serves to “lift” reasoning about assertions into reasoning about specifications. The next eight rules are reformulations of various aspects of Hoare’s logic [1], and the final rule says that a command will preserve an assertion that it does not interfere with. For these rules we assume π is a type assignment mapping p, q, r, i, p_{1}, p_{2}, q_{1}, q_{2} and ℓ into Boolean exp, and c, c_{1}, and c_{2} into comm:

(4.11) Static Implication.

{p} & {p implies q} ⇒ {q} : : π .

(4.12) Command Composition.

{p} c_{1} {q} & {q} c_{2} {r} ⇒ {p} c_{1}; c_{2} {r} : : π .

(4.13) Strengthening Precedent.

{p implies q} & {q} c {r} ⇒ {p} c {r} : : π .

(4.14) Weakening Consequent.

{p} c {q} & {q implies r} ⇒ {p} c {r} : : π .

(4.15) while Command.

{i and ℓ} c {i} ⇒ {i} while ℓ do c {i and ¬ℓ} : : π .

(4.16) Conditional Command.

{p and ℓ} c_{1} {q} & {p and ¬ℓ} c_{2} {q}
⇒ {p} if ℓ then c_{1} else c_{2} {q} : : π .

(4.17) skip Command.

{p} skip {p} : : π .

(4.18) Specification Conjunction.

{p_{1}} c {q_{1}} & {p_{2}} c {q_{2}} ⇒ {p_{1} and p_{2}} c {q_{1} and q_{2}} : : π .

(4.19) Specification Disjunction.

{p_{1}} c {q_{1}} & {p_{2}} c {q_{2}} ⇒ {p_{1} or p_{2}} c {q_{1} or q_{2}} : : π .

(4.20) Constancy.

c # p & {q} c {r} ⇒ {q and p} c {r and p} : : π .

The occurrence of # in the rule of constancy raises the question of how one can infer noninterference specifications, which will be considered in the next two sections.

5. Leftside Noninterference Decomposition

In this section and the next, we develop equivalences and inference rules describing noninterference. The overall effect of these rules is to allow any noninterference specification C # E to be decomposed into noninterference specifications in which only identifiers occur on the leftside, or rightside, of #. In this section, we deal with leftside decomposition.

To begin, several equivalences serve to define noninterference for acceptors and proper procedures in terms of noninterference for commands. If A ∈ ⟨τ acc, π⟩, E ∈ ⟨explike, π⟩, and ι ∉ dom(π), then

A # E ≡_{spec,π} (∀ι: τ exp)(A := ι # E) .  (5.1)

If θ_{1} ≰ commlike, θ_{2} ≤ commlike, H ∈ ⟨θ_{1} → θ_{2}, π⟩, E ∈ ⟨explike, π⟩, and ι ∉ dom(π), then

H # E ≡_{spec,π} (∀ι: θ_{1}) H(ι) # E .  (5.2)

If θ_{1} ≤ commlike, θ_{2} ≤ commlike, H ∈ ⟨θ_{1} → θ_{2}, π⟩, E ∈ ⟨explike, π⟩, and ι ∉ dom(π), then

H # E ≡_{spec,π} (∀ι: θ_{1})(ι # E ⇒ H(ι) # E) .  (5.3)

In addition, there are basic leftside decomposition rules for a variety of constructs in the language:

(5.4) If P ∈ ⟨ρ → ρ, π⟩ and E ∈ ⟨explike, π⟩ then

P # E ⇒ rec P # E : : π .

(5.5) If E ∈ ⟨explike, π⟩ then

⊥_{ρ} # E : : π .

(Notice that ρ ≤ commlike holds for all recursive phrase types.)

(5.6) If θ ≤ commlike, B ∈ ⟨Boolean exp, π⟩, P_{1}, P_{2} ∈ ⟨θ, π⟩, and E ∈ ⟨explike, π⟩, then

P_{1} # E & P_{2} # E ⇒ if B then P_{1} else P_{2} # E : : π .

(5.7) If E ∈ ⟨explike, π⟩ then

skip # E : : π .

(5.8) If C_{1}, C_{2} ∈ ⟨comm, π⟩ and E ∈ ⟨explike, π⟩ then

C_{1} # E & C_{2} # E ⇒ C_{1}; C_{2} # E : : π .

(5.9) If B ∈ ⟨Boolean exp, π⟩, C ∈ ⟨comm, π⟩, and E ∈ ⟨explike, π⟩ then

C # E ⇒ while B do C # E : : π .

(5.10) If C ∈ ⟨comm, [π | ι: τ τ var]⟩ and E ∈ ⟨explike, π⟩ and ι ∉ dom(π) then

(∀ι: τ τ var)(ι # E ⇒ C # E) ⇒ (new τ var ι in C) # E : : π .

We now want to derive a general inference rule that subsumes all of the previous rules and equivalences for leftside noninterference decomposition. As a preliminary we must define, for any command-like phrase C, a subset F_{commlike}(C) of the identifiers occurring free in C. Let C ∈ ⟨commlike, π⟩. Then F_{commlike}(C) ⊆ {ι | ι ∈ dom(π) and π(ι) ≤ commlike} is the set of identifiers such that:

(a) If C is an identifier ι then

F_{commlike}(C) = {ι}

(b) If C is C_{1}(C_{2}) then there must be one or more pairs θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ commlike, C_{1} ∈ ⟨θ_{1} → θ_{2}, π⟩, and C_{2} ∈ ⟨θ_{1}, π⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ commlike then

F_{commlike}(C) = F_{commlike}(C_{1})

(ii) Otherwise,

F_{commlike}(C) = F_{commlike}(C_{1}) ∪ F_{commlike}(C_{2}) .

(c) If C is λι: θ. C_{1} then

F_{commlike}(C) = F_{commlike}(C_{1}) − {ι} .

(d) If C is rec C_{1} then

F_{commlike}(C) = F_{commlike}(C_{1}) .

(e) If C is ⊥_{ρ} then

F_{commlike}(C) = {} .

(f) If C is if B then C_{1} else C_{2} then

F_{commlike}(C) = F_{commlike}(C_{1}) ∪ F_{commlike}(C_{2}) .

(g) If C is let ι be C_{1} in C_{2} then there must be at least one pair θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ commlike, C_{1} ∈ ⟨θ_{1}, π⟩, and C_{2} ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ commlike then

F_{commlike}(C) = F_{commlike}(C_{2}) − {ι} .

(ii) Otherwise,

F_{commlike}(C) = F_{commlike}(C_{1}) ∪ (F_{commlike}(C_{2}) − {ι}) .

(h) If C is letrec ι: ρ be C_{1} in C_{2} then

F_{commlike}(C) = (F_{commlike}(C_{1}) ∪ F_{commlike}(C_{2})) − {ι} .

(i) If C is skip then

F_{commlike}(C) = {} .

(j) If C is C_{1} := C_{2} then

F_{commlike}(C) = F_{commlike}(C_{1}) .

(k) If C is C_{1}; C_{2} then

F_{commlike}(C) = F_{commlike}(C_{1}) ∪ F_{commlike}(C_{2}) .

(l) If C is while B do C_{1} then

F_{commlike}(C) = F_{commlike}(C_{1}) .

(m) If C is new τ var ι in C_{1} then

F_{commlike}(C) = F_{commlike}(C_{1}) − {ι} .

This definition is the key to the following derived rule of inference:

(5.11) Leftside Noninterference Decomposition. Suppose that C ∈ ⟨commlike, π⟩, E ∈ ⟨explike, π⟩, and F_{commlike}(C) = {ι_{1}, …, ι_{n}}. Then

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C # E : : π .

The proof of this rule is considerably more complex than that of the derived rules encountered previously. To begin with, we will assume that no identifier bound in C belongs to dom(π); this restriction can always be met by renaming the bound identifiers of C, which changes neither the meaning of C nor F_{commlike}(C). With this restriction, the proof is by structural induction on C, with cases that parallel the definition of F_{commlike}:

(a) If C is an identifier ι then F_{commlike}(C) = {ι}, so that the specification to be proved is

ι # E ⇒ ι # E : : π ,

which follows from the fact that any specification implies itself.

(b) If C is C_{1}(C_{2}) then there must be one or more pairs θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ commlike, C_{1} ∈ ⟨θ_{1} → θ_{2}, π⟩, and C_{2} ∈ ⟨θ_{1}, π⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ commlike then F_{commlike}(C_{1}) = F_{commlike}(C), so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1} # E : : π .

But equivalence (5.2) gives

C_{1} # E ⇒ (∀ι: θ_{1})C_{1}(ι) # E : : π ,

where ι is some identifier not in dom(π), and quantifier removal gives

(∀ι: θ_{1})C_{1}(ι) # E ⇒ C_{1}(C_{2}) # E : : π .

Thus by modus ponens,

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1}(C_{2}) # E : : π .

(ii) Otherwise, F_{commlike}(C_{1}) ⊆ F_{commlike}(C) and F_{commlike}(C_{2}) ⊆ F_{commlike}(C), so that the induction hypothesis gives (with added assumptions)

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1} # E : : π ,
ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{2} # E : : π .

But equivalence (5.3) gives

C_{1} # E ⇒ (∀ι: θ_{1})(ι # E ⇒ C_{1}(ι) # E) : : π ,

where ι is some identifier not in dom(π), and quantifier removal gives

(∀ι: θ_{1})(ι # E ⇒ C_{1}(ι) # E) ⇒ (C_{2} # E ⇒ C_{1}(C_{2}) # E) : : π .

Thus

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1}(C_{2}) # E : : π .

(c) If C is λι: θ. C_{1} then

(i) If θ ≰ commlike then F_{commlike}(C_{1}) = F_{commlike}(C), since ι cannot belong to F_{commlike}(C_{1}), so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1} # E : : [π | ι: θ] .

Then quantifier introduction and reverse beta reduction give

ι_{1} # E &⋯ & ι_{n} # E ⇒ (∀ι: θ)(λι: θ. C_{1})(ι) # E : : π

since ι occurs bound in C and therefore does not belong to dom(π). But equivalence (5.2) gives

(∀ι: θ)(λι: θ. C_{1})(ι) # E ⇒ (λι: θ. C_{1}) # E : : π .

Thus

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (λι: θ. C_{1}) # E : : π .

(ii) If θ ≤ commlike then F_{commlike}(C_{1}) ⊆ F_{commlike}(C) ∪ {ι}, so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E & ι # E ⇒ C_{1} # E : : [π | ι: θ].

Then quantifier introduction and reverse beta reduction give

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (∀ι: θ)(ι # E ⇒ (λι: θ. C_{1})(ι) # E) : : π

since ι occurs bound in C and therefore does not belong to dom(π). But equivalence (5.3) gives

(∀ι: θ)(ι # E ⇒ (λι: θ. C_{1})(ι) # E) ⇒ (λι: θ. C_{1}) # E : : π .

Thus

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (λι: θ. C_{1}) # E : : π .

(d) If C is rec C_{1} then F_{commlike}(C_{1}) = F_{commlike}(C), so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1} # E : : π .

Then rule (5.4) gives

C_{1} # E ⇒ rec C_{1} # E : : π ,

and the result follows by modus ponens.

(e) If C is ⊥_{ρ} then F_{commlike}(C) = {}, so that the specification to be proved is

⊥_{ρ} # E : : π ,

which follows from rule (5.5).

(f) If C is if C_{1} then C_{2} else C_{3} then F_{commlike}(C_{2}) ⊆ F_{commlike}(C) and F_{commlike}(C_{3}) ⊆ F_{commlike}(C), so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{2} # E : : π ,
ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{3} # E : : π .

Then rule (5.6) gives

C_{2} # E & C_{3} # E ⇒ if C_{1} then C_{2} else C_{3} # E : : π ,

and the result follows by modus ponens.

(g) If C is let ι be C_{1} in C_{2} then there must be at least one pair θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ commlike, C_{1} ∈ ⟨θ_{1}, π⟩, and C_{2} ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ commlike, then F_{commlike}(C) = F_{commlike}(C_{2}) − {ι} = F_{commlike}(λι: θ_{1}. C_{2}) = F_{commlike}((λι: θ_{1}. C_{2})(C_{1})). Then the argument for (b) and (c) shows that

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (λι: θ_{1}. C_{2})(C_{1}) # E : : π ,

and the result follows from the defining equivalence (3.8) for let. (ii) Otherwise, F_{commlike}(C) = F_{commlike}(C_{1}) ∪(F_{commlike}(C_{2})−{ι}) = F_{commlike}(C_{1}) ∪

F_{commlike}(λι: θ_{1}. C_{2}) = F_{commlike}((λι: θ_{1}. C_{2})(C_{1})). Again the argument for (b) and (c) shows that

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (λι: θ_{1}. C_{2})(C_{1}) # E : : π ,

and the result follows from the defining equivalence (3.8) for let.

(h) If C is letrec ι: ρ be C_{1} in C_{2} then F_{commlike}(C) = (F_{commlike}(C_{1})∪F_{commlike}(C_{2}))−{ι} = F_{commlike}(λι: ρ. C_{1}) ∪ F_{commlike}(λι: ρ. C_{2}) = F_{commlike}((λι: ρ. C_{2})(rec λι: ρ. C_{1})). Then the argument for (b), (c), and (d) shows that

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (λι: ρ. C_{2})(rec λι: ρ. C_{1}) # E : : π ,

and the result follows from the defining equivalence (3.9) for letrec.

(i) If C is skip, then the result follows from rule (5.7) by an argument similar to (e).

(j) If C is C_{1} := C_{2} then F_{commlike}(C_{1}) = F_{commlike}(C), so that the induction hypothesis

gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ C_{1} # E : : π .

But equivalence (5.1) gives

C_{1} # E ⇒ (∀ι: τ exp)(C_{1} := ι # E) : : π ,

where ι is some identifier not in dom(π), and quantifier removal gives

(∀ι: τ exp)(C_{1} := ι # E) ⇒ C_{1} := C_{2} # E : : π .

The result follows by modus ponens.

(k) If C is C_{1}; C_{2} then the result follows from rule (5.8) by an argument similar to (f).

(l) If C is while C_{1} do C_{2} then the result follows from rule (5.9) by an argument similar to (d).

(m) If C is new τ var ι in C_{1}, then F_{commlike}(C_{1}) ⊆ F_{commlike}(C) ∪ {ι}, so that the induction hypothesis gives

ι_{1} # E & ⋯ & ι_{n} # E & ι # E ⇒ C_{1} # E : : [π | ι: τ τ var] .

Then quantifier introduction gives

ι_{1} # E & ⋯ & ι_{n} # E ⇒ (∀ι: τ τ var)(ι # E ⇒ C_{1} # E) : : π

since ι occurs bound in C and therefore does not belong to dom(π). But rule (5.10) gives

(∀ι: τ τ var)(ι # E ⇒ C_{1} # E) ⇒ (new τ var ι in C_{1}) # E : : π ,

so that the result follows by modus ponens.

6. Rightside Noninterference Decomposition

The development of rightside decomposition parallels that of the previous section. We begin with equivalences that define noninterference for function procedures. If θ_{1} ≰ explike, θ_{2} ≤ explike, C ∈ ⟨commlike, π⟩, H ∈ ⟨θ_{1} → θ_{2}, π⟩, and ι ∉ dom(π), then

C # H ≡_{spec,π} (∀ι: θ_{1})C # H(ι) .  (6.1)

On the other hand, if θ_{1} ≤ explike, θ_{2} ≤ explike, C ∈ ⟨commlike, π⟩, H ∈ ⟨θ_{1} → θ_{2}, π⟩, and ι ∉ dom(π), then

C # H ≡_{spec,π} (∀ι: θ_{1})(C # ι ⇒ C # H(ι)) .  (6.2)

Next we give basic decomposition rules for a variety of constructs in the language:

(6.3) If θ ≤ explike, C ∈ ⟨commlike, π⟩, B ∈ ⟨Boolean exp, π⟩, and E_{1}, E_{2} ∈ ⟨θ, π⟩, then

C # B & C # E_{1} & C # E_{2} ⇒ C # if B then E_{1} else E_{2} : : π .

(6.4) If C ∈ ⟨commlike, π⟩ then

C # 0 : : π ,
C # 1 : : π ,
C # 0.5 : : π ,
C # true : : π .

(6.5) If C ∈ ⟨commlike, π⟩ and E_{1}, E_{2} ∈ ⟨integer exp, π⟩ (or ⟨real exp, π⟩ or ⟨Boolean exp, π⟩)

then

C # E_{1} & C # E_{2} ⇒ C # E_{1} + E_{2} : : π ,
C # E_{1} & C # E_{2} ⇒ C # E_{1} = E_{2} : : π ,
C # E_{1} & C # E_{2} ⇒ C # E_{1} and E_{2} : : π .

(6.6) If C ∈ ⟨commlike, π⟩, E ∈ ⟨Boolean exp, [π | ι: integer exp]⟩, and ι ∉ dom(π), then

(∀ι: integer exp)(C # ι ⇒ C # E) ⇒ C # (∀ι) E : : π .

Then we define, for any expression-like phrase E, a subset F_{explike}(E) of the identifiers occurring free in E. Let E ∈ ⟨explike, π⟩. Then

F_{explike}(E) ⊆ {ι | ι ∈ dom(π) and π(ι) ≤ explike}

is the set of identifiers such that:

(a) If E is an identifier ι then

F_{explike}(E) = {ι}.

(b) If E is E_{1}(E_{2}) then there must be one or more pairs θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ explike, E_{1} ∈ ⟨θ_{1} → θ_{2}, π⟩, and E_{2} ∈ ⟨θ_{1}, π⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ explike then

F_{explike}(E) = F_{explike}(E_{1}) .

(ii) Otherwise,

F_{explike}(E) = F_{explike}(E_{1}) ∪ F_{explike}(E_{2}) .

(c) If E is λι: θ. E_{1} then

F_{explike}(E) = F_{explike}(E_{1}) − {ι} .

(d) If E is if B then E_{1} else E_{2} then

F_{explike}(E) = F_{explike}(B) ∪ F_{explike}(E_{1}) ∪ F_{explike}(E_{2}) .

(e) If E is let ι be E_{1} in E_{2} then there must be at least one pair θ_{1}, θ_{2} of phrase types such that θ_{2} ≤ explike, E_{1} ∈ ⟨θ_{1}, π⟩, and E_{2} ∈ ⟨θ_{2}, [π | ι: θ_{1}]⟩.

(i) If there is any such θ_{1} for which θ_{1} ≰ explike then F_{explike}(E) = F_{explike}(E_{2}) − {ι} .

(ii) Otherwise, F_{explike}(E) = F_{explike}(E_{1}) ∪ (F_{explike}(E_{2}) − {ι}) .

(f) If E is 0, 1, 0.5, or true, then

F_{explike}(E) = {} .

(g) If E is E_{1} + E_{2}, E_{1} = E_{2}, or E_{1} and E_{2}, then

F_{explike}(E) = F_{explike}(E_{1}) ∪ F_{explike}(E_{2}) .

(h) If E is (∀ι)E_{1} then

F_{explike}(E) = F_{explike}(E_{1}) − {ι} .

Finally, we give a general derived rule for rightside decomposition:

(6.7) Rightside Noninterference Decomposition. Suppose C ∈ ⟨commlike, π⟩, E ∈ ⟨explike, π⟩, and F_{explike}(E) = {ι_{1}, …, ι_{n}}. Then

C # ι_{1} & ⋯ & C # ι_{n} ⇒ C # E : : π .

We omit the proof, which is similar in style and tedium to that in the previous section.

7. Assignment and Simple Variable Declaration

To treat assignment, we begin with an equivalence that defines “good variable” specifications: If V ∈ ⟨τ τ var, π⟩ and ι and ι′ are distinct identifiers not belonging to dom(π), then

gv_{τ}(V) ≡_{spec,π} (∀ι: τ exp)(∀ι′: τ exp → Boolean exp) (V # ι′ ⇒ {ι′(ι)} V := ι {ι′(V)}) .  (7.1)

From this equivalence it is straightforward to derive an inference rule for assignment statements:

(7.2) Assignment. Let V ∈ ⟨τ τ var, π⟩, E ∈ ⟨τ exp, π⟩, P ∈ ⟨Boolean exp, [π | ι: τ exp]⟩, and F_{explike}(P) − {ι} = {ι_{1}, …, ι_{n}}. By quantifier removal, using the substitution ι, ι′ → E, λι: τ exp. P, we have

(∀ι: τ exp)(∀ι′: τ exp → Boolean exp) (V # ι′ ⇒ {ι′(ι)} V := ι {ι′(V)})

⇒ (V # λι: τ exp. P ⇒ {(λι: τ exp. P)(E)} V := E {(λι: τ exp. P)(V)}) : : π .

Next beta reduction and rightside noninterference decomposition give

(∀ι: τ exp)(∀ι′: τ exp → Boolean exp) (V # ι′ ⇒ {ι′(ι)} V := ι {ι′(V)})

⇒ (V # ι_{1} & ⋯ & V # ι_{n} ⇒ {P |_{ι→E}} V := E {P |_{ι→V} }) : : π

since F_{explike}(λι: τ exp. P) = {ι_{1}, …, ι_{n}}. Then equivalence (7.1) gives the conclusion

gv_{τ}(V) & V # ι_{1} & ⋯ & V # ι_{n} ⇒ {P |_{ι→E}} V := E {P |_{ι→V} } : : π .

In the special case where V = ι, this rule reduces to the simple assignment rule (R24) in [8], which says that Hoare-like reasoning about an assignment to ι requires ι to be a good variable that does not interfere with any other identifier with a free expression-like occurrence in P. In the simplest case, where ι is declared to be a simple variable, these assumptions will be assured by its declaration. Simple variable declarations are described by the following family of axioms:

(7.3) Simple Variable Declaration Axiom. Let π be a type assignment that maps e_{1}, …, e_{m} into explike, c_{1}, …, c_{n} into commlike, p, q into Boolean exp, and h into τ τ var → comm. Then

(∀x: τ τ var) \begin{matrix}(gv_{τ}(x) & x # e_{1} & ⋯ & x # e_{m} & c_{1} # x & ⋯ & c_{n} # x \\ ⇒ \{p\} h(x) \{q\}) \end{matrix}

⇒ {p} new τ var x in h(x) {q} : : π .

From this axiom we can derive a less abstract rule akin to (R25) in [8]:

(7.4) Simple Variable Declaration Rule. Suppose S ∈ ⟨spec, π⟩, E_{1},…, E_{m} ∈ ⟨explike, π⟩, C_{1},…, C_{n} ∈ ⟨commlike, π⟩, P, Q ∈ ⟨Boolean exp, π⟩, B ∈ ⟨comm, [π | ι: τ τ var]⟩, and ι ∉ dom(π) are such that

\begin{matrix}S & gv_{τ}(ι) & ι # E_{1} & ⋯ & ι # E_{m} & C_{1} # ι & ⋯ & C_{n} # ι \\ ⇒ \{P \} B \{Q\} : : [π | ι: τ τ var] . \end{matrix}

By quantifier introduction we have

S ⇒ (∀ι: τ τ var)
gv_{τ}(ι) & ι # E_{1} & ⋯ & ι # E_{m} & C_{1} # ι & ⋯ & C_{n} # ι
⇒ {P } B {Q} : : π .

In Axiom (7.3) we rename x to be ι (which can be assumed without loss of generality to be distinct from the identifiers occurring free in the axiom), and use the free substitution

e_{1}, …, e_{m} → E_{1}, …, E_{m}

c_{1}, …, c_{n} → C_{1}, …, C_{n}

p, q → P, Q

h → λι: τ τ var. B

to obtain

(∀ι: τ τ var) \begin{matrix}(gv_{τ}(ι) & ι # E_{1} & ⋯ & ι # E_{m} & C_{1} # ι & ⋯ & C_{n} # ι \\ ⇒ \{P \} (λι: τ τ var. B)(ι) \{Q\}) \end{matrix}

⇒ {P } new τ var ι in (λι: τ τ var. B)(ι) {Q} : : π .

Then, after beta-reducing the two redexes and using modus ponens, we obtain the conclusion

S ⇒ {P } new τ var ι in B {Q} : : π .

At this point, the reader may wonder if it is possible for a variable not to be good. An example is provided by the conditional variable

if m = 1 then m else n ,

where m and n are good integer variables. For a state where m = 1 and n = 2, the assignment

(if m = 1 then m else n) := 3

produces a state in which

(if m = 1 then m else n) = 2 .

Thus gv_{integer}(if m = 1 then m else n) is false. (Another example of a bad variable, discussed in [8], is a self-subscripting array such as X(X(1)).)

The seriousness of the bad variable problem arises from the fact that such a variable can be used as an actual parameter in a procedure call, where call by name implies that its abnormal behavior is inherited by the corresponding formal parameter.

8. let Commands and Function Procedures

We now consider the let construction, which can be used to define nonrecursive procedures. First we derive a rule for commands of the form let ι be M in B.

(8.1) let Commands. Suppose ι ∉ dom(π)

S ∈ ⟨spec, π⟩
S_{proc} ∈ ⟨spec, [π | ι: θ]⟩
P, Q ∈ ⟨Boolean exp, π⟩
B ∈ ⟨comm, [π | ι: θ]⟩
M ∈ ⟨θ, π⟩

are such that

S ⇒ (S_{proc}|_{ι→M}) : : π , (a)

S & S_{proc} ⇒ {P } B {Q} : : [π | ι: θ] . (b)

From (b), reverse beta reduction gives

S & S_{proc} ⇒ {P } (λι: θ. B)(ι) {Q} : : [π | ι: θ] ,

and free substitution gives

S & (S_{proc}|_{ι→M}) ⇒ {P } (λι: θ. B)(M) {Q} : : π

since ι does not occur free in S, P, Q, or the lambda expression. Then modus ponens with (a) gives

S ⇒ {P } (λι: θ. B)(M) {Q} : : π ,

and the equivalence (3.8) defining let gives the conclusion

S ⇒ {P } let ι be M in B {Q} : : π .

From this rule, one can derive more specific rules for nonrecursive proper and function procedure declarations. We limit our discussion to the latter, since the former is less interesting than the recursive case that will be considered later. For function procedures, however, only the nonrecursive case can be treated by specification logic. The following is a derivation of a rule similar to (R36′) in [8]. (The notation π⌉S denotes the restriction of π to S.)

(8.2) Nonrecursive Function Procedure Declaration. Suppose (for some n ≥ 0)

θ = θ_{1} → (⋯ → (θ_{n} → τ exp) ⋯)

ι, ι_{1}, …, ι_{n} are distinct identifiers

ι ∉ dom(π)

π′ = π⌉(dom(π) − {ι_{1}, …, ι_{n}})

π′′ = [π′ | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}]

S ∈ ⟨spec, π⟩

P, Q ∈ ⟨Boolean exp, π⟩

B_{proc} ∈ ⟨τ exp, π′′⟩

B ∈ ⟨comm, [π | ι: θ]⟩

{ι′′_{1}, …, ι′′_{m}} = F_{explike}(B_{proc}) − {ι_{1}, …, ι_{n}} ⊆ dom(π′)

ι_{c} ∉ {ι} ∪ dom(π′)

S_{proc} = (∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n}) {ι(ι_{1}) ⋯ (ι_{n}) = B_{proc}}
& (∀ι_{c}: commlike)(ι_{c} # ι′′_{1} & ⋯ & ι_{c} # ι′′_{n} ⇒ ι_{c} # ι)
∈ ⟨spec, [π′ | ι: θ]⟩ ,

and that

S & S_{proc} ⇒ {P } B {Q} : : [π | ι: θ] . (a)

Let M be λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} ∈ ⟨θ, π′⟩. When M is substituted for ι in S_{proc}, there is no renaming since ι_{1}, …, ι_{n} and ι_{c} do not occur free in M, and B_{proc} and ι′′_{1}, …, ι′′_{m} remain unchanged since they do not contain free occurrences of ι. Moreover, M(ι_{1}) ⋯ (ι_{n}) beta-reduces to B_{proc}. Thus S_{proc}|_{ι→M} ∈ ⟨spec, π′⟩ is

(∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n}) {B_{proc} = B_{proc}} & (∀ι_{c}: commlike)
(ι_{c} # ι′′_{1} & ⋯ & ι_{c} # ι′′_{m} ⇒ ι_{c} # λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc}),

which is universal for π′ since B_{proc} = B_{proc} is a mathematical fact and

ι_{c} # ι′′_{1} & ⋯ & ι_{c} # ι′′_{m} ⇒ ι_{c} # λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc}
: : [π′ | ι_{c}: commlike]

is a consequence of rightside noninterference decomposition along with the fact that F_{explike}(λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc}) = {ι′′_{1}, …, ι′′_{m}}. Broadening π′ to π and adding the assumption S gives

S ⇒ (S_{proc}|_{ι→M}) : : π . (b)

Then from (a) and (b) the rule (8.1) for let commands can be used to infer the conclusion

S ⇒ {P } let ι be λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} in B {Q} : : π .

9. Recursion

To encompass recursion, we must give basic rules for the operator rec and the constant ⊥. The behavior of ⊥ is described by

(9.1) Nontermination of ⊥. If P, Q ∈ ⟨Boolean exp, π⟩ then

{P } ⊥_{comm} {Q} : : π ,

along with equivalences (3.4) and (3.5), and inference rule (5.5).

Before giving a rule for the recursion operator rec, we must define, for any specification S, two subsets of the identifiers occurring free in S. If S ∈ ⟨spec, π⟩, we define F_{−}(S) and F_{+}(S) ⊆ dom(π) by

F_{−}({P } C {Q}) = {}  F_{+}({P } C {Q}) = F_{commlike}(C)
F_{−}({P }) = {}  F_{+}({P }) = {}
F_{−}(C # E) = {}  F_{+}(C # E) = F_{commlike}(C)
F_{−}(S & S′) = F_{−}(S) ∪ F_{−}(S′) F_{+}(S & S′) = F_{+}(S) ∪ F_{+}(S′)
F_{−}(S ⇒ S′) = F_{+}(S) ∪ F_{−}(S′) F_{+}(S ⇒ S′) = F_{−}(S) ∪ F_{+}(S′)
F_{−}((∀ι: θ)S) = F_{−}(S) − {ι}  F_{+}((∀ι: θ)S) = (F_{+}(S) ∪ F_{−}(S)) − {ι}

These sets reflect the semantic concept of continuity:

(1) If ι ∉ F_{−}(S) then the meaning of S, ordered by true ⊑ false, is continuous in the meaning of ι.

(2) If ι ∉ F_{+}(S) then the meaning of S, ordered by false ⊑ true, is continuous in the meaning of ι.

The asymmetric equations for quantified specifications reflect the fact that universal quantification preserves the first kind of continuity but not the second.

Consider F ∈ ⟨ρ → ρ, π⟩. Suppose some property holds for ⊥_{ρ} and, whenever this property holds for ι, it holds for F (ι). Then the property holds for each member of the sequence ⊥_{ρ}, F (⊥_{ρ}), F (F (⊥_{ρ})), …. Moreover, rec F can be regarded as the limit of this sequence, so that if the property is appropriately continuous—in the sense of (1) above—it will hold for rec F.

This reasoning is formalized by the following rule for rec, in which the property is expressed by a specification S regarded as a function of ι:

(9.2) Recursion. Suppose F ∈ ⟨ρ → ρ, π⟩, S ∈ ⟨spec, [π | ι: ρ]⟩, ι ∉ dom(π), and ι ∉ F_{−}(S).

Then

(S|_{ι→⊥_{ρ}}) & (∀ι: ρ)(S ⇒ (S|_{ι→F (ι)})) ⇒ (S|_{ι→rec F}) : : π .

It is illuminating to give an example showing the necessity of the condition ι ∉ F_{−}(S). Such an example can be developed from the fact that certain recursive procedures always terminate even though none of their “finite approximations” always terminate. Under the type assignment [p: integer exp → comm | x: integer exp]:

{true}p(x){false} specifies p does not terminate for x.

{true}p(x){false} ⇒ {false} specifies that p terminates for x.

(∀x: integer exp)({true}p(x){false} ⇒ {false}) specifies that p always terminates.

S = (∀x: integer exp)({true}p(x){false} ⇒ {false}) ⇒ {false} specifies that p does not always terminate.

Even though S holds for all finite approximations to p, it may fail to hold for the limit. This is possible since p ∈ F_{−}(S) and, in fact, the meaning of S, ordered by true ⊑ false, is not continuous in the meaning of p.

In formalizing this example, it will be convenient to use the following derived rule about the operation ⇒:

(9.3) Reversal. Suppose S_{1}, S_{2}, S_{3} ∈ ⟨spec, π⟩ and

S_{1} ⇒ S_{2} : : π .

From (3.25)

(S_{2} ⇒ S_{3}) ⇒ (S_{2} ⇒ S_{3}) : : π ,

so by (3.26) and (3.20)

S_{2} ⇒ ((S_{2} ⇒ S_{3}) ⇒ S_{3}) : : π ,

and by modus ponens

S_{1} ⇒ ((S_{2} ⇒ S_{3}) ⇒ S_{3}) : : π .

Then (3.26) and (3.20) give the conclusion

(S_{2} ⇒ S_{3}) ⇒ (S_{1} ⇒ S_{3}) : : π .

It will also simplify the argument to assume, for the duration of this example, that the values of integer expressions range over the natural numbers (excluding negative numbers). Thus x + 1 = 0 implies false is a mathematical fact for [x: integer exp].

Let F = λp: integer exp → comm. λx: integer exp. if x = 0 then skip else p(x − 1)

and π = [p: integer exp → comm | x: integer exp] .

Then {false}skip{false} : : π (4.17) {x + 1 = 0}skip{false} : : π (4.13) {true}p(x){false} ⇒ {true}p((x + 1) − 1){false} : : π (4.1) {true}p(x){false} ⇒ {¬x + 1 = 0} p((x + 1) − 1){false} : : π (4.13) {true}p(x){false} ⇒ {true}F (p)(x + 1){false} : : π (4.16, 3.1) ({true}F (p)(x + 1){false} ⇒ {false})

⇒ ({true}p(x){false} ⇒ {false}) : : π (9.3) (∀x: integer exp)({true}F (p)(x){false} ⇒ {false})

⇒ ({true}F (p)(x + 1){false} ⇒ {false}) : : π (4.8) (∀x: integer exp)({true}F (p)(x){false} ⇒ {false})

⇒ ({true}p(x){false} ⇒ {false}) : : π (4.6) (∀x: integer exp)({true}F (p)(x){false} ⇒ {false})

⇒ (∀x: integer exp)({true}p(x){false} ⇒ {false})

: : [p: integer exp → comm] (4.7) S ⇒ (S|_{p→F (p)}) : : [p: integer exp → comm] (9.3) (∀p: integer exp → comm)(S ⇒ (S|_{p→F (p)})) : : [ ] (4.7) {true} ⊥_{comm} false} : : [ ] (9.1) {true} ⊥_{integer exp→comm} (x){false} : : [x: integer exp] (3.4) (∀x: integer exp)({true} ⊥_{integer exp→comm} (x){false} ⇒ {false})

⇒ ({true} ⊥_{integer exp→comm} (x) {false} ⇒ {false})

: : [x: integer exp] (4.8) {true} ⊥_{integer exp→comm} (x){false} ⇒ (S|_{p→⊥_{integer exp→comm}})

: : [x: integer exp] (3.26, 3.20) S|_{p→⊥_{integer exp→comm}} : : [x: integer exp] (4.6) S|_{p→⊥_{integer exp→comm}} : : [ ] (4.3)

Now consider the recursion rule, taking ρ to be integer exp → comm, π to be the empty type assignment [ ], ι to be p, and S and F as above. In the absence of the restriction p ∉ F_{−}(S), one could infer

S|_{p→rec F} : : [ ]

But this is false, since in fact rec F always terminates.

10. letrec Commands and Proper Procedures From the rules in the previous section, we can derive a rule for letrec commands and a more specific rule for proper procedure declarations. (10.1) letrec Commands. Suppose

ι ∉ dom(π) S ∈ ⟨spec, π⟩ S_{proc} ∈ ⟨spec, [π | ι: ρ]⟩ P, Q ∈ ⟨Boolean exp, π⟩ B ∈ ⟨comm, [π | ι: ρ]⟩ M ∈ ⟨ρ, [π | ι: ρ]⟩ ι ∉ F_{−}(S_{proc})

are such that S ⇒ (S_{proc}|_{ι→⊥_{ρ}}) : : π (a) S & S_{proc} ⇒ (S_{proc}|_{ι→M}) : : [π | ι : ρ] (b) S & S_{proc} ⇒ {P } B {Q} : : [π | ι : ρ] . (c)

From (b), by backwards beta reduction, we have

S & S_{proc} ⇒ (S_{proc}|_{ι→(λι:ρ.M)(ι)}) : : [π | ι : ρ] , so that introducing a quantifier gives

S ⇒ (∀ι: ρ)(S_{proc} ⇒ (S_{proc}|_{ι→(λι:ρ.M)(ι)})) : : π . (d) From the recursion rule (9.2), replacing S by S_{proc} and F by λι: ρ. M, we get

(S_{proc}|_{ι→⊥_{ρ}}) & (∀ι: ρ)(S_{proc} ⇒ (S_{proc}|_{ι→(λι:ρ.M)(ι)}))

⇒ (S_{proc}|_{ι→rec λι:ρ.M}) : : π ,

which, by modus ponens with (a) and (d), gives

S ⇒ (S_{proc}|_{ι→rec λι:ρ.M}) : : π . (e) By backwards beta reduction in (c), we have

S & S_{proc} ⇒ {P } (λι: ρ. B)(ι) {Q} : : [π | ι: ρ] . Then, since ι does not occur free in S, P, λι: ρ. B, or Q, free substitution gives S & (S_{proc}|_{ι→rec λι:ρ.M})

⇒ {P } (λι: ρ. B)(rec λι: ρ. M) {Q} : : π ,

and modus ponens with (e), along with the equivalence (3.9) defining letrec, gives the conclusion

S ⇒ {P } letrec ι: ρ be M in B {Q} : : π .

From (10.1) we can derive the following more specific rule, which is similar to (R26) in [8]:

(10.2) Proper Procedure Declaration. Suppose that (for some n, k ≥ 0)

ρ = (θ_{1} → ⋯ (θ_{n} → comm) ⋯)

ι, ι_{1}, …, ι_{n}, ι′_{1}, …, ι′_{k} are distinct identifiers

ι ∉ dom(π)

π′ = π⌉ (dom(π) − {ι_{1}, … ι_{n}, ι′_{1}, … ι′_{k}})

π′′ = [π′ | ι_{1}: θ_{1} | ⋯ | ι_{n}: θ_{n}]

π′′′ = [π′′ | ι′_{1}: θ′_{1} | ⋯ | ι′_{k}: θ′_{k}]

S_{1} ∈ ⟨spec, π′⟩

S_{pa} ∈ ⟨spec, π′′′⟩

S_{2} ∈ ⟨spec, π⟩

P_{proc}, Q_{proc} ∈ ⟨Boolean exp, π′′′⟩

P, Q ∈ ⟨Boolean exp, π⟩

B_{proc} ∈ ⟨comm, [π′′ | ι: ρ]⟩

B ∈ ⟨comm, [π | ι: ρ]⟩

{ι′′_{1}, …, ι′′_{m}} = F_{commlike}(B_{proc}) − {ι, ι_{1}, …, ι_{n}} ⊆ dom(π′)

ι_{e} ∉ {ι} ∪ dom(π′)

S_{proc} = (∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n})(∀ι′_{1}: θ′_{1}) ⋯ (∀ι′_{k}: θ_{k})
(S_{pa} ⇒ {P_{proc}} ι(ι_{1}) ⋯ (ι_{n}) {Q_{proc}})
& (∀ι_{e}: explike)(ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e} ⇒ ι # ι_{e})
∈ ⟨spec, [π′ | ι: ρ]⟩

and that

S_{1} & S_{proc} & S_{pa} ⇒ {P_{proc}} B_{proc} {Q_{proc}} : : [π′′′ | ι: ρ] (a)

S_{2} & S_{proc} ⇒ {P } B {Q} : : [π | ι: ρ] . (b)

Let M be λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} ∈ ⟨ρ, [π′ | ι: ρ]⟩. When M is substituted for ι in S_{proc}, there is no renaming since ι_{1}, …, ι_{n}, ι′_{1}, …, ι′_{k}, and ι_{e} do not occur free in M, and S_{pa}, P_{proc}, Q_{proc}, ι′′_{1}, …, ι′′_{m} remain unchanged since they do not contain free occurrences of ι. Moreover, M(ι_{1}) ⋯ (ι_{n}) beta-reduces to B_{proc}. Thus S_{proc}|_{ι→M} ∈ ⟨spec, [π′ | ι: ρ]⟩ is

(∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n})(∀ι′_{1}: θ′_{1}) ⋯ (∀ι′_{k}: θ_{k})
(S_{pa} ⇒ {P_{proc}} B_{proc} {Q_{proc}})
& (∀ι_{e}: explike)
(ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e} ⇒ λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} # ι_{e}) .

By introducing quantifiers into (a), we have

S_{1} & S_{proc} ⇒ (∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n})(∀ι′_{1}: θ′_{1}) ⋯ (∀ι′_{k}: θ′_{k})

(S_{pa} ⇒ {P_{proc}} B_{proc} {Q_{proc}}) : : [π′ | ι: ρ] . (c)

Since F_{commlike}(λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc}) ⊆ {ι′′_{1}, …, ι′′_{m}, ι}, leftside noninterference decomposition gives

ι′′_{1} # ι_{e} & … & ι′′_{m} # ι_{e} & ι # ι_{e}
⇒ λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} # ι_{e} : : [π′ | ι: ρ | ι_{e}: explike],

but by quantifier removal

S_{proc} ⇒ (ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e} ⇒ ι # ι_{e}) : : [π′ | ι: ρ | ι_{e}: explike],

so that modus ponens gives

S_{proc} & ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e}
⇒ λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} # ι_{e} : : [π′ | ι: ρ | ι_{e}: explike],

and quantifier introduction gives

S_{proc} ⇒ (∀ι_{e}: explike)(ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e}

⇒ λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} # ι_{e}) : : [π′ | ι: ρ] . (d)

Then modus ponens of (c) and (d) gives

S_{1} & S_{proc} ⇒ (S_{proc}|_{ι→M}) : : [π′ | ι: ρ] . (e)

On the other hand, S_{proc}|_{ι→⊥_{ρ}} ∈ ⟨spec, π′⟩ is

\begin{matrix}(∀ι_{1}: θ_{1}) ⋯ (∀ι_{n}: θ_{n})(∀ι′_{1}: θ′_{1}) ⋯ (∀ι′_{k}: θ_{k}) \\ (S_{pa} ⇒ \{P_{proc}\} ⊥_{ρ} (ι_{1}) ⋯ (ι_{n}) \{Q_{proc}\}) \\ & (∀ι_{e}: explike)(ι′′_{1} # ι_{e} & ⋯ & ι′′_{m} # ι_{e} ⇒⊥_{ρ} # ι_{e}) : : π′′ , \end{matrix} (f)

whose universality can be inferred, by adding assumptions and introducing quantifiers, from

{P_{proc}} ⊥_{ρ}(ι_{1}) ⋯ (ι_{n}) {Q_{proc}} : : π′′′

and

⊥_{ρ} # ι_{e} : : [π′ | ι_{e}: explike] ,

which are consequences of (3.4), (9.1), and (5.5). Finally from (f), (e), and (b), broadening the type assignments to replace π′ by π, taking S to be S_{1} & S_{2}, and noting that ι ∉ F_{−}(S_{proc}), rule (10.1) for letrec commands gives the conclusion

S_{1} & S_{2} ⇒ {P } letrec ι: ρ be λι_{1}: θ_{1}…. λι_{n}: θ_{n}. B_{proc} in B {Q} : : π .

11. Some Questionable Rules of Inference

We conclude by introducing two rules of inference whose status, at this writing, is still in question. Although we have not been able to deduce a contradiction from these rules, they are not valid for the kind of semantics discussed in [8], and the problem of constructing a semantics for which they are valid has not been solved. However, they are extremely useful; indeed they—or something like them—seem to be necessary for certain aspects of program proving.

The first is a stronger version of (4.20):

(11.1) Strong Constancy. Let π be a type assignment mapping c into comm and p, q, and r into Boolean exp. Then

c # p & ({p} ⇒ {q} c {r}) ⇒ {q and p} c {r and p} : : π .

Roughly speaking, if p holds before executing c and is not interfered with by c (at any time during its execution), one can assume that it is a static assertion in reasoning about c. The difficulty is that it is not really static, i.e., there are environments for which c # p is true yet {p} is false.

The second rule is a limited kind of converse to our rule for leftside noninterference decomposition:

(11.2) Leftside Noninterference Composition. Suppose that C ∈ ⟨comm, π⟩, E ∈ ⟨explike, π⟩, P, Q ∈ ⟨Boolean exp, π⟩, and F_{commlike}(C) = {ι_{1}, …, ι_{n}}. Then

(ι_{1} # E & ⋯ & ι_{n} # E ⇒ {P } C {Q}) ⇒ (C # E ⇒ {P } C {Q}) : : π .

To see the difficulty with this rule, take π to be [k: integer integer var], C to be (λk: integer integer var. skip)(k), E to be k, P to be true, and Q to be false. Then (11.2) gives, with beta reduction of C,

(k # k ⇒ {true} skip {false}) ⇒ (skip # k ⇒ {true} skip {false}) : : π ,

which in conjunction with (5.7) gives

(k # k ⇒ {true} skip {false}) ⇒ {true} skip {false} : : π .

Clearly there are environments in which both k # k and {true} skip {false} are false, so this specification is not universal in a conventional semantics.

On the other hand, the need for a rule of this sort is illustrated by an attempt to show that

let iterate be λp: integer exp → comm.

new integer var k in

(k := 0; while k < 100 do (k := k + 1; p(k))) in (s := 0; iterate(λk: integer exp. s := s + f(k)))

will set s to ∑_{i=1}^{100} f(i).

It is a straightforward exercise to show

(∀k: integer exp)

(p(k) # k ⇒ {w(k − 1) and 1 ≤ k ≤ 100} p(k) {w(k)}) ⇒ {w(0)} new integer var k in ⋯ {w(100)}

: : [p: integer exp → comm | w: integer exp → Boolean exp]

which leads to an application of rule (10.2) with S_{proc} =

(∀p: integer exp → comm)(∀w: integer exp → Boolean exp)

((∀k: integer exp)

(p(k) # k ⇒ {w(k − 1) and 1 ≤ k ≤ 100} p(k) {w(k)}) ⇒ {w(0)} iterate(p) {w(100)})

& (∀e: explike) iterate # e .

Then by removing quantifiers, with the substitution

p → λk: integer exp. s := s + f(k)

w → λk: integer exp. s = ∑_{i=1}^{k} f(i) ,

we have (with appropriate beta reduction):

S_{proc} & (∀k: integer exp)(s := s + f(k) # k

⇒ {s = ∑_{i=1}^{k−1} f(i) and 1 ≤ k ≤ 100} s := s + f(k) {s = ∑_{i=1}^{k} f(i)})

⇒ {s = ∑_{i=1}^{0} f(i)} iterate(λk: integer exp. s := s + f(k)) {s = ∑_{i=1}^{100} f(i)}

: : π ,

where π is a type assignment that maps s into real real var, f into integer exp → real exp, and iterate into (integer exp → comm) → comm.

By the rule for assignment and well-known mathematical facts about summation, we can obtain

gv(s) & s # f ⇒ (s # k

⇒ {s = ∑_{i=1}^{k−1} f(i) and 1 ≤ k ≤ 100} s := s + f(k) {s = ∑_{i=1}^{k} f(i)}) : : π .

The need for rule (11.2) arises from the discrepancy between s # k and s := s+f(k) # k. If we can use (11.2), along with quantifier introduction, we get

gv(s) & s # f ⇒ (∀k: integer exp)(s := s + f(k) # k

⇒ {s = ∑_{i=1}^{k−1} f(i) and 1 ≤ k ≤ 100} s := s + f(k) {s = ∑_{i=1}^{k} f(i)}) : : π ,

and modus ponens gives the desired result:

S_{proc} & gv(s) & s # f ⇒
{s = ∑_{i=1}^{0} f(i)} iterate(λk: integer exp. s := s + f(k)) {s = ∑_{i=1}^{100} f(i)}
: : π .

References

[1] Hoare, C. A. R. 1969. An axiomatic basis for computer programming. Comm. ACM, 12(10):576–580 and 583.

[2] Landin, P. J. 1966. A λ-calculus approach. In Advances in Programming and Non-Numerical Computation, L. Fox, editor, Oxford. Pergamon Press, pages 97–141.

[3] Landin, P. J. 1965. A correspondence between Algol 60 and Church’s lambda-notation. Comm. ACM, 8(2,3):89–101 and 158–165.

[4] Hoare, C. A. R. 1971. Procedures and parameters: an axiomatic approach. In Symposium on Semantics of Algorithmic Languages, E. Engeler, editor, volume 188 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, pages 102–116.

[5] Hoare, C. A. R. and Wirth, N. 1973. An axiomatic definition of the programming language Pascal. Acta Informatica, 2(4):335–355.

[6] London, R. L., Guttag, J. V., Horning, J. J., Lampson, B. W., Mitchell, J. G., and Popek, G. J. 1978. Proof rules for the programming language Euclid. Acta Informatica, 10(1):1–26.

[7] Gries, D. and Levin, G. 1980. Assignment and procedure call proof rules. ACM Trans. on Programming Languages and Systems, 2(4):564–579.

[8] Reynolds, J. C. 1981a. The Craft of Programming. Prentice-Hall International, London.

[9] Wirth, N. and Hoare, C. A. R. 1966. A contribution to the development of Algol. Comm. ACM, 9(6):413–432.

[10] Reynolds, J. C. 1981b. The essence of Algol. In Algorithmic Languages, Proceedings of the International Symposium on Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, editors. North-Holland, Amsterdam, pages 345–372.