Conjoining Specifications

Martín Abadi and Leslie Lamport

3 November 1995

This is a revised version of SRC Research Report 118. It will appear in ACM Transactions on Programming Languages and Systems.

Contents

1 Introduction 507

2 An Informal Overview 508 2.1 Decomposing Complete Systems . . . . . . . . . . . . . . . . . . . . 508 2.2 Composing Open Systems . . . . . . . . . . . . . . . . . . . . . . . . 510

3 Preliminaries 513

3.1 TLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 513 3.1.1 Review of the Syntax and Semantics . . . . . . . . . . . . . . 513 3.1.2 Interleaving and Noninterleaving Representations . . . . . . . 514 3.1.3 The Queue Example . . . . . . . . . . . . . . . . . . . . . . . 515

3.2 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 516 3.3 Conditional Implementation . . . . . . . . . . . . . . . . . . . . . . . 518 3.4 Safety and Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . 518

3.4.1 Definition of Closure . . . . . . . . . . . . . . . . . . . . . . . 518 3.4.2 Machine Closure . . . . . . . . . . . . . . . . . . . . . . . . . 518 3.4.3 Closure and Hiding . . . . . . . . . . . . . . . . . . . . . . . . 519

3.5 Additional Temporal Operators . . . . . . . . . . . . . . . . . . . . . 519 3.5.1 The + Operator . . . . . . . . . . . . . . . . . . . . . . . . . 519 3.5.2 The −▷ Operator . . . . . . . . . . . . . . . . . . . . . . . . . 520

3.5.3 The −▷^{+} Operator . . . . . . . . . . . . . . . . . . . . . . . . . 520

3.5.4 The ⊥ Operator . . . . . . . . . . . . . . . . . . . . . . . . . 520

4 Decomposing a Complete Specification 521 4.1 Specifying a Component . . . . . . . . . . . . . . . . . . . . . . . . . 521 4.2 Conjoining Components to Form a Complete System . . . . . . . . . 523 4.3 The Decomposition Theorem . . . . . . . . . . . . . . . . . . . . . . 525

4.3.1 The Basic Theorem . . . . . . . . . . . . . . . . . . . . . . . 525 4.3.2 Verifying the Hypotheses . . . . . . . . . . . . . . . . . . . . 526 4.3.3 The General Theorem . . . . . . . . . . . . . . . . . . . . . . 527

5 Composing Assumption/Guarantee Specifications 528 5.1 The Form of an Assumption/Guarantee Specification . . . . . . . . . 528 5.2 The Composition Theorem . . . . . . . . . . . . . . . . . . . . . . . 529 5.3 The Queue Example . . . . . . . . . . . . . . . . . . . . . . . . . . . 530

6 Conclusion 530

Acknowledgements 532

References 532

A Definitions A–1 A1 Additional Semantic Notions . . . . . . . . . . . . . . . . . . . . . . A–1 A2 Proof Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–2 B Proofs A–2

B1 Properties of −▷ and −▷^{+} . . . . . . . . . . . . . . . . . . . . . . . . . A–2

B2 Closure and Existential Quantification . . . . . . . . . . . . . . . . . A–3 B3 Properties of + . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–5 B4 Properties of ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–10 B5 Composition as Conjunction . . . . . . . . . . . . . . . . . . . . . . . A–12 B6 Decomposition and Composition . . . . . . . . . . . . . . . . . . . . A–17

Index A–21

Conjoining Specifications

MARTÍN ABADI and LESLIE LAMPORT Digital Equipment Corporation

We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components’ specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification— correctness proofs; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—specification techniques General Terms: Theory, Verification Additional Key Words and Phrases: Composition, concurrent programming, decomposition, liveness properties, modular specification, safety properties, temporal logic

1. INTRODUCTION

Large systems are built from smaller parts. We present a method for deducing properties of a system by reasoning about its components. We show how to represent an individual component Π_{i} by a formula S_{i} so that the parallel composition usually denoted cobegin Π_{1} ∥ … ∥ Π_{n} coend is represented by the formula S_{1} ∧ … ∧ S_{n}. Composition is conjunction.

We reduce composition to conjunction not for the sake of elegance, but because it is the best way we know to prove properties of composite systems. Rigorous reasoning requires logic, and hence a language of logical formulas. It does not require a conventional programming language for describing systems. We find it most convenient to regard programs and circuit descriptions as low-level specifications, and to represent them in the same logic used for higher-level specifications. The logic we use is TLA, the Temporal Logic of Actions [Lamport 1994]. We do not discuss here the important problem of translating from a low-level TLA specification to an implementation in a conventional language.

The idea of representing concurrent programs and their specifications as formulas in a temporal logic was first proposed by Pnueli [1981]. It was later observed that, if specifications allow “stuttering” steps that leave the state unchanged, then S_{l} ⇒ S_{h} asserts that S_{l} implements S_{h} [Lamport 1983]. Hence, proving that a lower-level specification implements a higher-level one was reduced to proving a formula in

Authors’ address: Systems Research Center, Digital Equipment Corporation, 130 Lytton Avenue, Palo Alto, CA 94301. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

\begin{matrix}c \\ ◯ \end{matrix} 1995 ACM 0000-0000/95/0000-0000 $00.00

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995, Pages 507–533.

508 · Martín Abadi and Leslie Lamport

the logic. Still later, it was noticed that the formula ∃ ∃ ∃ ∃ ∃ ∃x : S specifies the same system as S except with the variable x hidden [Abadi and Lamport 1991; Lamport 1989], and variable hiding became logical quantification. The idea of composition as conjunction has also been suggested [Abadi and Plotkin 1993; Abramsky and Jagadeesan 1994; Zave and Jackson 1993], but our method for reducing composition to conjunction is new.

To deduce useful properties of a component, we must specify its environment. No component will exhibit its intended behavior in the presence of a sufficiently hostile environment. For example, a combinational circuit will not produce an output in the intended range if some input line, instead of having a 0 or a 1, has an improper voltage level of 1/2. The specification of the circuit’s environment must rule out such improper inputs.

How we reason about a composite system depends on how it was formed. Composite specifications arise in two ways: by decomposing a given system into smaller parts and by composing given parts to form a larger system. These two situations call for two methods of writing component specifications that differ in their treatment of the environment. This difference leads in turn to different proof rules.

When decomposing a specification, the environment of each component is assumed to be the other components, and is usually left implicit. To reason about a component, we must state what we are assuming about its environment, and then prove that this assumption is satisfied by the other components. The Decomposition Theorem of Section 4 provides the needed proof rule. It reduces the verification of a complex, low-level system to proving properties of a higher-level specification and properties of one low-level component at a time. Decomposing proofs in this way allows us to apply decision procedures to verifications that hitherto required completely hand-guided proofs [Kurshan and Lamport 1993].

When specifying a reusable component, without knowing precisely where it will be used, we must make explicit what it assumes of its environment. We therefore assert that the component satisfies a guarantee M only as long as its environment satisfies an assumption E. This assumption/guarantee property [Jones 1983] is denoted E −▷^{+} M. To show that a composition of reusable components satisfies a specification S, we must prove a formula of the form (E_{1} −▷^{+} M_{1}) ∧ … ∧ (E_{n} −▷^{+} M_{n}) ⇒ S, where S may again be an assumption/guarantee property. We prove such a formula with the Composition Theorem of Section 5. This theorem allows us to reason about assumption/guarantee specifications using well-established, effective methods for reasoning about specifications of complete systems.

In the following section, we examine the issues that arise in decomposition and composition. Our discussion is informal, because we wish to show that these issues are fundamental, not artifacts of a particular formalism. We treat these topics formally in Sections 4 and 5. Section 3 covers the formal preliminaries. A comparison with related work appears in the conclusion. Proofs are relegated to the appendix.

2. AN INFORMAL OVERVIEW

2.1 Decomposing Complete Systems

A complete system is one that is self-contained; it may be observed, but it does not interact with the observer. A program is a complete system, provided we model

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Conjoining Specifications · 509

inputs as being generated nondeterministically by the program itself.

As a tiny example of a complete system, we consider a program for computing a GCD (greatest common divisor), for which we have devised an informal programming-language notation. Statements within angle brackets are executed atomically; loop-endloop keywords enclose an infinite loop; cobegin-coend keywords enclose parallel statements, separated by ∥; and semicolon has its usual meaning. When writing processes, we will also mark variables as output, input, or internal; a process cannot change its input variables or access the internal variables of another process.

Program GCD var a initially 233344, b initially 233577899 ; cobegin loop ⟨ if a > b then a := a − b ⟩ endloop

∥ loop ⟨ if b > a then b := b − a ⟩ endloop coend

Program GCD satisfies the correctness property that eventually a and b become and remain equal to the gcd of 233344 and 233577899. We make no distinction between programs and properties, writing them all as TLA formulas. If formula M_{gcd} represents program GCD, and formula P_{gcd} represents the correctness property, then the program implements the property iff (if and only if) M_{gcd} implies P_{gcd}. Thus, correctness of program GCD is verified by proving M_{gcd} ⇒ P_{gcd}.

In hierarchical development, one decomposes the specification of a system into specifications of its parts. As explained in Section 4, the specification M_{gcd} of program GCD can be written as M_{a} ∧ M_{b}, where M_{a} asserts that a initially equals 233344 and is repeatedly decremented by the value of b whenever a > b, and where M_{b} is analogous. The formulas M_{a} and M_{b} are the specifications of two processes Π_{a} and Π_{b}. We can write Π_{a} and Π_{b} as

Process Π_{a} Process Π_{b} output var a initially 233344 ; output var b initially 233577899 ; input var b; input var a; loop ⟨ if a > b then a := a − b ⟩ loop ⟨ if b > a then b := b − a ⟩ endloop endloop

One decomposes a specification in order to refine the components separately. We can refine the GCD program, to remove simultaneous atomic accesses to both a and b, by refining process Π_{a} to

Process Π_{a}^{l} output var a initially 233344 ; internal var ai ; input var b; loop ⟨ ai := b ⟩; if ⟨ a > ai ⟩ then ⟨ a := a − ai ⟩ endloop

and refining Π_{b} to the analogous process Π_{b}^{l}.

The composition of processes Π_{a}^{l} and Π_{b}^{l} correctly implements program GCD. This is expressed in TLA by the assertion that M_{a}^{l} ∧ M_{b}^{l} implies M_{a} ∧ M_{b}, where M_{a}^{l} and M_{b}^{l} are the formulas representing Π_{a}^{l} and Π_{b}^{l}.

We would like to decompose the proof of M_{a}^{l} ∧ M_{b}^{l} ⇒ M_{a} ∧ M_{b} into proofs of M_{a}^{l} ⇒ M_{a} and M_{b}^{l} ⇒ M_{b}. These proofs would show that Π_{a}^{l} implements Π_{a} and that Π_{b}^{l} implements Π_{b}.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

initial state  37 sent 37 acked  4 sent 4 acked  19 sent
c.ack:  0  0  1  1  0  0  …
c.sig:  0  1  1  0  0  1  …
c.val:  −  37  37  4  4  19  …

Fig. 1. The two-phase handshake protocol for a channel c.

Unfortunately, Π_{a}^{l} does not implement Π_{a} because, in the absence of assumptions about when its input b can change, Π_{a}^{l} can behave in ways that process Π_{a} cannot. Process Π_{a} can decrement a only by the current value of b, but Π_{a}^{l} can decrement a by a previous value of b if b changes between the assignment to ai and the assignment to a. Similarly, Π_{b}^{l} does not implement Π_{b}.

Process Π_{a}^{l} does correctly implement process Π_{a} in a context in which b does not change when a > b. This is expressed in TLA by the formula E_{a} ∧ M_{a}^{l} ⇒ M_{a}, where E_{a} asserts that b does not change when a > b. Similarly, E_{b} ∧ M_{b}^{l} ⇒ M_{b} holds, for the analogous E_{b}. The Decomposition Theorem of Section 4.3 allows us to deduce M_{a}^{l} ∧ M_{b}^{l} ⇒ M_{a} ∧ M_{b} from approximately the following hypotheses:

\begin{matrix}E_{a} ∧ M_{a}^{l} ⇒ & M_{a} \\ E_{b} ∧ M_{b}^{l} ⇒ & M_{b} \\ M_{a} ∧ M_{b} ⇒ & E_{a} ∧ E_{b} \end{matrix}  (1)

The third hypothesis holds because the composition of processes Π_{a} and Π_{b} does not allow a to change when b > a or b to change when a > b.

Observe that E_{a} asserts only the property of Π_{b}^{l} needed to guarantee that Π_{a}^{l} implements Π_{a}. In a more complicated example, E_{a} will be significantly simpler than M_{b}^{l}, the full specification of Π_{b}^{l}. Verifying these hypotheses will therefore be easier than proving M_{a}^{l}∧M_{b}^{l} ⇒ M_{a}∧M_{b} directly, since this proof requires reasoning about the specification M_{a}^{l} ∧ M_{b}^{l} of the complete low-level program.

One cannot really deduce M_{a}^{l} ∧ M_{b}^{l} ⇒ M_{a} ∧ M_{b} from the hypotheses (1). For example, (1) is trivially satisfied if E_{a}, E_{b}, M_{a}, and M_{b} all equal false; but we cannot deduce M_{a}^{l} ∧ M_{b}^{l} ⇒ false for arbitrary M_{a}^{l} and M_{b}^{l}. The precise hypotheses of the Decomposition Theorem are more complicated, and we must develop a number of formal concepts in order to state them. We also develop results that allow us to discharge these more complicated hypotheses by proving conditions essentially as simple as (1).

2.2 Composing Open Systems

An open system is one that interacts with an environment it does not control. In our examples, we consider systems that communicate by using a standard twophase handshake protocol [Mead and Conway 1980] to send values over channels. The state of a channel c is described by three components: the value c.val that is being sent, and two bits c.sig and c.ack used for synchronization. We let c.snd denote the pair ⟨c.sig, c.val⟩. Figure 1 shows the sequence of states assumed in sending the sequence of values 37, 4, 19, …. The channel is ready to send when c.sig = c.ack. A value v is sent by setting c.val to v and complementing c.sig. Receipt of the value is acknowledged by complementing c.ack.

We consider an N-element queue with input channel i and output channel o. It

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

[figure: i.snd; i.ack; o.snd; o.ack; Queue]  ^{Fig. 2. A queue.}

Process Queue

output var i.ack, o.sig initially 0,

o.val;

internal var q initially ⟨ ⟩;

input var i.sig, i.val, o.ack;

cobegin loop [figure]if (i.ack ≠ i.sig) ∧ (|q| < N) [figure] endloop

then q := q ∘ ⟨i.val⟩;

i.ack := 1 − i.ack

∥ loop [figure]if (o.ack = o.sig) ∧ (|q| > 0) [figure] endloop

then o.val := head(q); q := tail(q); o.sig := 1 − o.sig

coend

Fig. 3. A queue process.

is depicted in Figure 2. To describe the queue, we use the programming-language constructs introduced in Section 2.1; in particular, we write large atomic actions within angle brackets. We also introduce the following notation for finite sequences: |ρ| denotes the length of sequence ρ, which equals 0 if ρ is empty; Head(ρ) and Tail(ρ) as usual denote the head (first element) and the tail of sequence ρ, if ρ is nonempty; and ρ ∘ τ denotes the concatenation of sequences ρ and τ. Moreover, angle brackets are used to form sequences; so ⟨ ⟩ denotes the empty sequence, and ⟨e⟩ denotes the sequence with e as its only element. With this notation, the queue can be written as in Figure 3.

Let QM be the TLA formula that represents this queue process. It might seem natural to take QM as the specification of the queue. However, this specification would be difficult or impossible to implement because it states that the queue behaves properly even if the environment does not obey the communication protocol. For example, in a lower-level implementation, reading the input o.ack and setting the outputs o.sig and o.val would be separate actions. If the environment changed o.ack between these actions, the implementation could violate the requirement that it change o.val only when o.ack = o.sig. This problem is not an artifact of our particular representation of the queue; actual hardware implementations of a queue can enter metastable states, consequently producing bizarre, unpredictable behavior, if their inputs are changed when they are not supposed to be [Mead and Conway 1980].

A specification of the queue should allow executions in which the queue performs correctly; it should not rule out bad behavior of the queue caused by the environment performing incorrectly. Such a specification can be written in the assumption/guarantee style, a generalization of the traditional pre/postcondition style for sequential programs. An assumption/guarantee specification asserts that the system provides a guarantee M if its environment satisfies an assumption E. For the queue, M is the formula QM , and E asserts that the environment obeys

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Fig. 4. A simple example.  [figure: c; \begin{matrix}System \\ C \end{matrix}; d; \begin{matrix}System \\ D \end{matrix}]

the communication protocol.

It is not obvious how to reason about the composition of systems described by assumption/guarantee specifications. The basic problem is illustrated by the simple case of two systems, one guaranteeing M_{c} assuming M_{d}, and the other guaranteeing M_{d} assuming M_{c}. Since each system guarantees to satisfy the other’s environment assumption, we would like to conclude that their composition implements the specification M_{c} ∧ M_{d} unconditionally, with no environment assumption. Can we? We attempt to answer this question by considering two simple examples, based on Figure 4.

In the first example:

—M_{c}^{0} asserts that c always equals 0. —M_{d}^{0} asserts that d always equals 0.

We can implement these specifications with the following two processes.

Process Π_{c} Process Π_{d} output var c initially 0 ; output var d initially 0 ; input var d; input var c; loop ⟨ c := d ⟩ endloop loop ⟨ d := c ⟩ endloop

Process Π_{c} guarantees M_{c}^{0} assuming M_{d}^{0}, and process Π_{d} guarantees M_{d}^{0} assuming M_{c}^{0}. Clearly, their composition leaves c and d unchanged, so it implements M_{c}^{0}∧M_{d}^{0}.

In the second example:

—M_{c}^{1} asserts that c eventually equals 1. —M_{d}^{1} asserts that d eventually equals 1.

The same processes Π_{c} and Π_{d} implement the specifications in this case too; process Π_{c} guarantees M_{c}^{1} assuming M_{d}^{1}, and process Π_{d} guarantees M_{d}^{1} assuming M_{c}^{1}. However, since their composition leaves c and d unchanged, it does not implement M_{c}^{1} ∧ M_{d}^{1}.

Our conclusion in the first example does not depend on the particular choice of processes Π_{c} and Π_{d}. We can deduce directly from the assumption/guarantee specifications that the composition must implement M_{c}^{0} ∧ M_{d}^{0}, because the first process to change its output variable would violate its guarantee before its assumption had been violated. This argument does not apply to the second example, because violating M_{c}^{1} and M_{d}^{1} are sins of omission that do not occur at any particular instant. A property that can be made false only by being violated at some instant is called a safety property [Alpern and Schneider 1985]. As the examples suggest, reasoning about the composition of assumption/guarantee specifications is easiest when assumptions are safety properties.

The argument that the composition should implement M_{c}^{0} ∧ M_{d}^{0} in the first example rests on the requirement that a process maintains its guarantee until after

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

the environment violates its assumption. In other words, we interpret the assumption/guarantee specification as an assertion that the guarantee M can become false only after the assumption E becomes false. We write this assertion as the formula E −▷^{+} M. Section 5 discusses this form of specification.

Our rules for reasoning about the composition of assumption/guarantee specifications are embodied in the Composition Theorem of Section 5.2. With the Composition Theorem, we can prove that the conjunction of the assumption/guarantee specifications M_{c}^{0} −▷^{+} M_{d}^{0} and M_{d}^{0} −▷^{+} M_{c}^{0} implies M_{c}^{0}∧M_{d}^{0}. We can also prove more substantial results—for example, that the composition of queues implements a larger queue. Verifying the hypotheses of the theorem requires reasoning only about complete systems, so the theorem allows us to handle assumption/guarantee specifications as easily as complete-system specifications.

3. PRELIMINARIES

3.1 TLA

3.1.1 Review of the Syntax and Semantics. A state is an assignment of values to variables. (Technically, our variables are the “flexible” variables of temporal logic that correspond to the variables of programming languages; they are distinct from the variables of first-order logic.) A behavior is an infinite sequence of states. Semantically, a TLA formula F is true or false of a behavior; we say that F is valid, and write ⊧ F, iff it is true of every behavior. Syntactically, TLA formulas are built up from state functions using Boolean operators (¬, ∧, ∨, ⇒ [implication], and = [equivalence]) and the operators ′, □, and ∃ ∃ ∃ ∃ ∃ ∃, as described below.

A state function is like an expression in a programming language. Semantically, it assigns a value to each state—for example 3 + x assigns to state s three plus the value of the variable x in s. A state predicate is a Boolean-valued state function. An action is a Boolean-valued expression containing primed and unprimed variables. Semantically, an action is true or false of a pair of states, with primed variables referring to the second state—for example, x + 1 > y′ is true for ⟨s, t⟩ iff the value of x + 1 in s is greater than the value of y in t. A pair of states satisfying action A is called an A step. We say that A is enabled in state s iff there exists a state t such that ⟨s, t⟩ is an A step—for example, (x > 0) ∧ (x + 1 > y′) is enabled only in states where x > 0. The state predicate Enabled A is true for state s iff A is enabled in s. We write v′ for the expression obtained by priming all the variables of the state function v, and [A]_{v} for A ∨ (v′ = v), so an [A]_{v} step is either an A step or a step that leaves v unchanged.

As usual in temporal logic, if F is a formula then □F is a formula that means that F is always true, and ◇F, an abbreviation for ¬□¬F, means that F is eventually true. In addition, if A is an action and v is a state function then □[A]_{v} is a formula; ◇⟨A⟩_{v} is an abbreviation for ¬□[¬A]_{v}. Using □ and “enabled” predicates, we can define fairness operators WF and SF. The weak-fairness formula WF_{v}(A) asserts of a behavior that either there are infinitely many A steps that change v, or there are infinitely many states in which such steps are not enabled. This can be written (□◇⟨A⟩_{v}) ∨ (□◇¬Enabled ⟨A⟩_{v}). The strong-fairness formula SF_{v}(A) asserts that either there are infinitely many A steps that change v, or there are only finitely many states in which such steps are enabled. This can be written

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

(□◇⟨A⟩_{v}) ∨ (◇□¬Enabled ⟨A⟩_{v}).

The formula ∃ ∃ ∃ ∃ ∃ ∃x : F means essentially that there is some way of choosing a sequence of values for x such that the temporal formula F holds. We think of ∃ ∃ ∃ ∃ ∃ ∃x : F as “F with x hidden” and call x an internal variable of ∃ ∃ ∃ ∃ ∃ ∃x : F. Both x and x′ are bound by ∃ ∃ ∃ ∃ ∃ ∃x in ∃ ∃ ∃ ∃ ∃ ∃x : F. If x is a tuple of variables ⟨x_{1}, …, x_{k}⟩, we write ∃ ∃ ∃ ∃ ∃ ∃x : F for ∃ ∃ ∃ ∃ ∃ ∃x_{1} : … ∃ ∃ ∃ ∃ ∃ ∃x_{k} : F.

The standard way of specifying a system in TLA is with a formula in the “canonical form” ∃ ∃ ∃ ∃ ∃ ∃x : Init ∧ □[N]_{v} ∧ L, where Init is a predicate and L a conjunction of fairness conditions. This formula asserts that there exists a sequence of values for x such that (1) Init is true for the initial state, (2) every step of the behavior is an N step or leaves the state function v unchanged, and (3) L holds. For example, the specification M_{gcd} of the complete high-level GCD program is written in canonical form by taking^{1}

Init =^{Δ} (a = 233344) ∧ (b = 233577899)
N =^{Δ}  \begin{matrix}∨ (a > b) ∧ (a′ = a − b) ∧ (b′ = b) \\ ∨ (b > a) ∧ (b′ = b − a) ∧ (a′ = a) \end{matrix}
v =^{Δ} ⟨a, b⟩
L =^{Δ} WF_{v}(N)

(2)

Intuitively, a variable represents some part of the universe, and a behavior represents a possible complete history of the universe. A system Π is represented by a TLA formula M that is true for precisely those behaviors that represent histories in which Π is running. We make no formal distinction between systems, specifications, and properties; they are all represented by TLA formulas, which we usually call specifications.

3.1.2 Interleaving and Noninterleaving Representations. Let ξ and ψ be two objects, represented by the variables x and y, respectively. When representing a history of the universe as a behavior, we can describe concurrent changes to ξ and ψ either by a single simultaneous change to x and y, or by separate changes to x and y in some order. If the changes to ξ and ψ are directly linked, then it is usually most convenient to describe their concurrent change by a single change to both x and y. However, if the changes are independent, then we are free to choose whether or not to allow simultaneous changes to x and y. An interleaving representation is one in which such simultaneous changes are disallowed.

When changes to ξ and ψ are directly linked, we often think of x and y as output variables of a single component. An interleaving representation is then one in which simultaneous changes to output variables of different processes are disallowed. The absence of such simultaneous changes can be expressed as a TLA formula. For a system with n components in which v_{i} is the tuple of output variables of component i, interleaving is expressed by the formula

Disjoint(v_{1}, …, v_{n}) =^{Δ} ⋀_{i≠j} □[(v′_{i} = v_{i}) ∨ (v′_{j} = v_{j})]_{⟨v_{i}, v_{j}⟩}

1We let a list of formulas bulleted with ∧ or ∨ denote the conjunction or disjunction of the formulas, using indentation to eliminate parentheses. We also let ⇒ have lower precedence than the other Boolean operators.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

[figure: i.snd; i.ack; o.snd; o.ack; Queue; S e n d e r; R e c e i v e r]

Fig. 5. The complete system of queue plus environment.

We have found that, in TLA, interleaving representations are usually easier to write and to reason about. Moreover, an interleaving representation is adequate for reasoning about a system if the system is modeled at a sufficiently fine grain of atomicity. However, as discussed below, TLA also works for noninterleaving representations. TLA does not mandate any particular method for representing systems. Indeed, one can write specifications that are intermediate between interleaving and noninterleaving representations.

3.1.3 The Queue Example. We now give a TLA specification of the queue of natural numbers of length N, which was described informally in Section 2.2 and illustrated in Figure 2. As in Section 2.2, we write c.snd for the pair ⟨c.sig, c.val⟩ for a channel c; we also write c for the triple ⟨c.sig, c.ack, c.val⟩.

A channel is initially ready for sending, so the initial condition on wire c is the predicate CInit(c) defined by

CInit(c) =^{Δ} (c.sig = c.ack = 0)

The operations of sending a value v and acknowledging receipt of a value on channel c are represented by the following Send(v, c) and Ack(c) actions.

Send(v, c) =^{Δ} ∧ c.sig = c.ack ∧ c.snd′ = ⟨1 − c.sig, v⟩ ∧ c.ack′ = c.ack Ack(c) =^{Δ} ∧ c.sig ≠ c.ack ∧ c.ack′ = 1 − c.ack ∧ c.snd′ = c.snd

To represent the queue as a complete system, we add an environment that sends arbitrary natural numbers over channel i and acknowledges receipt of values on channel o. The resulting complete system is shown in Figure 5.

The TLA formula CQ specifying the queue is defined in Figure 6. It has the canonical form ∃ ∃ ∃ ∃ ∃ ∃x : Init ∧ □[N]_{v} ∧ L, where:

—x is the internal variable q, which represents the sequence of values received on

the input channel i but not yet sent on the output channel o. —Init is written as the conjunction Init_{E} ∧ Init_{M} of initial predicates for the

environment and component. (We arbitrarily consider the initial conditions on a channel to be part of the sender’s initial predicate.)

—N is the disjunction of two actions: Q_{M}, describing the steps taken by the component, and Q_{E} ∧(q′ = q), describing steps taken by the environment (which leave q unchanged). Action Q_{M} is the disjunction of actions Enq and Deq. An Enq step acknowledges receipt of a value on i and appends the value to q; it is enabled only when q has fewer than N elements. A Deq step removes the first element of q and sends it on o. Action Q_{E} is the disjunction of Put, which

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Init_{E} =^{Δ} CInit(i)  Environment Actions
Put =^{Δ} (∃v ∈ Nat : Send(v, i)) ∧ (o′ = o)
Get =^{Δ} Ack(o) ∧ (i′ = i)
Q_{E}  =^{Δ} Get ∨ Put
Init_{M} =^{Δ} CInit(o) ∧ (q = ⟨ ⟩)  Component Actions
Enq =^{Δ} \begin{matrix}∧ |q| < N \\ ∧ Ack(i) ∧ (q′ = q ∘ ⟨i.val⟩) \\ ∧ o′ = o \end{matrix}

Deq =^{Δ} ∧ |q| > 0
∧ Send(Head(q), o) ∧ (q′ = Tail(q))
∧ i′ = i
Q_{M}  =^{Δ} Enq ∨ Deq
ICL =^{Δ}

WF_{⟨i, o, q⟩}(Q_{M}) Complete-System

Specification

ICQ =^{Δ}

∧ Init_{E} ∧ Init_{M}

∧ □ [ \begin{matrix}∨ Q_{E} ∧ (q′ = q) \\ ∨ Q_{M} \end{matrix}]_{⟨i, o, q⟩}

∧ ICL

CQ  =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ q : ICQ

Fig. 6. The specification CQ of the complete queue. (Formulas CInit, Send, and Ack are defined in the text.)

sends an arbitrary number on channel i, and Get, which acknowledges receipt of a number on channel o.

—v is the tuple ⟨i, o, q⟩ of all relevant variables.^{2} —L is the weak-fairness condition ICL, which is defined to be WF_{⟨i, o, q⟩}(Q_{M}), and

asserts that a component step cannot remain forever possible without occurring. It can be shown that a logically equivalent specification is obtained if this condition is replaced with WF_{⟨i, o, q⟩}(Enq) ∧ WF_{⟨i, o, q⟩}(Deq).

Formula CQ gives an interleaving representation of a queue; simultaneous steps by the queue and its environment are not allowed. Moreover, simultaneous changes to the two inputs i.snd and o.ack are disallowed, as are simultaneous changes to the two outputs i.ack and o.snd. In Section 4, we describe a noninterleaving representation of the queue.

3.2 Implementation

A specification M^{l} implies a specification M iff every behavior that satisfies M^{l} also satisfies M; hence proving M^{l} ⇒ M shows that the system Π^{l} represented by M^{l} implements the system or property Π represented by M. Note that if M^{l} is inconsistent (equivalent to false), then M^{l} ⇒ M holds vacuously, but an inconsistent M^{l} does not represent any system Π^{l}.

The formula M^{l} ⇒ M is proved by applying a handful of simple rules [Lamport 1994]. When M has the form ∃ ∃ ∃ ∃ ∃ ∃ x : M̂, a key step in the proof is finding a refinement

2Informally, we write ⟨i, o, q⟩ for the concatenation of the tuples i, o, and ⟨q⟩.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

[figure: i.snd; i.ack; z.snd; z.ack; Queue1; S e n d e r; o.snd; o.ack; Queue2; R e c e i v e r]

Fig. 7. A complete system containing two queues in series.

ICDQ =^{Δ}

∧ Init_{E} ∧ Init_{M}^{[1]} ∧ Init_{M}^{[2]}

∧ □ [ \begin{matrix}∨ Q_{E} ∧ & ⟨q_{1}, q_{2}, z⟩′ = ⟨q_{1}, q_{2}, z⟩ \\ ∨ Q_{M}^{[1]} ∧ & ⟨q_{2}, o⟩′ = ⟨q_{2}, o⟩ \\ ∨ Q_{M}^{[2]} ∧ & ⟨q_{1}, i⟩′ = ⟨q_{1}, i⟩ \end{matrix} ]_{⟨i, o, z, q_{1}, q_{2}⟩}

∧ ICL^{[1]} ∧ ICL^{[2]}

CDQ =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ q_{1}, q_{2} : ICDQ

Fig. 8. Specification of the complete double-queue system of Figure 7.

mapping—a tuple of state functions \overline{x} such that M^{l} implies \overline{M̂}, where \overline{M̂} is the formula obtained by substituting \overline{x} for x (and therefore (\overline{x})′ for x′) in M̂. Under reasonable assumptions, such a refinement mapping exists when M^{l} ⇒ ∃ ∃ ∃ ∃ ∃ ∃ x : M̂ is valid [Abadi and Lamport 1991].

As an example, we show that the system composed of two queues in series, shown in Figure 7, implements a single larger queue. We first specify the composite queue. Let F [e_{1}/v_{1}, …, e_{n}/v_{n}] denote the result of (simultaneously) substituting each expression e_{i} for v_{i} in a formula F. For example, if Get is defined as in Figure 6, then Get[z/i] equals Ack(o) ∧ (z′ = z). For any formula F, let

F^{[1]} =^{Δ} F [z/o, q_{1}/q] F^{[2]} =^{Δ} F [z/i, q_{2}/q]

In Figure 8, the specification CDQ of the complete system, consisting of the double queue and its environment, is defined in terms of the formulas from Figure 6. We think of the complete system as containing three components: the environment and the two queues. The initial condition is the conjunction of the initial conditions of each component. The next-state action consists of three disjuncts, representing actions of each of the three components that leave other components’ variables unchanged. Finally, we take as the liveness condition the conjunction of the fairness conditions of the two queues.

We now show that the composite queue implements a (2N + 1)-element queue. (The “+1” arises because the internal channel z acts as a buffer element.) The correctness condition is CDQ ⇒ CQ^{[dbl]}, where F^{[dbl]} denotes F [(2N + 1)/N], for any formula F. This is proved by showing ICDQ ⇒ \overline{ICQ^{[dbl]}}, with the refinement

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

mapping defined by

q

=^{Δ}
if z.sig = z.ack then q_{1} ∘ q_{2}
else q_{1} ∘ ⟨z.val⟩ ∘ q_{2}

The formula ICDQ ⇒ \overline{ICQ^{[dbl]}} can be proved by standard TLA reasoning of the kind described by Lamport [1994].

3.3 Conditional Implementation

Instead of proving that a specification M^{l} implements a specification M, we sometimes want to prove the weaker condition that M^{l} implements M assuming a formula G. In other words, we want to prove G ⇒ (M^{l} ⇒ M), which is equivalent to G ∧ M^{l} ⇒ M. The formula G may express one or more of the following:

—A law of nature. For example, in a real-time specification, G might assert that time increases monotonically. If the current time is represented by the variable now, this assumption is expressed by the formula (now ∈ R) ∧ □[now′ ∈ (now, ∞)]_{now}, where R is the set of real numbers.

—An interface refinement, where G expresses the relation between a low-level tuple l of variables and its high-level representation as a tuple h of variables. For example, l might be a low-level interface representing the transmission of sequences of bits over a wire, and h could be the high-level interface in which the sending of seven successive bits is interpreted as the transmission of a single ASCII character.

—An assumption about how reality is translated into the formalism of behaviors. In particular, G may assert an interleaving assumption—for example, an assumption of the form Disjoint(v_{1}, …, v_{n}).

Conditional implementation, with an explicit formula G, is needed only for open systems. For a complete system, the properties expressed by G can easily be made part of the system specification. For example, the system can include a component that advances time. In contrast, it can be difficult to include G in the specification of an open system.

3.4 Safety and Closure

3.4.1 Definition of Closure. A finite sequence of states is called a finite behavior. For any formula F and finite behavior ρ, we say that ρ satisfies F iff ρ can be extended to an infinite behavior that satisfies F. For convenience, we say that the empty sequence ⟨ ⟩ satisfies every formula (even false).

A safety property is a formula that is satisfied by an infinite behavior σ iff it is satisfied by every prefix of σ [Alpern and Schneider 1985]. For any predicate Init, action N, and state function v, the formula Init ∧ □[N]_{v} is a safety property. It can be shown that, for any TLA formula F, there is a TLA formula C(F), called the closure of F, such that a behavior σ satisfies C(F) iff every prefix of σ satisfies F. Formula C(F) is the strongest safety property such that ⊧ F ⇒ C(F). Proposition 1 below implies that C(Init ∧ □[N]_{v} ∧ L) equals Init ∧ □[N]_{v} when L is the conjunction of suitable fairness properties.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

3.4.2 Machine Closure. When writing a specification in the form Init ∧□[N]_{v}∧L, we expect L to constrain infinite behaviors, not finite ones. Formally, this means that the closure of Init ∧ □[N]_{v} ∧ L should be Init ∧ □[N]_{v}. A pair of properties (P, L) is called machine closed iff C(P ∧ L) equals P [Abadi and Lamport 1991]. (We often say informally that P ∧ L is machine closed.)

Proposition 1 below, which we have already proved [Abadi and Lamport 1994], shows that we can use fairness properties to write machine-closed specifications. The proposition relies on the following definition: an action A is a subaction of a safety property P iff for every finite behavior ρ = ⟨r_{0}, …, r_{n}⟩, if ρ satisfies P and A is enabled in state r_{n}, then there exists a state r_{n+1} such that ⟨r_{0}, …, r_{n+1}⟩ satisfies P and ⟨r_{n}, r_{n+1}⟩ is an A step. It follows from this definition of subaction that, if A implies N, then A is a subaction of Init ∧ □[N]_{v}.

Proposition 1. If P is a safety property and L is the conjunction of a countable number of formulas of the form WF_{w}(A) and/or SF_{w}(A) such that A ∧ (w′ ≠ w) is a subaction of P, then (P, L) is machine closed.

3.4.3 Closure and Hiding. Several of our results have hypotheses of the form C(M_{1}) ∧ … ∧ C(M_{n}) ⇒ C(M). The obvious first step in proving such a formula is to compute the closures C(M_{1}), …, C(M_{n}), and C(M). We can use Proposition 1 to compute the closure of a formula with no internal variables. When there are internal variables, the following proposition allows us to reduce the proof of C(M_{1}) ∧ … ∧ C(M_{n}) ⇒ C(M) to the proof of a formula in which the closures can be computed with Proposition 1.

Proposition 2. Let x, x_{1}, …, x_{n} be tuples of variables such that for each i, no variable in x_{i} occurs in M or in any M_{j} with i ≠ j.

If ⊧ ⋀_{i=1}^{n} C(M_{i}) ⇒ ∃ ∃ ∃ ∃ ∃ ∃ x : C(M), then ⊧ ⋀_{i=1}^{n} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃x : M).

Proofs are in the appendix.

Some of our results also have hypotheses of the form C(M_{1}) ∧ … ∧ C(M_{n}) ⇒ E, where we expect E to be a safety property. If we can verify that E is a safety property, so ⊧ E = C(E), then we can apply Proposition 2. When E has internal variables, we can often use Proposition 2 of [Abadi and Lamport 1991] to verify that E is a safety property.

3.5 Additional Temporal Operators

We now define some additional temporal operators. Although they can be expressed in terms of the primitive TLA operations ′, □, and ∃ ∃ ∃ ∃ ∃ ∃, we define them semantically.

3.5.1 The + Operator. The formula E_{+v} asserts that, if the temporal formula E ever becomes false, then the state function v stops changing. More precisely, a behavior σ satisfies E_{+v} iff either σ satisfies E, or there is some n such that (1) E holds for the first n states of σ and (2) v never changes from the (n + 1)st state on. When E is a safety property in canonical form, it is easy to write E_{+v} explicitly:

Proposition 3. If x is a tuple of variables none of which occurs in v, and s is a variable that does not occur in Init, N, w, v, or x, and

Înit =^{Δ} (Init ∧ (s = 0)) ∨ (¬Init ∧ (s = 1))
N̂ =^{Δ} \begin{matrix}∨ (s = 0) ∧ \begin{matrix}∨ (s′ = 0) ∧ (N ∨ (w′ = w)) \\ ∨ (s′ = 1) ∧ ¬(N ∨ (w′ = w)) \end{matrix} \\ ∨ (s = 1) ∧ (s′ = 1) ∧ (v′ = v) \end{matrix}

then ⊧ (∃ ∃ ∃ ∃ ∃ ∃ x : Init ∧ □[N]_{w})_{+v} = ∃ ∃ ∃ ∃ ∃ ∃ x, s : Înit ∧ □[N̂]_{⟨w, v, s⟩}.

We need to reason about + only to verify hypotheses of the form ⊧ C(E)_{+v} ∧ C(M^{l}) ⇒ C(M) in our Decomposition and Composition Theorems. We can verify such a hypothesis by first applying the observation that C(E)_{+v} equals C(E_{+v}) and using Proposition 3 to calculate E_{+v}. However, this approach is necessary only for noninterleaving specifications. Proposition 4 below provides a way of proving these hypotheses for interleaving specifications without having to calculate E_{+v}.

3.5.2 The −▷ Operator. For temporal formulas E and M, the formula E −▷ M asserts that M holds at least as long as E does [Abadi and Plotkin 1993]. More precisely E −▷ M is true of a behavior σ iff E ⇒ M is true of σ and, for every finite prefix ρ of σ, if E is true of ρ then M is true of ρ. It follows from this definition of −▷ that E −▷ M equals (C(E) −▷ C(M)) ∧ (E ⇒ M). The operator −▷ acts much like ordinary implication. In fact, ⊧ E −▷ M is equivalent to ⊧ E ⇒ M. Of course, it is not in general true that ⊧ (E −▷ M) = (E ⇒ M).

3.5.3 The −▷^{+} Operator. As we observed in the introduction, we interpret the specification that M is guaranteed under assumption E as the formula E −▷^{+} M, which means that M holds at least one step longer than E does. More precisely, E −▷^{+} M is true of a behavior σ iff E ⇒ M is true of σ and, for every n ≥ 0, if E holds for the first n states of σ, then M holds for the first n+1 states of σ. It follows from this definition of −▷^{+} that E −▷^{+} M equals (C(E) −▷^{+} C(M)) ∧ (E ⇒ M).

The formula E −▷^{+} M is stronger than E −▷ M, which asserts that M holds as long as E does. It can be shown that, if E is a safety property, then E −▷^{+} M equals (M −▷ E) −▷ M. We prove in the appendix that, if E and M are both safety properties and v is a tuple of variables containing all free variables of M,

then E −▷^{+} M equals E_{+v} −▷ M.

3.5.4 The ⊥ Operator. The specification M of a component can be made false only by a step that changes the component’s output variables. In an interleaving representation, we do not allow a single step to change output variables of two different components. Hence, if E and M are specifications of separate components, we expect that no step will make both E and M false. More precisely, we expect E and M to be orthogonal (⊥), where E ⊥ M is true of a behavior σ iff there is no n ≥ 0 such that E and M are both true for the first n states of σ and both false for the first n+1 states of σ. It can be shown that E ⊥ M equals C(E) ⊥ C(M), and that, if E and M are safety properties, then E ⊥ M equals (E ∧ M) −▷^{+} (E ∨ M).

If no step falsifies both E and M, and M remains true as long as E does, then M must remain true at least one step longer than E does. Hence, E ⊥ M implies the equivalence of E −▷ M and E −▷^{+} M. In fact, we prove in the appendix that

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

(E −▷^{+} M) = (E −▷ M) ∧ (E ⊥ M) is valid. From this and the relation between −▷^{+} and +, we can derive:

Proposition 4. If E, M, and R are safety properties, and v is a tuple of variables containing all variables that occur free in M, then ⊧ E ∧ R ⇒ M and ⊧ R ⇒ E ⊥ M imply ⊧ E_{+v} ∧ R ⇒ M.

This proposition enables us to use orthogonality to remove + from proof obligations. To apply the proposition, we must prove the orthogonality of component specifications. We do this for interleaving specifications with the following result.

Proposition 5. If

⊧ C(E) = Init_{E} ∧ □[N_{E}]_{⟨x, e⟩}
⊧ C(M) = Init_{M} ∧ □[N_{M}]_{⟨y, m⟩}

then ⊧ (∃x : Init_{E} ∨ ∃y : Init_{M}) ∧ Disjoint(e, m) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃x : E) ⊥ C(∃ ∃ ∃ ∃ ∃ ∃y : M)

4. DECOMPOSING A COMPLETE SPECIFICATION

4.1 Specifying a Component

Let us consider how to write the specification M of one component of a larger system. We assume that the free variables of the specification can be partitioned into tuples m of output variables and e of input variables; the component changes the values of the variables of m only. (A more general situation is discussed below.) The specification of a component has the same form ∃ ∃ ∃ ∃ ∃ ∃x : Init ∧ □[N]_{v} ∧ L as that of a complete system. For a component specification:

—v is the tuple ⟨x, m, e⟩.

—Init describes the initial values of the component’s output variables m and internal variables x.

—N should allow two kinds of steps—ones that the component performs and ones that its environment performs. Steps performed by the component, which change its output variables m, are described by an action N_{m}. In an interleaving representation, the component’s inputs and outputs cannot change simultaneously, so N_{m} implies e′ = e. In a noninterleaving representation, N_{m} does not constrain the value of e′, so the variables of e do not appear primed in N_{m}. In either case, we are specifying the component but not its environment, so we let the environment do anything except change the component’s output variables or internal variables. In other words, the environment is allowed to perform any step in which ⟨m, x⟩′ equals ⟨m, x⟩. (Below, we describe more general specifications in which an environment action can change x.) Therefore, N should equal N_{m} ∨ (⟨m, x⟩′ = ⟨m, x⟩).

—L is the conjunction of fairness conditions, each of the form WF_{⟨m, x⟩}(A) or SF_{⟨m, x⟩}(A). For an interleaving representation, which by definition does not allow steps that change both e and m, the subscripts ⟨m, x⟩ and ⟨e, m, x⟩ yield equivalent fairness conditions.

This leads us to write M in the form

M =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃x : Init ∧ □[N_{m} ∨ (⟨m, x⟩′ = ⟨m, x⟩)]_{⟨e, m, x⟩} ∧ L  (3)

By simple logic, (3) is equivalent to

M =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : Init ∧ □[N_{m}]_{⟨m, x⟩} ∧ L  (4)

For the specification M_{a} of process Π_{a} in the GCD example, x is the empty tuple (there is no internal variable), the input variable e is b, the output variable m is a, and

Init_{a} =^{Δ} a = 233344
N_{a}  =^{Δ} (a > b) ∧ (a′ = a − b) ∧ (b′ = b)
M_{a}  =^{Δ} Init_{a} ∧ □[N_{a}]_{a} ∧ WF_{a}(N_{a})

(5)

For the specification M_{a}^{l} of the low-level process Π_{a}^{l}, the tuple x is ⟨ai, pca⟩, where pca is an internal variable that tells whether control is at the beginning of the loop or after the assignment to ai. The specification has the form

M_{a}^{l} =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ ai, pca : Init_{a}^{l} ∧ □[N_{a}^{l}]_{⟨a, ai, pca⟩} ∧ WF_{⟨a, ai, pca⟩}(N_{a}^{l})  (6)

for appropriate initial condition Init_{a}^{l} and next-state action N_{a}^{l}. The specifications M_{b} and M_{b}^{l} are similar.

In our queue example, we can write the specifications of both the queue and its environment as separate components in the form (4). For the queue component, the tuple m of output variables is ⟨i.ack, o.snd⟩, the tuple e of input variables is ⟨i.snd, o.ack⟩, and the specification is

IQM =^{Δ} Init_{M} ∧ □[Q_{M}]_{⟨i.ack, o.snd, q⟩} ∧ ICL
QM =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ q : IQM

(7)

The specification of the environment as a separate component is

QE =^{Δ} Init_{E} ∧ □ [Q_{E}]_{⟨i.snd, o.ack⟩}  (8)

We have provided specifications of the queue and its environment in an interleaving representation. A noninterleaving representation of the queue can be obtained by modifying its specification as follows.

—Change the Enq and Deq actions so they do not constrain the values of i.snd′ or

o.ack′. —Define an action DeqEnq that simultaneously enqueues an input value and de-

queues an output value, and change the definition of Q_{M} to have DeqEnq as an additional disjunct.

The resulting specification QM^{ni} is given in Figure 9. It is a noninterleaving specification because it allows a step that changes i and o simultaneously. A noninterleaving representation of the queue’s environment can be obtained in a similar fashion.

In describing the component’s next-state action N, we required that an environment action not change the component’s internal variables. One can also write a

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Init_{M}  =^{Δ} CInit(o) ∧ (q = ⟨ ⟩)
Enq^{ni}  =^{Δ} ∧ |q| < N

∧ Ack(i) ∧ (q′ = q ∘ ⟨i.val⟩)

∧ o.snd′ = o.snd

Deq^{ni}  =^{Δ} ∧ |q| > 0

∧ Send(Head(q), o) ∧ (q′ = Tail(q))

∧ i.ack′ = i.ack

DeqEnq^{ni} =^{Δ}

∧ (|q| > 0) ∧ Send(Head(q), o)

∧ Ack(i)

∧ q′ = Tail(q) ∘ ⟨i.val⟩

Qni_{M}  =^{Δ} Enq^{ni} ∨ Deq^{ni} ∨ DeqEnq^{ni}
IQM^{ni}  =^{Δ} Init_{M} ∧ □[Qni_{M}]_{⟨i.ack, o.snd, q⟩} ∧ WF_{⟨i.ack, o.snd, q⟩}(Qni_{M})
QM^{ni}  =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ q : IQM^{ni}

Fig. 9. A noninterleaving representation of the queue component.

specification in which the component records environment actions by changing its own internal variables. In this case, N will not equal N_{m} ∨ (⟨m, x⟩′ = ⟨m, x⟩), but may just imply (e′ = e) ∨ (m′ = m). The resulting formula will not be a pure interleaving specification because environment actions can change the component’s variables, but no action can change both the component’s and the environment’s output variables. We have not explored this style of specification.

We have been assuming that the visible variables of the component’s specification can be partitioned into tuples m of output variables and e of input variables. To see how to handle a more general case, let μ_{M} be the action m′ ≠ m, let v equal ⟨e, m⟩, and observe that [N_{M}]_{⟨m, x⟩} equals [N_{M} ∨ (¬μ_{M} ∧ (x′ = x))]_{⟨v, x⟩}. A μ_{M} step is one that is attributed to the component, since it changes the component’s output variables. When the tuple v of variables is not partitioned into input and output variables, we define an action μ_{M} that specifies what steps are attributed to the component, and we write the component’s next-state action in the form N_{M} ∨ (¬μ_{M} ∧ (x′ = x)). All our results for separate input and output variables can be generalized by writing the next-state action in this form. However, for simplicity, we consider only the special case.

4.2 Conjoining Components to Form a Complete System

In Section 3.1, we describe how to specify a complete system. In Section 4.1, we describe how to specify an individual component of a system. A complete system is the composition of its components. Composing two systems means constructing a universe in which they are both running. If formulas M_{1} and M_{2} represent the two systems, then M_{1} ∧ M_{2} represents their composition, since a behavior represents a possible history of a universe containing both systems iff it satisfies both M_{1} and M_{2}. Thus, in principle, composition is conjunction. We now show that composition is conjunction in practice as well.

For composition to be conjunction, the conjunction of the specifications of all components should be equivalent to the specification of the complete system. For example, the conjunction of the specifications QM of the queue and QE of its environment should be equivalent to the specification CQ of the complete system

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

shown in Figure 5. Recall that

QE = Init_{E} ∧ □ [Q_{E}]_{⟨i.snd, o.ack⟩}
QM = ∃ ∃ ∃ ∃ ∃ ∃ q : Init_{M} ∧ □[Q_{M}]_{⟨i.ack, o.snd, q⟩} ∧ ICL
CQ = ∃ ∃ ∃ ∃ ∃ ∃ q : ∧ Init_{E} ∧ Init_{M} ∧ □ [ \begin{matrix}∨ Q_{E} ∧ (q′ = q) \\ ∨ Q_{M} \end{matrix}]_{⟨i, o, q⟩} ∧ ICL

We deduce the equivalence of QE ∧ QM and CQ from the following result, by substituting QE for M_{1} and QM for M_{2}. (In this case, x_{1} is the empty tuple ⟨ ⟩, so x̂_{2} equals ⟨ ⟩ and x′_{2} = x̂_{2} equals true.)

Proposition 6. Let m_{1}, …, m_{n}, x_{1}, …, x_{n} be tuples of variables, and let

m =^{Δ} ⟨m_{1}, …, m_{n}⟩ x =^{Δ} ⟨x_{1}, …, x_{n}⟩

x̂_{i} =^{Δ} ⟨x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}⟩

M_{i} =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x_{i} : Init_{i} ∧ □[N_{i}]_{⟨m_{i}, x_{i}⟩} ∧ L_{i}

If, for all i, j = 1, …, n with i ≠ j:

(1) no variable of x_{j} occurs free in x_{i} or M_{i},

(2) m includes all free variables of M_{i}, and

(3) ⊧ N_{i} ⇒ (m′_{j} = m_{j})

then

⊧ ⋀_{i=1}^{n} M_{i} = ∃ ∃ ∃ ∃ ∃ ∃ x : ⋀_{i=1}^{n} Init_{i} ∧ □[ ⋁_{i=1}^{n} N_{i} ∧ (x′_{i} = x̂_{i})]_{⟨m, x⟩} ∧ ⋀_{i=1}^{n} L_{i}

In this proposition, the third hypothesis asserts that component i leaves the variables of other components unchanged, so M_{i} is an interleaving representation of component i. Hence, M_{i} implies Disjoint(m_{i}, m_{j}), for each j ≠ i, and ⋀_{i=1}^{n} M_{i} implies Disjoint(m_{1}, …, m_{n}), as expected for an interleaving representation of the complete system.

In the GCD example, we apply this proposition to the formula M_{a} of (5) and the analogous formula M_{b}. We immediately get that M_{a} ∧M_{b} is equivalent to a formula that is the same as M_{gcd}, defined by (2), except with WF_{⟨a, b⟩}(N_{a}) ∧ WF_{⟨a, b⟩}(N_{b}) instead of WF_{⟨a, b⟩}(N). It can be shown that these two fairness conditions are equivalent; hence M_{a} ∧ M_{b} is equivalent to M_{gcd}.

For another example of decomposition, we consider the system of Figure 7, which consists of two queues in series together with an environment. This system can be decomposed into three components with the following specifications.

1st queue: ∃ ∃ ∃ ∃ ∃ ∃ q_{1} : Init_{M}^{[1]} ∧ □[Q_{M}^{[1]} ∧ (o′ = o)]_{⟨i.ack, z.snd, q_{1}⟩} ∧ ICL^{[1]}
2nd queue: ∃ ∃ ∃ ∃ ∃ ∃ q_{2} : Init_{M}^{[2]} ∧ □[Q_{M}^{[2]} ∧ (i′ = i)]_{⟨z.ack, o.snd, q_{2}⟩} ∧ ICL^{[2]}
environment: Init_{E} ∧ □[Q_{E} ∧ (z′ = z)]_{⟨i.snd, o.ack⟩}

To obtain an interleaving representation, we have conjoined o′ = o to Q_{M}^{[1]} in the

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

first queue’s next-state action, because Q_{M}^{[1]} does not mention o. Similarly, we have conjoined i′ = i to the second queue’s next-state action, and z′ = z to the environment’s. It follows from Proposition 6 that the conjunction of these three specifications equals the specification CDQ of the complete system, defined in Figure 8.

The third hypothesis of Proposition 6 is satisfied only by interleaving representations. For arbitrary representations, a straightforward calculation shows

⊧ ⋀_{i=1}^{n} M_{i} = ∃ ∃ ∃ ∃ ∃ ∃ x : \begin{matrix}∧ ⋀_{i=1}^{n} Init_{i} \\ ∧ □[ ⋀_{i=1}^{n}(N_{i} ∨ ⟨m_{i}, x_{i}⟩′ = ⟨m_{i}, x_{i}⟩)]_{⟨m, x⟩} \\ ∧ ⋀_{i=1}^{n} L_{i} \end{matrix}  (9)

assuming only the first hypothesis of the proposition. The right-hand side has the expected form for a noninterleaving specification, since it allows N_{i} ∧ N_{j} steps for i ≠ j. Hence, composition is conjunction for noninterleaving representations too.

4.3 The Decomposition Theorem

4.3.1 The Basic Theorem. Consider a complete system decomposed into components Π_{i}. We would like to prove that this system is implemented by a lower-level one, consisting of components Π_{i}^{l}, by proving that each Π_{i}^{l} implements Π_{i}. Let M_{i} be the specification of Π_{i} and M_{i}^{l} be the specification of Π_{i}^{l}. We must prove that ⋀_{i=1}^{n} M_{i}^{l} implies ⋀_{i=1}^{n} M_{i}. This implication is trivially true if M_{i}^{l} implies M_{i}, for all i. However, as we saw in the GCD example, M_{i}^{l} need not imply M_{i}.

Even when M_{i}^{l} ⇒ M_{i} does not hold, we need not reason about all the lower-level components together. Instead, we prove E_{i} ∧ M_{i}^{l} ⇒ M_{i}, where E_{i} includes just the properties of the other components assumed by component i, and is usually much simpler than ⋀_{k≠i} M_{k}^{l}. Proving E_{i} ∧ M_{i}^{l} ⇒ M_{i} involves reasoning only about component i, not about the entire lower-level system.

In propositional logic, to deduce that ⋀_{i=1}^{n} M_{i}^{l} implies ⋀_{i=1}^{n} M_{i} from ⋀_{i=1}^{n}(E_{i} ∧ M_{i}^{l} ⇒ M_{i}), we may prove that ⋀_{k=1}^{n} M_{k}^{l} implies E_{i} for each i. However, proving this still requires reasoning about ⋀_{k=1}^{n} M_{k}^{l}, the specification of the entire lower-level system. The following theorem shows that we need only prove that E_{i} is implied by ⋀_{k=1}^{n} M_{k}, the specification of the higher-level system—a formula usually much simpler than ⋀_{k=1}^{n} M_{k}^{l}.

Proving E_{i}∧M_{i}^{l} ⇒ M_{i} and (⋀_{k=1}^{n} M_{k}) ⇒ E_{i} for each i and deducing (⋀_{i=1}^{n} M_{i}^{l}) ⇒ (⋀_{i=1}^{n} M_{i}) is circular reasoning, and is not sound in general. Such reasoning would allow us to deduce (⋀_{i=1}^{n} M_{i}^{l}) ⇒ (⋀_{i=1}^{n} M_{i}) for any M_{i}^{l} and M_{i}—simply let E_{i} equal M_{i}. To break the circularity, we need to add some C’s and one hypothesis: if E_{i} is ever violated then, for at least one additional step, M_{i}^{l} implies M_{i}. This hypothesis is expressed formally as ⊧ C(E_{i})_{+v} ∧ C(M_{i}^{l}) ⇒ C(M_{i}), for some v; the hypothesis is weakest when v is taken to be the tuple of all relevant variables. Our proof rule is:

Theorem 1 (Decomposition Theorem). If, for i = 1, …, n,

(1) ⊧ ⋀_{j=1}^{n}C(M_{j}) ⇒ E_{i}

(2) (a) ⊧ C(E_{i})_{+v} ∧ C(M_{i}^{l}) ⇒ C(M_{i})

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

(b) ⊧ E_{i} ∧ M_{i}^{l} ⇒ M_{i}

then ⊧ ⋀_{i=1}^{n}M_{i}^{l} ⇒ ⋀_{i=1}^{n}M_{i}.

This theorem is a corollary of the Composition Theorem of Section 5.2 below.

In the GCD example, we want to use the theorem to prove M_{a}^{l} ∧ M_{b}^{l} ⇒ M_{a} ∧ M_{b}. (The component specifications are described in Section 4.1.) The abstract environment specification E_{a} asserts that b can change only when a < b, and that a is not changed by steps that change b. Thus,

E_{a} =^{Δ} □[(a < b) ∧ (a′ = a)]_{b}

The definition of E_{b} is analogous. We let v be ⟨a, b⟩.

In general, the environment and component specifications can have internal variables. The theorem also allows them to contain fairness conditions. However, the first hypothesis asserts that the E_{i} are implied by safety properties. In practice, this means that the theorem can be applied only when the E_{i} are safety properties. The examples of Section 2.2 lead us to expect such a restriction. Moreover, if the E_{i} have internal variables, we expect them to be simple history-determined variables [Abadi and Lamport 1994], so Proposition 2 of [Abadi and Lamport 1991] can be used to prove that the E_{i} are safety properties.

4.3.2 Verifying the Hypotheses. We now discuss how one verifies the hypotheses of the Decomposition Theorem, illustrating the method with the GCD example.

To prove the first hypothesis, one first eliminates the closure operators and existential quantifiers by using Propositions 1 and 2 and Proposition 2 of [Abadi and Lamport 1991]. This reduces the hypothesis to a condition of the form

⊧ ⋀_{i=1}^{n}(Init_{i} ∧ □[N_{i}]_{v_{i}}) ⇒ E_{i}  (10)

For interleaving representations, we can then use Proposition 6 to write ⋀_{i=1}^{n}(Init_{i}∧ □[N_{i}]_{v_{i}}) in canonical form. For noninterleaving representations, we apply (9). In either case, the proof of (10) is an implementation proof of the kind discussed in Section 3.2.

For the GCD example, the first hypothesis asserts that C(M_{a}) ∧ C(M_{b}) implies E_{a} and E_{b}. This differs from the third hypothesis of (1) in Section 2.1 because of the C’s. To verify the hypothesis, we can apply Proposition 1 to show that C(M_{a}) and C(M_{b}) are obtained by simply deleting the fairness conditions from M_{a} and M_{b}. Since N_{b} implies (a < b) ∧ (a′ = a), it is easy to see that C(M_{b}) implies E_{a}. It is equally easy to see that C(M_{a}) implies E_{b}. (In more complicated examples, E_{i} will not follow from C(M_{j}) for any single j.)

To prove part (a) of the second hypothesis, we first eliminate the +. For noninterleaving representations, this must be done with Proposition 3, as described in Section 3.5.1. For interleaving representations, we can apply Propositions 4 and 5, as described in Section 3.5.4. In either case, we can prove the resulting formula by first using Proposition 2 to eliminate quantifiers, using Proposition 1 to compute closures, and then performing a standard implementation proof with a refinement mapping.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Part (b) of the hypothesis also calls for a standard implementation proof, for which we use the same refinement mapping as in the proof of (a). Since E_{i} implies C(E_{i})_{+v} and M_{i}^{l} implies C(M_{i}^{l}), we can infer from part (a) that E_{i} ∧ M_{i}^{l} implies C(M_{i}). Thus proving part (b) requires verifying only the liveness part of M_{i}.

For the GCD example, we verify the two parts of the second hypothesis by proving C(E_{a})_{+⟨a, b⟩} ∧C(M_{a}^{l}) ⇒ C(M_{a}) and E_{a} ∧M_{a}^{l} ⇒ M_{a}; the proofs of the corresponding conditions for M_{b} are similar. We first observe that the initial condition of E_{a} is true, and that, since M_{a}^{l} is an interleaving representation, its next-state action N_{a}^{l} implies that no step changes both a and b, so C(M_{a}^{l}) implies Disjoint(a, b). Hence, applying Propositions 4 and 5, we reduce our task to proving C(E_{a}) ∧ C(M_{a}^{l}) ⇒ C(M_{a}) and E_{a} ∧ M_{a}^{l} ⇒ M_{a}. Applying Proposition 2 to remove the quantifier from C(M_{a}^{l}) and Proposition 1 to remove the C’s, we reduce proving C(E_{a}) ∧ C(M_{a}^{l}) ⇒ C(M_{a}) to proving

E_{a} ∧ Init_{a}^{l} ∧ □[N_{a}^{l}]_{⟨a, ai, pca⟩} ⇒ Init_{a} ∧ □[N_{a}]_{a}  (11)

Using simple logic and (11), we reduce proving E_{a} ∧ M_{a}^{l} ⇒ M_{a} to proving

E_{a} ∧ Init_{a}^{l} ∧ □[N_{a}^{l}]_{⟨a, ai, pca⟩} ∧ WF_{⟨a, ai, pca⟩}(N_{a}^{l}) ⇒ WF_{a}(N_{a})  (12)

We can use Proposition 6 to rewrite the left-hand sides of (11) and (12) in canonical form. The resulting conditions are in the usual form for a TLA implementation proof.

In summary, by applying our propositions in a standard sequence, we can use the Decomposition Theorem to reduce decompositional reasoning to ordinary TLA reasoning. This reduction may seem complicated for so trivial an example as the GCD program. However, it will be insignificant compared to the complexity of the complete proof in any realistic example, such as the one by Kurshan and Lamport [1993], discussed below.

4.3.3 The General Theorem. We sometimes need to prove the correctness of systems defined inductively. At induction stage N+1, the low- and high-level specifications are defined as the conjunctions of k copies of low- and high-level specifications of stage N, respectively. For example, a 2^{N+1}-bit multiplier is sometimes implemented by combining four 2^{N}-bit multipliers. We want to prove by induction on N that the stage N low-level specification implements the stage N high-level specification. For such a proof, we need a more general decomposition theorem whose conclusion at stage N can be used in proving the hypotheses at stage N +1. The appropriate theorem is:

Theorem 2 (General Decomposition Theorem). If, for i = 1, …, n,

(1) ⊧ C(E) ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ E_{i}

(2) (a) ⊧ C(E_{i})_{+v} ∧ C(M_{i}^{l}) ⇒ C(M_{i})

(b) ⊧ E_{i} ∧ M_{i}^{l} ⇒ M_{i}

(3) v is a tuple of variables including all the free variables of M_{i}

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

then

\begin{matrix}(a) & ⊧ C(E)_{+v} ∧ ⋀_{j=1}^{n}C(M_{j}^{l}) ⇒ ⋀_{j=1}^{n}C(M_{j}) and \\ (b) & ⊧ E ∧ ⋀_{j=1}^{n}M_{j}^{l} ⇒ ⋀_{j=1}^{n}M_{j}. \end{matrix}

Conclusion (b) of this theorem has the same form as hypothesis 2(b), with M_{i}^{l} and M_{i} replaced with conjunctions. To make the corresponding hypothesis 2(a) follow from conclusion (a), it suffices to prove ⋀_{j=1}^{n} C(M_{j}) ⇒ C(⋀_{j=1}^{n} M_{j}), since C(⋀_{j=1}^{n} M_{j}^{l}) ⇒ ⋀_{j=1}^{n} C(M_{j}^{l}) is always true.

The General Decomposition Theorem has been applied to the verification of an inductively defined multiplier circuit [Kurshan and Lamport 1993].

It can be shown that both versions of our decomposition theorem provide complete rules for verifying that one composition implies another. However, this result is of no significance. Decomposition can simplify a proof only if the proof can be decomposed, in the sense that each M_{i}^{l} implements the corresponding M_{i} under a simple environment assumption E_{i}. Our theorems are designed to handle those proofs that can be decomposed.

5. COMPOSING ASSUMPTION/GUARANTEE SPECIFICATIONS

5.1 The Form of an Assumption/Guarantee Specification

An assumption/guarantee specification asserts that a system guarantees M under the assumption that its environment satisfies E. As we saw in Section 2.2, this specification is expressed by the formula E −▷^{+} M, which means that, for any n, if the environment satisfies E through “time” n, then the system must satisfy M through “time” n+1.

Perhaps the most obvious form for an assumption/guarantee specification is E ⇒ M. The formula E ⇒ M is weaker than E −▷^{+} M, since it allows behaviors in which M is violated before E. However, an implementation could exploit this extra freedom only by predicting in advance that the environment will violate E. A system does not control its environment, so it cannot predict what the environment will do. The specifications E ⇒ M and E −▷^{+} M therefore allow the same implementations. We take E −▷^{+} M to be the form of assumption/guarantee specifications because this form leads to the simpler rules for composition.

As discussed in Section 2.2, composition works best when environment assumptions are safety properties. It can be shown that E −▷^{+} M is equivalent to C(E) −▷^{+} (C(M) ∧ (E ⇒ M)), so we can in principle convert any assumption/guarantee specification to one whose assumption is a safety property. (A similar observation appears in our earlier work [Abadi and Lamport 1993, Theorem 1].) However, this equivalence is of intellectual interest only. In practice, we write the environment assumption as a safety property and the system’s fairness guarantee as the conjunction of properties E_{L} ⇒ WF_{v}(A) and E_{L} ⇒ SF_{v}(A), where E_{L} is an environment fairness assumption. We can apply Proposition 1 to show that the resulting specification is machine closed because, if (P, L) is machine closed and L implies R, then (P, R) is also machine closed [Abadi and Lamport 1994, Proposition 3].

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

5.2 The Composition Theorem

Suppose we are given n devices, each with an assumption/guarantee specification E_{j} −▷^{+} M_{j}. To verify that the composition of these devices implements a higher-level assumption/guarantee specification E −▷^{+} M, we must prove ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j}) ⇒ (E −▷^{+} M). We use the following theorem:

Theorem 3 (Composition Theorem). If, for i = 1, …, n,

(1) ⊧ C(E) ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ E_{i}

(2) (a) ⊧ C(E)_{+v} ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ C(M)

(b) ⊧ E ∧ ⋀_{j=1}^{n}M_{j} ⇒ M

then ⊧ ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j}) ⇒ (E −▷^{+} M).

This theorem also allows us to prove conditional implementation results of the form G ∧ ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j}) ⇒ (E −▷^{+} M); we just let M_{1} equal G and E_{1} equal true, since true −▷^{+} G equals G. For interleaving specifications, we can in general prove only conditional implementation, where G includes disjointness conditions asserting that the outputs of different components do not change simultaneously.

The hypotheses of the Composition Theorem are similar to those of the Decomposition Theorem, and they are proved in much the same way. The major difference is that, for interleaving specifications, the orthogonality condition C(E) ⊥ C(M) does not follow from the form of the component specifications, but requires explicit disjointness assumptions.

Observe that the hypotheses have the form ⊧ P ∧ ⋀_{j=1}^{n} Q_{j} ⇒ R. Each formula P ∧ ⋀_{j=1}^{n} Q_{j} has the form of the specification of a complete system, with component specifications P, Q_{1}, …, Q_{n}. Thus, each hypothesis asserts that a complete system satisfies a property R. In other words, the theorem reduces reasoning about assumption/guarantee specifications to the kind of reasoning used for complete-system specifications.

Among the corollaries of the Composition Theorem are ones that allow us to prove that a lower-level specification implies a higher-level one. The simplest such result has, as its conclusion, ⊧ (E −▷^{+} M^{l}) ⇒ (E −▷^{+} M). This condition expresses the correctness of the refinement of a component with a fixed environment assumption.

Corollary 1. If E is a safety property and

(a) ⊧ E_{+v} ∧ C(M^{l}) ⇒ C(M)

(b) ⊧ E ∧ M^{l} ⇒ M

then ⊧ (E −▷^{+} M^{l}) ⇒ (E −▷^{+} M).

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

5.3 The Queue Example

The assumption/guarantee specification of the queue of Figure 2 is QE −▷^{+} QM , where QM and QE are defined in (7) and (8) of Section 4.1. We now compose two queues, as shown in Figure 7. The specifications of these queues are obtained from QE −▷^{+} QM by substitution; they are QE^{[1]} −▷^{+} QM^{[1]} and QE^{[2]} −▷^{+} QM^{[2]}. We want to show that their composition implements the (2N +1)-element queue specified by QE^{[dbl]} −▷^{+} QM^{[dbl]}. The obvious thing to try to prove is

(QE^{[1]} −▷^{+} QM^{[1]}) ∧ (QE^{[2]} −▷^{+} QM^{[2]}) ⇒ (QE^{[dbl]} −▷^{+} QM^{[dbl]}) (13)

We could prove this had we used a noninterleaving representation of the queue. However, (13) is not valid for an interleaving representation, for the following reason. The specification of the first queue does not mention o, and that of the second queue does not mention i. The conjunction of the two specifications allows an enqueue action of the first queue and a dequeue action of the second queue to happen simultaneously, a step that changes i.ack and o.snd simultaneously. But, in an interleaving representation, the (2N +1)-element queue’s guarantee does not allow such a step, so (13) must be invalid. Another problem with (13) is that the conjunction of the component queues’ specifications allows a step that changes z.snd and o.ack simultaneously. Such a step satisfies the (2N +1)-element queue’s environment assumption QE^{[dbl]}, which does not mention z, so (13) asserts that the next step must satisfy its guarantee QM^{[dbl]}. However, a step that changes both z.snd and o.ack violates the second component queue’s environment assumption QE^{[2]}, permitting the component queue to make arbitrary changes to o.snd in the next step. A similar problem is caused by simultaneous changes to i.snd and z.ack.

We already faced the problem of disallowing simultaneous changes to different components’ outputs in Section 4.2, where we decomposed an interleaving specification of a (2N +1)-element queue. There, the solution was to strengthen the next-state actions of the component queues and of the environment. This solution cannot be used if we want to compose preexisting specifications without modifying them. In this case, we prove that the composition implements the larger queue under the assumption that the outputs of two different components do not change simultaneously. Thus, we prove

G ∧ (QE^{[1]} −▷^{+} QM^{[1]}) ∧ (QE^{[2]} −▷^{+} QM^{[2]}) ⇒ (QE^{[dbl]} −▷^{+} QM^{[dbl]}) (14)

where G is the formula

G =^{Δ} Disjoint(⟨i.snd, o.ack⟩, ⟨z.snd, i.ack⟩, ⟨o.snd, z.ack⟩)

The proof is outlined in Figure 10.

6. CONCLUSION

We have developed a method for describing components of concurrent systems as TLA formulas. We have shown how to describe a complete system as the conjunction of component specifications and how to describe an open system as a formula E −▷^{+} M, where E and M are specifications of an environment component and a system component, respectively. Although the idea of reducing programming concepts to logic is old, our approach is new. Our style of writing specifications is direct and, we believe, practical.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

1. C(QE^{[dbl]}) ∧ C(G) ∧ C(QM^{[1]}) ∧ C(QM^{[2]}) ⇒ QE^{[1]} ∧ QE^{[2]} Proof: We use Propositions 2 and 1 to remove the quantifiers and closure operators from the left-hand side of the implication. The resulting formula then asserts that a complete system, consisting of the safety parts of the two queues (with their internal state visible) together with the environment, implements QE^{[1]} and QE^{[2]}. The proof of this formula is straightforward.

2. C(QE^{[dbl]})_{+⟨i, o, z⟩} ∧ C(QM^{[1]}) ∧ C(G) ∧ C(QM^{[2]}) ⇒ C(QM^{[dbl]})

2.1. C(G) ∧ C(QM^{[1]}) ∧ C(QM^{[2]}) ⇒ C(QE^{[dbl]}) ⊥ C(QM^{[dbl]})

2.1.1. C(IQM^{[1]}) ∧ C(IQM^{[2]}) ⇒ ∃ q_{1}, q_{2} : Init_{M}^{[1]} ∧ Init_{M}^{[2]}

Proof: Follows easily from Proposition 1 and the definitions. 2.1.2. C(QM^{[1]}) ∧ C(QM^{[2]}) ⇒ ∃ q_{1}, q_{2} : Init_{M}^{[1]} ∧ Init_{M}^{[2]}

Proof: 2.1.1 and Proposition 2 (since any predicate is a safety property). 2.1.3. Q.E.D.

Proof: 2.1.2, the definition of G, and Proposition 5 (since disjointness is a safety property).

2.2. C(QE^{[dbl]}) ∧ C(G) ∧ C(QM^{[1]}) ∧ C(QM^{[2]}) ⇒ C(QM^{[dbl]})

Proof: We use Propositions 2 and 1 to remove the quantifiers and closures from the formula. The resulting formula is proved when proving the safety part of step 3.

2.3. Q.E.D.

Proof: 2.1, 2.2, and Proposition 4.

3. QE^{[dbl]} ∧ G ∧ QM^{[1]} ∧ QM^{[2]} ⇒ QM^{[dbl]} Proof: A direct calculation shows that the left-hand side of the implication implies CDQ, the complete-system specification of the double queue. We already observed in Section 3.2 that CDQ implements CQ^{[dbl]}, which equals QE^{[dbl]} ∧ QM^{[dbl]}.

4. Q.E.D.

Proof: 1–3 and the Composition Theorem, substituting

M_{1} ← G  M_{2} ← QM^{[1]}  M_{3} ← QM^{[2]}  M ← QM^{[dbl]}
E_{1} ← true  E_{2} ← QE^{[1]}  E_{3} ← QE^{[2]}  E ← QE^{[dbl]}

Fig. 10. Proof sketch of (14).

We have also provided rules for proving properties of large systems by reasoning about their components. The Composition and Decomposition Theorems are rather simple, yet they allow fairness properties and hiding. They were preceded by results in a long list of publications, described next.

Like ours, most previous composition theorems were strong, in the sense that they could handle circularities for safety properties. Our approach differs from earlier ones in its general treatment of fairness and hiding. The first strong composition theorem we know is that of Misra and Chandy [1981], who considered safety properties of processes communicating by means of CSP primitives. They wrote assumption/guarantee specifications as Hoare triples containing assertions about history variables. Pandya and Joseph [1991] extended this approach to handle some liveness properties. Pnueli [1984] was the first to use temporal logic to write assumption/guarantee specifications. He had a strong composition theorem for safety properties with no hiding. To handle liveness, he wrote assumption/guarantee specifications with implication instead of −▷^{+}, so he did not obtain a strong composition theorem. Stark [1985] also wrote assumption/guarantee specifications as implications of temporal formulas and required that circularity be avoided. Our earlier work [Abadi and Lamport 1993] was semantic, in a more complicated model with agents. It lacked practical proof rules for handling fairness and hiding. Collette [1993] adapted this work to Unity. Abadi and Plotkin [1993] used a propositional logic with agents, and considered only safety properties.

Most previous papers were concerned only with composition of assumption/guarantee specifications, and lacked an analog of our Decomposition Theorem. An exception is the work of Berthet and Cerny [1988], who used decomposition in proving safety properties for finite-state automata.

So far, we have applied our Composition Theorem only to toy examples. Formal reasoning about systems is still rare, and it generally occurs on a case-by-case basis. When the specification of a component is used only to verify a specific system, there is no need for a general assumption/guarantee specification. For most practical applications, decomposition suffices. When decomposition does not suffice, the Composition Theorem makes reasoning about open systems almost as easy as reasoning about complete ones.

We have used our Decomposition Theorem with no difficulty on a few toy examples. However, we believe that its biggest payoff will be for systems that are too complex to verify easily by hand. The theorem makes it possible for decision procedures to do most of the work in verifying a system, even when these procedures cannot be applied to the whole system because its state space is very large or unbounded. This approach is currently being pursued in one substantial example: the mechanical verification of a multiplier circuit using a combination of TLA reasoning and mechanical verification with COSPAN [Kurshan and Lamport 1993]. Because it eliminates reasoning about the complete low-level system, the Decomposition Theorem is the key to this division of labor.

Acknowledgments

Karlis Cerans, Stephan Merz, Yuan Yu, and anonymous referees provided helpful comments on an earlier version.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

REFERENCES

Abadi, M. and Lamport, L. 1994. An old-fashioned recipe for real time. ACM Trans. Program.

Lang. Syst. 16, 5 (Sept.), 1543–1571. Abadi, M. and Lamport, L. 1993. Composing specifications. ACM Trans. Program. Lang.

Syst. 15, 1 (Jan.), 73–132. Abadi, M. and Lamport, L. 1991. The existence of refinement mappings. Theor. Comput.

Sci. 82, 2 (May), 253–284. Abadi, M. and Plotkin, G. 1993. A logical view of composition. Theor. Comput. Sci. 114, 1

(June), 3–30. Abramsky, S. and Jagadeesan, R. 1994. Games and full completeness for multiplicative linear

logic. J. Symb. Logic 59, 2 (June), 543–574. Alpern, B. and Schneider, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.),

181–185. Berthet, C. and Cerny, E. 1988. An algebraic model for asynchronous circuits verification.

IEEE Trans. Comput. 37, 7 (July), 835–847. Collette, P. 1993. Application of the composition principle to Unity-like specifications. In

TAPSOFT’93: Theory and Practice of Software Development, M.-C. Gaudel and J.-P. Jouannaud, Eds. Lecture Notes in Computer Science, vol. 668. Springer-Verlag, Berlin, 230–242.

Jones, C. B. 1983. Specification and design of (parallel) programs. In Information Processing 83: Proceedings of the IFIP 9th World Congress, R. E. A. Mason, Ed. North-Holland, Amsterdam, 321–332.

Kurshan, R. P. and Lamport, L. 1993. Verification of a multiplier: 64 bits and beyond. In Computer-Aided Verification, C. Courcoubetis, Ed. Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Berlin, 166–179. Proceedings of the 5th International Conference, CAV’93.

Lamport, L. 1994. The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 3

(May), 872–923. Lamport, L. 1989. A simple approach to specifying concurrent systems. Commun. ACM 32, 1

(Jan.), 32–45. Lamport, L. 1983. What good is temporal logic? In Information Processing 83: Proceedings of

the IFIP 9th World Congress, R. E. A. Mason, Ed. North-Holland, Amsterdam, 657–668. Mead, C. and Conway, L. 1980. Introduction to VLSI Systems. Addison-Wesley, Reading,

Mass., chap. 7. Misra, J. and Chandy, K. M. 1981. Proofs of networks of processes. IEEE Trans. Softw.

Eng. SE-7, 4 (July), 417–426. Pandya, P. K. and Joseph, M. 1991. P-A logic—a compositional proof system for distributed

programs. Distrib. Comput. 5, 1, 37–54. Pnueli, A. 1984. In transition from global to modular temporal reasoning about programs. In

Logics and Models of Concurrent Systems, K. R. Apt, Ed. NATO ASI Series, Springer-Verlag, Berlin, 123–144.

Pnueli, A. 1981. The temporal semantics of concurrent programs. Theor. Comput. Sci. 13,

45–60. Stark, E. W. 1985. A proof technique for rely/guarantee properties. In Foundations of Software

Technology and Theoretical Computer Science, S. N. Maheshwari, Ed. Lecture Notes in Computer Science, vol. 206. Springer-Verlag, Berlin, 369–391.

Zave, P. and Jackson, M. 1993. Conjunction as composition. ACM Trans. Softw. Eng. Method. 2, 4 (Oct.), 379–411.

Received December 1993; revised July 1994 and January 1995; accepted January 1995

APPENDIX

An appendix to this article is available in electronic form (PostScript^{TM}). Any of the following methods may be used to obtain it; or see the inside back cover of a current issue for up-to-date instructions.

—By anonymous ftp from acm.org, file [pubs.journals.toplas.append]p1532.ps

—Send electronic mail to mailserve@acm.org containing the line

send [anonymous.pubs.journals.toplas.append]p1532.ps

—By Gopher from acm.org

—By anonymous ftp from ftp.cs.princeton.edu, file pub/toplas/append/p1532.ps

—Hardcopy from Article Express, for a fee: phone 800-238-3458, fax 201-216-8526, or write P.O. Box 1801, Hoboken NJ 07030; and request acm-toplas-appendix-

1532.

Conjoining Specifications · A–1

this document is the appendix to the following paper:

Conjoining Specifications

MARTÍN ABADI and LESLIE LAMPORT Digital Equipment Corporation

ACM Transactions on Programming Languages and Systems 17, 3 (May, 1995)

We now prove our propositions and theorems. Section A introduces some definitions and notation required for the proofs, and explains our structured proof notation. The proofs are in Section B.

APPENDIX A. DEFINITIONS

A1 Additional Semantic Notions

As before, ∘ denotes concatenation of sequences, and angle brackets ⟨ ⟩ are used to form sequences. We write σ|_{n} for the finite behavior consisting of the first n states of a behavior σ. In particular, σ|_{0} is the empty sequence ⟨ ⟩, which satisfies every formula. We write σ_{n} for the nth state of behavior σ, so σ equals ⟨σ_{1}, σ_{2}, … ⟩. When σ is finite, we write last(σ) for its last state, and |σ| for its length.

We let [[e]] denote the meaning of an expression e. When e is a state function, [[e]] is a mapping from states to values; in the special case when e is a state predicate, [[e]] is a mapping from states to truth values. When e is an action, [[e]] is a mapping from pairs of states to truth values. When e is a temporal formula, [[e]] is a mapping from behaviors to truth values. We extended this mapping to finite behaviors by letting [[e]](ρ) = true iff [[e]](σ) = true for some σ that extends ρ. In all cases, we let u ⊧ e mean [[e]](u) = true. If F is a temporal formula and σ a behavior, then σ ⊧ C(F) iff σ|_{n} ⊧ F for all n. Hence, [[C(F)]](ρ) = [[F]](ρ) for any finite behavior ρ.

If s and t are states and x is a tuple of variables, we write s =_{x} t when s and t are identical except possibly for the value they assign to the tuple x. In other words, s =_{x} t iff [[y]](s) = [[y]](t) for every variable y not in the tuple x. We extend this notion to behaviors, and write σ =_{x} τ iff σ_{n} =_{x} τ_{n} for all n > 0.

The stutter-free version of a behavior is the behavior obtained by removing from it all finite repetitions of states; thus, the stutter-free version of σ ∘ ⟨s, s⟩ ∘ τ equals the stutter-free version of σ ∘ ⟨s⟩ ∘ τ. Two behaviors are stuttering equivalent iff they have the same stutter-free version. Every TLA formula F is invariant under stuttering, in the sense that [[F]](σ) = [[F]](τ) for any two stuttering-equivalent behaviors σ and τ. More generally, [[F]](σ) = [[F]](τ) if there is a behavior τ̂ stuttering equivalent to σ such that [[y]](τ̂_{n}) = [[y]](τ_{n}) for all n > 0 and all variables

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

\begin{matrix}c \\ ◯ \end{matrix}1995 ACM

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

A–2 · Martín Abadi and Leslie Lamport

y occurring free in F.

We write σ ≃_{x} τ when σ̂ =_{x} τ̂ for some σ̂ and τ̂ stuttering equivalent to σ and τ, respectively. If F is a TLA formula and σ a behavior, we let [[∃ ∃ ∃ ∃ ∃ ∃ x : F]](σ) = true iff there exists a behavior τ such that σ ≃_{x} τ and [[F]](τ) = true. Equivalently, since F is invariant under stuttering, [[∃ ∃ ∃ ∃ ∃ ∃ x : F]](σ) = true iff there exist behaviors σ̂ and τ̂ such that σ̂ is stuttering equivalent to σ, σ̂ =_{x} τ̂, and [[F]](τ̂) = true.

An operator H on formulas is superdiagonal iff ⊧ A ⇒ H(A) for all A in its domain. For example, C is superdiagonal. As usual, an operator H is monotonic iff ⊧ A ⇒ B implies ⊧ H(A) ⇒ H(B) for all A and B. Antimonotonicity is defined similarly, with the second implication reversed.

A2 Proof Notation

Reliable reasoning about specifications depends on the correctness of the underlying logical proofs. Even a minor error, such as the omission of a hypothesis in a proposition, could allow one to “prove” the correctness of an incorrect implementation. To avoid such errors, we provide detailed, hierarchically structured proofs.

In our proof notation, the theorem to be proved is statement ⟨0⟩1. The proof of statement ⟨i⟩j is either an ordinary paragraph-style proof or the sequence of statements ⟨i+1⟩1, ⟨i+1⟩2, … and their proofs. (The absence of a proof means that the statement follows easily from definitions, previous statements, and assumptions.) Within a proof, ⟨k⟩l denotes the most recent statement with that number. A statement has the form

Assume: Assump Prove: Goal which is abbreviated to Goal if there is no assumption. The assertion Q.E.D. in statement number ⟨i + 1⟩k of the proof of statement ⟨i⟩j denotes the goal of statement ⟨i⟩j. The statement

Case: Assump is an abbreviation for

Assume: Assump Prove: Q.E.D. Within the proof of statement ⟨i⟩j, assumption ⟨i⟩ denotes that statement’s assumption, and ⟨i⟩:k denotes the assumption’s k^{th} item.

We recommend that proofs be read hierarchically, from the top level down. To read the proof of a long level-k step: (i) read the level-(k+1) statements that comprise its proof, together with the proof of the final Q.E.D. step (which is usually a short paragraph), and (ii) read the proof of each level-(k+1) step, in any desired order.

APPENDIX B. PROOFS

Results are organized in groups that roughly correspond to their subject and to the position of the corresponding discussion in the text.

Our proofs employ many lemmas. We omit the proofs of some of the simpler ones. We also omit the proof of Proposition 1, which is given in [Abadi and Lamport 1994].

B1 Properties of −▷ and −▷^{+}

The proofs of most of these properties are straightforward and are omitted. Some of the basic arguments about −▷ can be found in [Abadi and Plotkin 1993].

Lemma 1. If P, Q, and R are safety properties, then 1. P −▷ Q and P −▷^{+} Q are safety properties.

2. ⊧ P ⇒ (Q −▷ R) if and only if ⊧ P ∧ Q ⇒ R.

Lemma 2. For any properties P and Q, 1. ⊧ (P −▷ Q) = (C(P) −▷ C(Q)) ∧ (P ⇒ Q)

2. ⊧ (P −▷^{+} Q) = (C(P) −▷^{+} C(Q)) ∧ (P ⇒ Q)

Lemma 3. For any properties P and Q, 1. ⊧ P ∧ (P −▷ Q) ⇒ Q

2. ⊧ P ∧ (P −▷^{+} Q) ⇒ Q

Lemma 4. If P and Q are safety properties, then ⊧ (P −▷ Q) ∧ (Q −▷ P) ⇒ ((P ∨ Q) −▷ (P ∧ Q))

Lemma 5. If P_{i} and Q_{i} are safety properties, for i = 1, …, n, then

⊧ ⋀_{i=1}^{n}(P_{i} −▷^{+} Q_{i}) ⇒ ((⋀_{i=1}^{n}P_{i}) −▷^{+} (⋀_{i=1}^{n}Q_{i}))

Lemma 6. If P is a safety property and Q is any property, then

⊧ (P −▷^{+} Q) = ((Q −▷ P) −▷ Q)

Lemma 7. Assume: 1. P, Q, and R are safety properties.

2. ⊧ Q ∧ R ⇒ P

Prove: ⊧ (P −▷^{+} Q) ⇒ (R −▷^{+} Q)

⟨1⟩1. ⊧ (Q −▷ R) ⇒ (Q −▷ P)

⟨2⟩1. ⊧ Q ∧ (Q −▷ R) ⇒ R

Proof: Lemma 3(1). ⟨2⟩2. ⊧ Q ∧ (Q −▷ R) ⇒ (Q ∧ R)

Proof: ⟨2⟩1 and propositional logic. ⟨2⟩3. ⊧ Q ∧ (Q −▷ R) ⇒ P

Proof: ⟨2⟩2 and assumption ⟨0⟩:2. ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩3, assumption ⟨0⟩:1, and Lemma 1(2).

⟨1⟩2. ⊧ (P −▷^{+} Q) ∧ (Q −▷ P) ⇒ Q

Proof: Assumption ⟨0⟩:1, Lemma 6, and Lemma 3(1).

⟨1⟩3. ⊧ (P −▷^{+} Q) ∧ (Q −▷ R) ⇒ Q

Proof: ⟨1⟩2 and ⟨1⟩1.

⟨1⟩4. ⊧ (P −▷^{+} Q) ⇒ ((Q −▷ R) −▷ Q)

Proof: ⟨1⟩3, assumption ⟨0⟩:1, and Lemma 1. ⟨1⟩5. Q.E.D.

Proof: ⟨1⟩4, assumption ⟨0⟩:1, and Lemma 6.

B2 Closure and Existential Quantification These results are useful for reasoning about the closure of a quantified formula. This reasoning can be difficult because C and ∃ ∃ ∃ ∃ ∃ ∃ do not commute.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Lemma 8. For any property M and tuple of variables x,

⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x : C(M)) = C(∃ ∃ ∃ ∃ ∃ ∃ x : M)

⟨1⟩1. ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x : M) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : C(M))

Proof: C is superdiagonal and both C and ∃ ∃ ∃ ∃ ∃ ∃x are monotonic. ⟨1⟩2. ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x : C(M)) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : M)

⟨2⟩1. ⊧ M ⇒ ∃ ∃ ∃ ∃ ∃ ∃ x : M

Proof: ∃ ∃ ∃ ∃ ∃ ∃ is superdiagonal. ⟨2⟩2. ⊧ C(M) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : M)

Proof: ⟨2⟩1 and the monotonicity of C. ⟨2⟩3. ⊧ (∃ ∃ ∃ ∃ ∃ ∃ x : C(M)) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : M)

Proof: ⟨2⟩2, since x does not occur free in C(∃ ∃ ∃ ∃ ∃ ∃ x : M). ⟨2⟩4. Q.E.D.

Proof:⟨2⟩3 and the monotonicity and idempotence of C. ⟨1⟩3. Q.E.D.

Lemma 9. Assume: x_{i} is a tuple of variables, and no variable in x_{i} occurs free in M_{j}, for all

i, j ∈ {1, …, n} with i ≠ j.

Prove: ⊧ ⋀_{i} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1}, …, x_{n} : ⋀_{i} C(M_{i}))

The proof is by induction on n, setting apart the cases for n = 1 and n = 2. ⟨1⟩1. Case: n = 1

Proof: Immediate from Lemma 8. ⟨1⟩2. Case: n=2

Let: A =^{Δ} C(∃ ∃ ∃ ∃ ∃ ∃ x_{1}, x_{2} : C(M_{1}) ∧ C(M_{2}))

⟨2⟩1. ⊧ C(M_{1}) ∧ C(M_{2}) ⇒ A

Proof: Predicate logic, since C is superdiagonal. ⟨2⟩2. ⊧ C(M_{1}) ⇒ (C(M_{2}) −▷ A)

Proof: ⟨2⟩1 and Lemma 1(2). ⟨2⟩3. ⊧ M_{1} ⇒ (C(M_{2}) −▷ A)

Proof: ⟨2⟩2, since C is superdiagonal. ⟨2⟩4. ⊧ (∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) ⇒ (C(M_{2}) −▷ A)

Proof: ⟨2⟩3 and the hypothesis that no variable of x_{1} occurs free in M_{2}. ⟨2⟩5. ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) ⇒ (C(M_{2}) −▷ A)

Proof: ⟨2⟩4 and the monotonicity and idempotence of C, since A is closed by definition and C(M_{2}) −▷ A is closed by Lemma 1(1).

⟨2⟩6. ⊧ C(M_{2}) ⇒ (C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) −▷ A)

Proof: ⟨2⟩5 and two applications of Lemma 1(2) ⟨2⟩7. ⊧ M_{2} ⇒ (C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) −▷ A)

Proof: ⟨2⟩6, since C is superdiagonal. ⟨2⟩8. ⊧ (∃ ∃ ∃ ∃ ∃ ∃ x_{2} : M_{2}) ⇒ (C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) −▷ A)

Proof: ⟨2⟩7 and predicate logic. ⟨2⟩9. ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x_{2} : M_{2}) ⇒ (C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} : M_{1}) −▷ A)

Proof: ⟨2⟩8, Lemma 1(1), and the monotonicity and idempotence of C. ⟨2⟩10. Q.E.D.

Proof: ⟨2⟩9 and Lemma 1(2). ⟨1⟩3. Case: n > 2

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Assume: ⊧ ⋀_{i=1}^{n−1} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n−1} : ⋀_{i=1}^{n−1} C(M_{i}))

Prove: ⊧ ⋀_{i=1}^{n} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n} : ⋀_{i=1}^{n} C(M_{i}))

Proof: ⋀_{i=1}^{n} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i})

⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n−1} : ⋀_{i=1}^{n−1} C(M_{i})) ∧ C(∃ ∃ ∃ ∃ ∃ ∃ x_{n} : M_{n})

by assumption ⟨1⟩ = C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n−1} : C(⋀_{i=1}^{n−1} C(M_{i}))) ∧ C(∃ ∃ ∃ ∃ ∃ ∃ x_{n} : M_{n})

a conjunction of safety properties is a safety property ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n} : C(⋀_{i=1}^{n−1} C(M_{i})) ∧ C(M_{n}))

by ⟨1⟩2

= C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n} : ⋀_{i=1}^{n} C(M_{i}))

a conjunction of safety properties is a safety property

⟨1⟩4. Q.E.D.

Proposition 2. Assume: 1. x_{i} is a tuple of variables, and no variable in x_{i} occurs free in M or

M_{j}, for all i, j ∈ {1, …, n} with i ≠ j

2. ⊧ ⋀_{i=1}^{n} C(M_{i}) ⇒ ∃ ∃ ∃ ∃ ∃ ∃ x : C(M)

Prove: ⊧ ⋀_{i=1}^{n} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : M)

Proof: ⋀_{i=1}^{n} C(∃ ∃ ∃ ∃ ∃ ∃ x_{i} : M_{i}) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n} : ⋀_{i=1}^{n} C(M_{i})) by Lemma 9 and assumption ⟨0⟩:1 ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x_{1} … x_{n} : ∃ ∃ ∃ ∃ ∃ ∃ x : C(M)) by assumption ⟨0⟩:2 and the monotonicity of ∃ ∃ ∃ ∃ ∃ ∃ and C = C(∃ ∃ ∃ ∃ ∃ ∃ x : C(M)) by assumption ⟨0⟩:1 = C(∃ ∃ ∃ ∃ ∃ ∃ x : M) by Lemma 8.

B3 Properties of + Lemma 10. For any state function f, if P is a safety property, then P_{+f} is a safety property.

Proof: By the definition of safety properties, it suffices to: Assume: 1. P a safety property.

2. ∀n : σ|_{n} ⊧ P_{+f}

Prove: σ ⊧ P_{+f} ⟨1⟩1. Case: ∀n : σ|_{n} ⊧ P

Proof: Assumption ⟨0⟩:1. ⟨1⟩2. Case: ∃ ∃ ∃ ∃ ∃ ∃n : ¬(σ|_{n} ⊧ P)

⟨2⟩1. Choose the largest m such that σ|_{m} ⊧ P.

Proof: m exists since σ|_{0} ⊧ P is true for any σ and P. ⟨2⟩2. ∀n > m : [[f]](σ_{n}) = [[f]](σ_{m+1})

Proof: ⟨2⟩1, assumption ⟨0⟩:2, and the definition of P_{+f}. ⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and the definition of P_{+f}. ⟨1⟩3. Q.E.D.

Lemma 11. Assume: 1. P and Q are safety properties.

2. the tuple x includes all the free variables of Q.

Prove: ⊧ (P_{+x} −▷ Q) = (P −▷^{+} Q)

⟨1⟩1. ⊧ (P_{+x} −▷ Q) ⇒ (P −▷^{+} Q)

By assumption ⟨0⟩:1, Lemma 1(1), and the definition of −▷^{+}, it suffices to: Assume: 1. For all n, σ|_{n} ⊧ (P_{+x} −▷ Q)

2. σ|_{n−1} ⊧ P

Prove: σ|_{n} ⊧ Q ⟨2⟩1. σ|_{n} ⊧ P_{+x}

Proof: By assumption ⟨1⟩:2 and the definition of P_{+x}. ⟨2⟩2. Q.E.D.

Proof: ⟨2⟩1 and assumption ⟨1⟩:1.

⟨1⟩2. ⊧ (P −▷^{+} Q) ⇒ (P_{+x} −▷ Q)

By assumption ⟨0⟩:1, Lemmas 10 and 1(1), and the definition of −▷, it suffices to: Assume: 1. For all n, σ|_{n} ⊧ (P −▷^{+} Q)

2. σ|_{n} ⊧ P_{+x}

Prove: σ|_{n} ⊧ Q ⟨2⟩1. Choose m ≤ n such that

1. σ|_{m} ⊧ P

2. ∀p : m < p ≤ n ⇒ [[x]](σ_{p}) = [[x]](σ_{m+1}) Proof: Assumption ⟨1⟩:2.

⟨2⟩2. σ|_{m+1} ⊧ Q

Proof: ⟨2⟩1.1 and assumption ⟨1⟩:1. ⟨2⟩3. Q.E.D.

Proof: ⟨2⟩2, ⟨2⟩1.2, and assumption ⟨0⟩:2, since Q is invariant under stuttering.

⟨1⟩3. Q.E.D.

Lemma 12. Assume: 1. P, Q, and R are safety properties.

2. ⊧ R_{+f} ∧ P ⇒ Q

Prove: ⊧ (R −▷^{+} P) ⇒ (R −▷^{+} Q)

⟨1⟩1. ⊧ R −▷^{+} R_{+f}

By assumption ⟨0⟩:1 and Lemmas 10 and 1, it suffices to: Assume: σ|_{n} ⊧ R Prove: σ|_{n+1} ⊧ R_{+f} ⟨2⟩1. σ|_{n+1} ∘ ⟨σ_{n+1}, σ_{n+1}, …⟩ ⊧ R_{+f}

Proof: The definition of R_{+f}. ⟨2⟩2. Q.E.D.

⟨1⟩2. Q.E.D.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Proof: (R −▷^{+} P) \begin{matrix}⇒ & (R −▷^{+} P) ∧ (R −▷^{+} R_{+f}) \\ & by ⟨1⟩1 \\ ⇒ & (R −▷^{+} (P ∧ R_{+f})) \\ & by assumption ⟨0⟩:1 and Lemmas 5 and 10 \\ ⇒ & (R −▷^{+} Q) \\ & by assumption ⟨0⟩:2 and monotonicity of −▷^{+} in \\ & its second argument. \end{matrix}

Lemma 13. Assume: No variable of the tuple x occurs free in v. Prove: ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P_{+v}) = (∃ ∃ ∃ ∃ ∃ ∃x : P)_{+v}

⟨1⟩1. ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P_{+v}) ⇒ (∃ ∃ ∃ ∃ ∃ ∃x : P)_{+v} Assume: σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P_{+v}) Prove: σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P)_{+v} ⟨2⟩1. Choose σ̂ such that σ̂ ≃_{x} σ and σ̂ ⊧ P_{+v}.

Proof: Assumption ⟨1⟩ and the definition of ∃ ∃ ∃ ∃ ∃ ∃. ⟨2⟩2. Case: σ̂ ⊧ P

⟨3⟩1. σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P)

Proof: ⟨2⟩1 and case assumption ⟨2⟩. ⟨3⟩2. Q.E.D.

Proof: ⟨3⟩1 and the definition of (…)_{+v}. ⟨2⟩3. Case: There exists ρ̂ and τ̂ such that σ̂ = ρ̂∘ τ̂, ρ̂ ⊧ P, and τ̂ ⊧ □ [false]_{v}.

⟨3⟩1. Choose ρ and τ such that σ = ρ ∘ τ, ρ ≃_{x} ρ̂, and τ ≃_{x} τ̂.

Proof: ⟨2⟩1 and case assumption ⟨2⟩. ⟨3⟩2. ρ ⊧ ∃ ∃ ∃ ∃ ∃ ∃x : P

Proof: ⟨3⟩1 (which asserts ρ ≃_{x} ρ̂) and case assumption ⟨2⟩ (which asserts ρ̂ ⊧ P).

⟨3⟩3. τ ⊧ □ [false]_{v} Proof: ⟨3⟩1 (which asserts τ ≃_{x} τ̂), case assumption ⟨2⟩ (which asserts τ̂ ⊧ □ [false]_{v}), and assumption ⟨0⟩.

⟨3⟩4. Q.E.D.

Proof: ⟨3⟩1 (which asserts σ = ρ ∘ τ), ⟨3⟩2, ⟨3⟩3, and the definition of (…)_{+v}.

⟨2⟩4. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, ⟨2⟩3, and the definition of (…)_{+v}. ⟨1⟩2. ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P)_{+v} ⇒ (∃ ∃ ∃ ∃ ∃ ∃x : P_{+v}) Assume: σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P)_{+v} Prove: σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P_{+v})

⟨2⟩1. Case: σ ⊧ (∃ ∃ ∃ ∃ ∃ ∃x : P)

Proof: Immediate, since ⊧ P ⇒ P_{+v} and ∃ ∃ ∃ ∃ ∃ ∃ is monotonic. ⟨2⟩2. Case: There exist ρ and τ such that σ = ρ ∘ τ, ρ ⊧ ∃ ∃ ∃ ∃ ∃ ∃x : P, and τ ⊧

□ [false]_{v}.

⟨3⟩1. Choose ρ̂ such that ρ̂ ≃_{x} ρ and ρ̂ ⊧ P.

Proof: Case assumption ⟨2⟩ and the definition of ∃ ∃ ∃ ∃ ∃ ∃. ⟨3⟩2. ρ̂∘ τ ⊧ P_{+v}

Proof: ⟨3⟩1, case assumption ⟨2⟩ (which asserts τ ⊧ □ [false]_{v}), and the definition of (…)_{+v}.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

⟨3⟩3. Q.E.D.

Proof: ⟨3⟩1, ⟨3⟩2, and case assumption ⟨2⟩, which imply ρ̂∘ τ ≃_{x} σ. ⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and the definition of (…)_{+v}. ⟨1⟩3. Q.E.D.

Lemma 14. If s is a variable that does not occur in Init, N, w, or v, and

Înit =^{Δ} (Init ∧ (s = 0)) ∨ (¬Init ∧ (s = 1))
N̂ =^{Δ} \begin{matrix}∨ (s = 0) ∧ \begin{matrix}∨ (s′ = 0) ∧ (N ∨ (w′ = w)) \\ ∨ (s′ = 1) ∧ ¬(N ∨ (w′ = w)) \end{matrix} \\ ∨ (s = 1) ∧ (s′ = 1) ∧ (v′ = v) \end{matrix}

then ⊧ (Init ∧ □[N]_{w})_{+v} = ∃ ∃ ∃ ∃ ∃ ∃s : Înit ∧ □[N̂]_{⟨w, v, s⟩}.

⟨1⟩1. ⊧ (Init ∧ □[N]_{w})_{+v} ⇒ ∃ ∃ ∃ ∃ ∃ ∃s : Înit ∧ □[N̂]_{⟨w, v, s⟩} Assume: σ ⊧ (Init ∧ □[N]_{w})_{+v} Prove: σ ⊧ ∃ ∃ ∃ ∃ ∃ ∃s : Înit ∧ □[N̂]_{⟨w, v, s⟩}

Let: σ̂ be the behavior such that σ̂ =_{s} σ and, for all n > 0: [[s]](σ̂_{n}) =^{Δ} if σ|_{n} ⊧ (Init ∧ □[N]_{w}) then 0 else 1

⟨2⟩1. σ̂ ⊧ Înit ∧ □[N̂]_{⟨w, v, s⟩}

⟨3⟩1. σ̂ ⊧ Înit Proof: The definitions of σ̂ and Înit, assumption ⟨1⟩, and the hypothesis that s does not occur in Init.

⟨3⟩2. σ̂ ⊧ □[N̂]_{⟨w, v, s⟩}

⟨4⟩1. Case: σ ⊧ Init ∧ □[N]_{w}

⟨5⟩1. σ̂ ⊧ □[(s = 0) ∧ (s′ = 0) ∧ (N ∨ (w′ = w))]_{⟨w, v, s⟩} Proof: The definition of σ̂, case assumption ⟨4⟩, and the hypothesis that s does not occur in N or w.

⟨5⟩2. Q.E.D.

Proof: ⟨5⟩1 and the definition of N̂. ⟨4⟩2. Case: σ |̸= Init

⟨5⟩1. σ ⊧ □ [false]_{v} Proof: Case assumption ⟨4⟩, assumption ⟨1⟩, and the definition of (…)_{+v}.

⟨5⟩2. σ̂ ⊧ □ (s = 1) ∧ □ [false]_{v}.

Proof: ⟨5⟩1 and the definition of σ̂. ⟨5⟩3. Q.E.D.

Proof: ⟨5⟩2 and the definition of N̂. ⟨4⟩3. Case: σ ⊧ Init and σ |̸= Init ∧ □[N]_{w}.

⟨5⟩1. Choose ρ and τ with |ρ| > 0 such that 1. σ = ρ ∘ τ,

2. ρ ⊧ Init ∧ □[N]_{w}

3. ρ ∘ ⟨τ_{1}⟩ |̸= □[N]_{w}

4. τ ⊧ □ [false]_{v} Proof: Case assumption ⟨4⟩, assumption ⟨1⟩, and the definition of (…)_{+v}.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

⟨5⟩2. Choose ρ̂ and τ̂ such that σ̂ = ρ̂∘ τ̂, ρ̂ =_{s} ρ, and τ̂ =_{s} τ.

Proof: The definition of σ̂ and ⟨5⟩1.1. ⟨5⟩3. ρ̂ ⊧ □[(s = 0) ∧ (s′ = 0) ∧ (N ∨ (w′ = w))]_{⟨w, v, s⟩}

Proof: The definition of σ̂, ⟨5⟩1.2, ⟨5⟩2, and the hypothesis that s does not occur in N or w.

⟨5⟩4. ⟨last(ρ̂), τ̂_{1}⟩ ⊧ (s = 0) ∧ (s′ = 1) ∧ ¬N ∧ (w′ ≠ w)

Proof: The definition of σ̂, ⟨5⟩1.3, ⟨5⟩2, and the hypothesis that s does not occur in N or w.

⟨5⟩5. τ̂ ⊧ □ (s = 1) ∧ □ [false]_{v} Proof: The definition of σ̂,, ⟨5⟩1.4, ⟨5⟩2, and the hypothesis that s does not occur in v.

⟨5⟩6. Q.E.D.

Proof: ⟨5⟩2, ⟨5⟩3, ⟨5⟩4, and ⟨5⟩5, and the definition of N̂. ⟨4⟩4. Q.E.D.

Proof: ⟨4⟩1, ⟨4⟩2, ⟨4⟩3, assumption ⟨1⟩, and the definition of (…)_{+v}. ⟨3⟩3. Q.E.D.

⟨2⟩2. Q.E.D.

Proof: The definition of σ̂, ⟨2⟩1, and the definition of ∃ ∃ ∃ ∃ ∃ ∃.

⟨1⟩2. ⊧ ∃ ∃ ∃ ∃ ∃ ∃s : Înit ∧ □[N̂]_{⟨w, v, s⟩} ⇒ (Init ∧ □[N]_{w})_{+v} Assume: σ ⊧ ∃ ∃ ∃ ∃ ∃ ∃s : Înit ∧ □[N̂]_{⟨w, v, s⟩} Prove: σ ⊧ (Init ∧ □[N]_{w})_{+v}

⟨2⟩1. Choose σ̂ such that σ̂ ≃_{s} σ and σ̂ ⊧ Înit ∧ □[N̂]_{⟨w, v, s⟩}.

Proof: Assumption ⟨1⟩ and the definition of ∃ ∃ ∃ ∃ ∃ ∃. ⟨2⟩2. σ̂ ⊧ (Init ∧ □[N]_{w})_{+v}

⟨3⟩1. Case: σ̂ ⊧ □ (s = 0)

⟨4⟩1. σ̂ ⊧ (Init ∧ □[N]_{w})

Proof: ⟨2⟩1, case assumption ⟨3⟩, and the definitions of Înit and N̂. ⟨4⟩2. Q.E.D.

Proof: ⟨4⟩1, since the operator (…)_{+v} is superdiagonal. ⟨3⟩2. Case: σ̂ ⊧ □ (s = 1)

⟨4⟩1. σ̂ ⊧ □ [false]_{v}

Proof: ⟨2⟩1, the definition of N̂, and case assumption ⟨3⟩. ⟨4⟩2. Q.E.D.

Proof: ⟨4⟩1 and the definition of (…)_{+v}. ⟨3⟩3. Case: σ̂ |̸= □ (s = 0) and σ̂ |̸= □ (s = 1)

⟨4⟩1. Choose ρ̂ and τ̂ with |ρ̂| > 0 such that 1. σ̂ = ρ̂∘ τ̂

2. ρ̂ ⊧ □ (s = 0)

3. τ̂ ⊧ □ (s = 1), Proof: Case assumption ⟨3⟩, ⟨2⟩1, and the definitions of Înit and N̂.

⟨4⟩2. ρ̂ ⊧ (Init ∧ □[N]_{w})

Proof: ⟨2⟩1, ⟨4⟩1.2, and the definitions of Înit and N̂. ⟨4⟩3. τ̂ ⊧ □ [false]_{v}

Proof: ⟨2⟩1, ⟨4⟩1.3, and the definition of N̂. ⟨4⟩4. Q.E.D.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Proof: ⟨4⟩1.1, ⟨4⟩2, ⟨4⟩3, ⟨3⟩, and the definition of (…)_{+v}.

⟨3⟩4. Q.E.D. ⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and the hypothesis that s does not occur in Init, N, w, or v.

⟨1⟩3. Q.E.D.

Proposition 3. If x is a tuple of variables none of which occurs in v, and s is a variable that does not occur in Init, N, w, v, or x, and

Înit =^{Δ} (Init ∧ (s = 0)) ∨ (¬Init ∧ (s = 1))
N̂ =^{Δ} \begin{matrix}∨ (s = 0) ∧ \begin{matrix}∨ (s′ = 0) ∧ (N ∨ (w′ = w)) \\ ∨ (s′ = 1) ∧ ¬(N ∨ (w′ = w)) \end{matrix} \\ ∨ (s = 1) ∧ (s′ = 1) ∧ (v′ = v) \end{matrix}

then ⊧ (∃ ∃ ∃ ∃ ∃ ∃ x : Init ∧ □[N]_{w})_{+v} = ∃ ∃ ∃ ∃ ∃ ∃ x, s : Înit ∧ □[N̂]_{⟨w, v, s⟩}.

Proof: Follows immediately from Lemmas 13 and 14.

B4 Properties of ⊥

Lemma 15.

1. For any properties P and Q, ⊧ P ⊥ Q = C(P) ⊥ C(Q).

2. If P and Q are safety properties, then ⊧ P ⊥ Q = (P ∧ Q) −▷^{+} (P ∨ Q).

Lemma 16. For any properties P and Q,

⊧ (P −▷^{+} Q) = (P −▷ Q) ∧ (P ⊥ Q)

⟨1⟩1. Case: P and Q safety properties

⟨2⟩1. ⊧ (P −▷^{+} Q) ⇒ (P −▷ Q) ∧ (P ⊥ Q)

⟨3⟩1. ⊧ (P −▷^{+} Q) ⇒ (P −▷ Q)

Proof: Obvious from the definitions of −▷ and −▷^{+}.

⟨3⟩2. ⊧ (P −▷^{+} Q) ⇒ (P ⊥ Q)

Proof: Lemma 15(2), since −▷^{+} is monotonic in its second argument and antimonotonic in its first.

⟨3⟩3. Q.E.D.

⟨2⟩2. ⊧ (P −▷ Q) ∧ (P ⊥ Q) ⇒ (P −▷^{+} Q)

⟨3⟩1. ⊧ (P −▷ Q) ∧ (P ⊥ Q) ∧ (Q −▷ P) ⇒ Q Proof: (P ⊥ Q) ∧ (P −▷ Q) ∧ (Q −▷ P) = (((P ∨ Q) −▷ (P ∧ Q)) −▷ (P ∨ Q)) ∧ (P −▷ Q) ∧ (Q −▷ P) case assumption ⟨1⟩, Lemma 15(2), and Lemma 6 ⇒ (((P ∨ Q) −▷ (P ∧ Q)) −▷ (P ∨ Q)) ∧ ((P ∨ Q) −▷ (P ∧ Q))

by Lemma 4 ⇒ (P ∨ Q) ∧ ((P ∨ Q) −▷ (P ∧ Q))

by Lemma 3(1) ⇒ Q

by Lemma 3(1).

⟨3⟩2. ⊧ (P −▷ Q) ∧ (P ⊥ Q) ⇒ ((Q −▷ P) −▷ Q)

Proof: ⟨3⟩1 and Lemma 1(2).

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

⟨3⟩3. Q.E.D.

Proof: ⟨3⟩2, case assumption ⟨1⟩, and Lemma 6. ⟨1⟩2. Q.E.D.

Proof: P −▷^{+} Q = (P ⇒ Q) ∧ (C(P) −▷^{+} C(Q)) by Lemma 2(2) = (P ⇒ Q) ∧ (C(P) −▷ C(Q)) ∧ (C(P) ⊥ C(Q)) by ⟨1⟩1 = (P ⇒ Q) ∧ (C(P) −▷ C(Q)) ∧ (P ⊥ Q) by Lemma 15(1) = (P −▷ Q) ∧ (P ⊥ Q) by Lemma 2(1).

Proposition 4. Assume: 1. P, Q, and R are safety properties.

2. ⊧ P ∧ Q ⇒ R

3. ⊧ Q ⇒ P ⊥R

4. the tuple x contains all the free variables of R.

Prove: ⊧ P_{+x} ∧ Q ⇒ R

⟨1⟩1. ⊧ Q ⇒ (P −▷ R)

Proof: Assumptions ⟨0⟩:1 and ⟨0⟩:2, and Lemma 1(2).

⟨1⟩2. ⊧ Q ⇒ (P −▷^{+} R)

Proof: ⟨1⟩1, assumption ⟨0⟩:3, and Lemma 16. ⟨1⟩3. ⊧ Q ⇒ (P_{+x} −▷ R)

Proof: ⟨1⟩2, assumptions ⟨0⟩:1 and ⟨0⟩:4, and Lemma 11. ⟨1⟩4. Q.E.D.

Proof: ⟨1⟩3 and Lemma 1(2).

Lemma 17.

Let: E =^{Δ} Init_{E} ∧ □ [N_{E}]_{⟨x, e⟩}

M =^{Δ} Init_{M} ∧ □ [N_{M}]_{⟨y, m⟩}

Prove: ⊧ ((∃ ∃ ∃ ∃ ∃ ∃ x : Init_{E}) ∨ (∃ ∃ ∃ ∃ ∃ ∃ y : Init_{M})) ∧ Disjoint(e, m) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : E) ⊥ C(∃ ∃ ∃ ∃ ∃ ∃ y : M)

Proof: By definition of ⊥, it suffices to prove the following, for all n ≥ 0: Assume: 1. σ ⊧ ((∃ x : Init_{E}) ∨ (∃ y : Init_{M}))

2. σ ⊧ Disjoint(e, m)

3. σ|_{n} ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x : E) ∧ C(∃ ∃ ∃ ∃ ∃ ∃ y : M)

Prove: σ|_{n+1} ⊧ C(∃ ∃ ∃ ∃ ∃ ∃ x : E) ∨ C(∃ ∃ ∃ ∃ ∃ ∃ y : M) ⟨1⟩1. Case: n = 0

⟨2⟩1. Case: σ ⊧ (∃ x : Init_{E})

⟨3⟩1. Choose a state s such that s =_{x} σ_{1} and s ⊧ Init_{E}.

Proof: Case assumption ⟨2⟩. ⟨3⟩2. ⟨s, s, s, … ⟩ ⊧ E

Proof: ⟨3⟩1 and the definition of E. ⟨3⟩3. ⟨σ_{1}, s, s, s, … ⟩ ⊧ ∃ ∃ ∃ ∃ ∃ ∃ x : E

Proof: ⟨3⟩1, ⟨3⟩2, and the definition of ∃ ∃ ∃ ∃ ∃ ∃. ⟨3⟩4. σ|_{1} ⊧ ∃ ∃ ∃ ∃ ∃ ∃x : E Proof: ⟨3⟩3.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

⟨3⟩5. Q.E.D. ⟨2⟩2. Case: σ ⊧ (∃ x : Init_{M})

Proof: The proof is the same as the proof of ⟨2⟩1, with M substituted for E and y substituted for x.

⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and assumption ⟨0⟩:1. ⟨1⟩2. Case: n > 0

⟨2⟩1. ([[e]](σ_{n}) = [[e]](σ_{n+1})) ∨ ([[m]](σ_{n}) = [[m]](σ_{n+1}))

Proof: Assumption ⟨0⟩:2. ⟨2⟩2. Case: [[e]](σ_{n}) = [[e]](σ_{n+1})

⟨3⟩1. Choose ρ such that:

1. ρ ≃_{x} σ|_{n}

2. ρ ⊧ E Proof: Assumption ⟨0⟩:3, since η ⊧ C(P) iff η ⊧ P, for any property P and finite behavior η.

Let: t be the state such that t =_{x} σ_{n+1} and [[x]](t) = [[x]](last(ρ)). ⟨3⟩2. ρ ∘ ⟨t⟩ ⊧ E

Proof: ⟨3⟩1.2, case assumption ⟨2⟩, and the definitions of t and E. ⟨3⟩3. σ|_{n+1} ≃_{x} ρ ∘ ⟨t⟩

Proof: ⟨3⟩1.1 and the definition of t. ⟨3⟩4. σ|_{n+1} ⊧ ∃ ∃ ∃ ∃ ∃ ∃x : E

Proof: ⟨3⟩2 and ⟨3⟩3. ⟨3⟩5. Q.E.D.

Proof: ⟨3⟩4. ⟨2⟩3. Case: [[m]](σ_{n}) = [[m]](σ_{n+1})

Proof: The proof is the same as the proof of ⟨2⟩2, with m, M, and y substituted for e, E, and x, respectively.

⟨2⟩4. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and ⟨2⟩3. ⟨1⟩3. Q.E.D.

Proposition 5. Assume: 1. ⊧ C(E) = Init_{E} ∧ □ [N_{E}]_{⟨x, e⟩}

2. ⊧ C(M) = Init_{M} ∧ □ [N_{M}]_{⟨y, m⟩}

Prove: ⊧ ((∃ ∃ ∃ ∃ ∃ ∃ x : Init_{E}) ∨ (∃ ∃ ∃ ∃ ∃ ∃ y : Init_{M})) ∧ Disjoint(e, m) ⇒ C(∃ ∃ ∃ ∃ ∃ ∃ x : E) ⊥ C(∃ ∃ ∃ ∃ ∃ ∃ y : M)

Proof: Follows from Lemma 17, with C(E) substituted for E and C(M) substituted for M, and Lemma 8.

B5 Composition as Conjunction

Proposition 6. Let m_{1}, …, m_{n}, x_{1}, …, x_{n} be tuples of variables, and let

m =^{Δ} ⟨m_{1}, …, m_{n}⟩ x =^{Δ} ⟨x_{1}, …, x_{n}⟩

x̂_{i} =^{Δ} ⟨x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}⟩

M_{i} =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x_{i} : Init_{i} ∧ □[N_{i}]_{⟨m_{i}, x_{i}⟩} ∧ L_{i}

Assume: For all i, j with i ≠ j:

1. no variable of x_{j} occurs free in x_{i} or M_{i}.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

2. m includes all free variables of M_{i}.

3. ⊧ N_{i} ⇒ (m′_{j} = m_{j})

Prove: ⊧ ⋀_{i=1}^{n} M_{i} = ∃ ∃ ∃ ∃ ∃ ∃ x : ⋀_{i=1}^{n} Init_{i} ∧ □[ ⋁_{i=1}^{n} N_{i} ∧ (x′_{i} = x̂_{i})]_{⟨m, x⟩} ∧ ⋀_{i=1}^{n} L_{i}

Proof: The hypotheses remain true and the conclusion is unchanged if we remove from m_{j} any variable that appears in x_{j}. (Assumption 2 remains true because, by assumption 1, the variable removed cannot occur free in M_{i}.) Therefore, without loss of generality, we can strengthen assumption 1 to: Assume: 1(a). The variables in x_{j} do not occur free in M_{i}, and are distinct from

the variables in x_{i} and m_{j}.

The proof is by induction on n, with the cases for n = 1 and n = 2 proved separately. ⟨1⟩1. Case: n = 1

Proof: This case follows immediately from the definition of M_{i}. ⟨1⟩2. Case: n = 2

Let: N_{H} =^{Δ} [\begin{matrix}∨ N_{1} ∧ (x′_{2} = x_{2}) \\ ∨ N_{2} ∧ (x′_{1} = x_{1}) \end{matrix}]_{⟨m, x⟩}

N_{U} =^{Δ} [\begin{matrix}∨ N_{1} ∧ (x′_{2} = x_{2}) \\ ∨ N_{2} ∧ (x′_{1} = x_{1}) \\ ∨ N_{1} ∧ N_{2} \end{matrix}]_{⟨m, x⟩}
H =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x_{1}, x_{2} : Init_{1} ∧ Init_{2} ∧ □ N_{H} ∧ L_{1} ∧ L_{2}
U =^{Δ} Init_{1} ∧ Init_{2} ∧ □ N_{U} ∧ L_{1} ∧ L_{2}

Prove: ⊧ M_{1} ∧ M_{2} = H

⟨2⟩1. ⊧ M_{1} ∧ M_{2} = ∃ ∃ ∃ ∃ ∃ ∃ x_{1}, x_{2} : U

Let: N_{V} =^{Δ} [\begin{matrix}∧ N_{1} ∨ (⟨m_{1}, x_{1}⟩′ = ⟨m_{1}, x_{1}⟩) \\ ∧ N_{2} ∨ (⟨m_{2}, x_{2}⟩′ = ⟨m_{2}, x_{2}⟩) \end{matrix}]_{⟨m, x⟩}

V =^{Δ} Init_{1} ∧ Init_{2} ∧ □ N_{V} ∧ L_{1} ∧ L_{2}

⟨3⟩1. ⊧ N_{V} = N_{U} Proof: Assumption ⟨0⟩:3, which implies

\begin{matrix}⊧ N_{2} ∧ (⟨m_{1}, x_{1}⟩′ = ⟨m_{1}, x_{1}⟩) = N_{2} ∧ (x′_{1} = x_{1}) \\ ⊧ N_{1} ∧ (⟨m_{2}, x_{2}⟩′ = ⟨m_{2}, x_{2}⟩) = N_{1} ∧ (x′_{2} = x_{2}) \end{matrix}

⟨3⟩2. ⊧ V = U

Proof: ⟨3⟩1 and the definitions of V and U. ⟨3⟩3. ⊧ [N_{1}]_{⟨m_{1}, x_{1}⟩} ∧ [N_{2}]_{⟨m_{2}, x_{2}⟩} = N_{V} Proof: The definition of m and x.

⟨3⟩4. ⊧ M_{1} ∧ M_{2} = ∃ ∃ ∃ ∃ ∃ ∃ x_{1}, x_{2} : V

Proof: ⟨3⟩3 and assumption ⟨0⟩:1(a), since □ distributes over ∧. ⟨3⟩5. Q.E.D.

Proof: ⟨3⟩2 and ⟨3⟩4. ⟨2⟩2. ⊧ H ⇒ M_{1} ∧ M_{2}

Proof: ⟨2⟩1, since ⊧ N_{H} ⇒ N_{U}. ⟨2⟩3. ⊧ M_{1} ∧ M_{2} ⇒ H

Assume: σ ⊧ M_{1} ∧ M_{2}

Prove: σ ⊧ H

⟨3⟩1. Choose τ such that τ ≃_{⟨x_{1}, x_{2}⟩} σ and τ ⊧ U. Proof: τ exists by assumption ⟨2⟩, ⟨2⟩1, and the definition of ∃ ∃ ∃ ∃ ∃ ∃.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Let: η be the behavior such that, for all n > 0:

η_{2n−1} =^{Δ} τ_{n}

η_{2n} =^{Δ} if [[x_{1}]](τ_{n}) = [[x_{1}]](τ_{n+1}) or [[x_{2}]](τ_{n}) = [[x_{2}]](τ_{n+1})

then τ_{n}
else the state such that [[x_{1}]](η_{2n}) = [[x_{1}]](τ_{n+1})
and η_{2n} =_{x_{1}} τ_{n}.

(η is the same as τ except that each step is split in two. A step that changes both x_{1} and x_{2} is split into a step that changes only x_{1} followed by one that leaves x_{1} unchanged. For a step that leaves x_{1} or x_{2} unchanged, a stuttering step is added.)

⟨3⟩2. For all n > 0, if [[x_{1}]](τ_{n}) ≠ [[x_{1}]](τ_{n+1}) and [[x_{2}]](τ_{n}) ≠ [[x_{2}]](τ_{n+1}) then

⟨τ_{n}, τ_{n+1}⟩ is an N_{1} ∧ N_{2} ∧ (m′ = m) step. Assume: [[x_{1}]](τ_{n}) ≠ [[x_{1}]](τ_{n+1}) and [[x_{2}]](τ_{n}) ≠ [[x_{2}]](τ_{n+1}). Prove: ⟨τ_{n}, τ_{n+1}⟩ is an N_{1} ∧ N_{2} ∧ (m′ = m) step. ⟨4⟩1. ⟨τ_{n}, τ_{n+1}⟩ is an N_{U} step.

Proof: ⟨3⟩1 (which asserts τ ⊧ U) and the definition of U. ⟨4⟩2. ⟨τ_{n}, τ_{n+1}⟩ is an N_{1} ∧ N_{2} step.

Proof: Assumption ⟨3⟩, ⟨4⟩1, and the definition of N_{U}. ⟨4⟩3. Q.E.D.

Proof: ⟨4⟩2 and assumption ⟨0⟩:3. ⟨3⟩3. For all n > 0, ⟨η_{n}, η_{n+1}⟩ is an N_{H} step.

Let: k =^{Δ} (n + 1) div 2

⟨4⟩1. Case: [[x_{1}]](τ_{k}) = [[x_{1}]](τ_{k+1}) or [[x_{2}]](τ_{k}) = [[x_{2}]](τ_{k+1})

(In this case, ⟨η_{n}, η_{n+1}⟩ is a step of τ or a stutter.)

⟨5⟩1. ⟨η_{n}, η_{n+1}⟩ = ⟨τ_{k}, τ_{k+1}⟩ or η_{n} = η_{n+1}.

Proof: The definition of η and case assumption ⟨4⟩. ⟨5⟩2. [[x_{1}]](η_{n}) = [[x_{1}]](η_{n+1}) or [[x_{2}]](η_{n}) = [[x_{2}]](η_{n+1}).

Proof: ⟨5⟩1 and case assumption ⟨4⟩. ⟨5⟩3. ⟨η_{n}, η_{n+1}⟩ is an N_{U} step.

Proof: ⟨5⟩1, ⟨3⟩1 (which asserts τ ⊧ U), and the definition of U. ⟨5⟩4. Q.E.D.

Proof: ⟨5⟩2 and ⟨5⟩3, since ⊧ N_{U} ∧ ((x′_{1} = x_{1}) ∨ (x′_{2} = x_{2})) ⇒ N_{H}. ⟨4⟩2. Case: n = 2k − 1, [[x_{1}]](τ_{k}) ≠ [[x_{1}]](τ_{k+1}), and

[[x_{2}]](τ_{k}) ≠ [[x_{2}]](τ_{k+1}).

(In this case, ⟨η_{n}, η_{n+1}⟩ is a step that changes only x_{1}.)

⟨5⟩1. η_{n} = τ_{k}, [[x_{1}]](η_{n+1}) = [[x_{1}]](τ_{k+1}), and η_{n+1} =_{x_{1}} τ_{k}

Proof: The definition of η and case assumption ⟨4⟩. ⟨5⟩2. ⟨τ_{k}, τ_{k+1}⟩ is an N_{1} ∧ N_{2} ∧ (m′ = m) step.

Proof: ⟨3⟩2 and case assumption ⟨4⟩. ⟨5⟩3. [[m]](η_{n}) = [[m]](τ_{k}) and [[m]](η_{n+1}) = [[m]](τ_{k+1})

Proof: ⟨5⟩1 implies [[m]](η_{n}) = [[m]](τ_{k}), ⟨5⟩1 and assumption ⟨0⟩:1(a) (which implies that no variable in x_{1} occurs in m_{1} or m_{2}) imply [[m]](η_{n+1}) = [[m]](τ_{k}), and ⟨5⟩2 implies [[m]](τ_{k}) = [[m]](τ_{k+1}).

⟨5⟩4. [[x_{1}]](η_{n}) = [[x_{1}]](τ_{k}) and [[x_{1}]](η_{n+1}) = [[x_{1}]](τ_{k+1})

Proof: ⟨5⟩1. ⟨5⟩5. ⟨m, x_{1}⟩ contains all variables free in N_{1}.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Proof: Assumption ⟨0⟩:2 and the definition of M_{1}. ⟨5⟩6. ⟨η_{n}, η_{n+1}⟩ is an N_{1} step

Proof: ⟨5⟩2, ⟨5⟩3, ⟨5⟩4, and ⟨5⟩5. ⟨5⟩7. ⟨η_{n}, η_{n+1}⟩ is an x′_{2} = x_{2} step.

Proof: ⟨5⟩1 and ⟨0⟩:1(a), which implies that x_{1} and x_{2} have no variable in common.

⟨5⟩8. Q.E.D.

Proof: ⟨5⟩6 and ⟨5⟩7, since ⊧ N_{1} ∧ (x′_{2} = x_{2}) ⇒ N_{H}. ⟨4⟩3. Case: n = 2k, [[x_{1}]](τ_{k}) ≠ [[x_{1}]](τ_{k+1}), and

[[x_{2}]](τ_{k}) ≠ [[x_{2}]](τ_{k+1}).

(In this case, ⟨η_{n}, η_{n+1}⟩ is a step that leaves x_{1} unchanged.)

⟨5⟩1. η_{n+1} = τ_{k+1}, [[x_{1}]](η_{n}) = [[x_{1}]](τ_{k+1}), and η_{n} =_{x_{1}} τ_{k}.

Proof: The definition of η and case assumption ⟨4⟩. ⟨5⟩2. ⟨τ_{k}, τ_{k+1}⟩ is an N_{2} step.

Proof: ⟨3⟩2 and case assumption ⟨4⟩. ⟨5⟩3. [[⟨m, x_{2}⟩]](η_{n}) = [[⟨m, x_{2}⟩]](τ_{k}) and

[[⟨m, x_{2}⟩]](η_{n+1}) = [[⟨m, x_{2}⟩]](τ_{k+1}). Proof: ⟨5⟩1 and assumption ⟨0⟩:1(a), which implies that x_{1} has no variable in common with x_{2} or m.

⟨5⟩4. ⟨m, x_{2}⟩ contains all variables free in N_{2}.

Proof: Assumption ⟨0⟩:2 and the definition of M_{2}. ⟨5⟩5. ⟨η_{n}, η_{n+1}⟩ is an N_{2} step

Proof:⟨5⟩2, ⟨5⟩3, and ⟨5⟩4. ⟨5⟩6. ⟨η_{n}, η_{n+1}⟩ is an x′_{1} = x_{1} step.

Proof: ⟨5⟩1. ⟨5⟩7. Q.E.D.

Proof:⟨5⟩5 and ⟨5⟩6, since ⊧ N_{2} ∧ (x′_{1} = x_{1}) ⇒ N_{H}. ⟨4⟩4. Q.E.D.

Proof: ⟨4⟩1, ⟨4⟩2, and ⟨4⟩3. ⟨3⟩4. η ⊧ Init_{1} ∧ Init_{2}

⟨4⟩1. τ ⊧ Init_{1} ∧ Init_{2}

Proof: The definition of U and ⟨3⟩1 (which asserts τ ⊧ U). ⟨4⟩2. η_{1} = τ_{1}

Proof: The definition of η. ⟨4⟩3. Q.E.D.

Proof: ⟨4⟩1 and ⟨4⟩2, since [[P]](ρ) = [[P]](ρ_{1}) for any predicate P and behavior ρ.

⟨3⟩5. η ⊧ L_{1} ∧ L_{2}

⟨4⟩1. η ⊧ L_{1}

⟨5⟩1. τ ⊧ L_{1}

Proof: ⟨3⟩1 and the definition of U. ⟨5⟩2. For all n > 0:

1. η_{2n−1} = τ_{n}

2. [[⟨m, x_{1}⟩]](η_{2n}) = [[⟨m, x_{1}⟩]](τ_{n}) or
[[⟨m, x_{1}⟩]](η_{2n}) = [[⟨m, x_{1}⟩]](τ_{n+1})

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Proof: Part 1 follows from the definition of η. Part 2 follows from the definition of η and ⟨3⟩2, which implies [[m]](τ_{n}) = [[m]](τ_{n+1}) when the if condition in the definition is false.

⟨5⟩3. Choose η̂ such that η̂_{2n−1} = τ_{n} and

η̂_{2n} = if [[⟨m, x_{1}⟩]](η_{2n}) = [[⟨m, x_{1}⟩]](τ_{n}) \begin{matrix}then & τ_{n} \\ else & τ_{n+1} \end{matrix}

for all n. Then η̂ is stuttering equivalent to τ, and, for all n, [[⟨m, x_{1}⟩]](η̂_{n}) = [[⟨m, x_{1}⟩]](η_{n}).

Proof: ⟨5⟩2. ⟨5⟩4. η̂ ⊧ L_{1}

Proof: ⟨5⟩1 and ⟨5⟩3, since TLA formulas are invariant under stuttering.

⟨5⟩5. [[L_{1}]](η̂) = [[L_{1}]](η)

Proof: ⟨5⟩3, since ⟨m, x_{1}⟩ contains all variables occurring free in L_{1}, by assumption ⟨0⟩:2 and the definition of M_{1}.

⟨5⟩6. Q.E.D.

Proof: ⟨5⟩4 and ⟨5⟩5. ⟨4⟩2. η ⊧ L_{2}

⟨5⟩1. τ ⊧ L_{2}

Proof: ⟨3⟩1 and the definition of U. ⟨5⟩2. η ≃_{x_{1}} τ

Proof: The definition of η. ⟨5⟩3. Q.E.D.

Proof: ⟨5⟩1, ⟨5⟩2, and assumption ⟨0⟩:1(a), which implies that x_{1} does not occur free in L_{2}.

⟨4⟩3. Q.E.D. ⟨3⟩6. η ⊧ H

Proof: ⟨3⟩3, ⟨3⟩4, and ⟨3⟩5, and the definition of H. ⟨3⟩7. η ≃_{⟨x_{1}, x_{2}⟩} σ

Proof: ⟨3⟩1, which asserts τ ≃_{⟨x_{1}, x_{2}⟩} σ, and the definition of η, which implies η ≃_{x_{1}} τ.

⟨3⟩8. Q.E.D.

Proof: ⟨3⟩6, ⟨3⟩7, and the definition of H. ⟨2⟩4. Q.E.D.

⟨1⟩3. Case: n > 2, and the theorem holds with p substituted for n, for all p < n.

Let: \begin{matrix}mm =^{Δ} & ⟨m_{1}, …, m_{n−1}⟩ \\ xx =^{Δ} & ⟨x_{1}, …, x_{n−1}⟩ \\ x̂x_{i} =^{Δ} & ⟨x_{1}, … x_{i−1}, , x_{i+1}, …, x_{n−1}⟩ \end{matrix}

Proof: ⋀_{i≤n} M_{i} = (⋀_{i≤n−1} M_{i}) ∧ M_{n} by propositional logic

= \begin{matrix}∧ ∃ ∃ ∃ ∃ ∃ ∃xx : \begin{matrix}∧ ⋀_{i≤n−1} Init_{i} \\ ∧ □ [ ⋁_{i≤n−1} N_{i} ∧ (x̂x′_{i} = x̂x_{i})]_{⟨mm, xx⟩} \\ ∧ ⋀_{n−1} L_{i} \end{matrix} \\ ∧ M_{n} \end{matrix} by case assumption ⟨1⟩, with n − 1 substituted for p

= ∃ ∃ ∃ ∃ ∃ ∃xx, x_{n} : \begin{matrix}∧ ⋀ Init_{i} \\ ∧ □ [\begin{matrix}∨ \begin{matrix}∧ ⋁_{i≤n−1} N_{i} ∧ (x̂x′_{i} = x̂x_{i}) \\ ∧ (x′_{n} = x_{n}) \end{matrix} \\ ∨ N_{n} ∧ (x′_{n} = x̂_{n}) \end{matrix}]_{⟨mm, xx, m_{n}, x_{n}⟩} \\ ∧ ⋀ L_{i} \end{matrix} by case assumption ⟨1⟩, with 2 substituted for p

= ∃ ∃ ∃ ∃ ∃ ∃ x : ⋀_{i=1}^{n} Init_{i} ∧ □[ ⋁_{i=1}^{n} N_{i} ∧ (x′_{i} = x̂_{i})]_{⟨m, x⟩} ∧ ⋀_{i=1}^{n} L_{i}

⟨1⟩4. Q.E.D.

Proof: ⟨1⟩1, ⟨1⟩2, ⟨1⟩3, and mathematical induction.

B6 Decomposition and Composition

Theorem 1 is an immediate consequence of Theorem 2. The proof of Theorem 2 assumes Theorem 3, but Theorem 2 is not used in the proof of Theorem 3 or of any lemma, so there is no circularity. Theorem 2. Assume: For i = 1, …, n:

1. ⊧ C(E) ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ E_{i}

2. a. ⊧ C(E_{i})_{+v} ∧ C(M_{i}^{l}) ⇒ C(M_{i})

b. ⊧ E_{i} ∧ M_{i}^{l} ⇒ M_{i}

3. v is a tuple of variables including all the free variables of M_{i}.

Prove: a. ⊧ C(E)_{+v} ∧ ⋀_{j=1}^{n}C(M_{j}^{l}) ⇒ ⋀_{j=1}^{n}C(M_{j})

b. ⊧ E ∧ ⋀_{j=1}^{n}M_{j}^{l} ⇒ ⋀_{j=1}^{n}M_{j}

⟨1⟩1. For any E, E_{i}, M_{i}^{l}, and M_{i} satisfying assumptions ⟨0⟩:1–3, and all i =

1, …, n: ⊧ ( ⋀_{j=1}^{n}M_{j}^{l}) ⇒ (E −▷^{+} M_{i})

⟨2⟩1. For j = 1, …, n: ⊧ M_{j}^{l} ⇒ (E_{i} −▷^{+} M_{j})

⟨3⟩1. For i = 1, …, n: ⊧ C(M_{i}^{l}) ⇒ (C(E_{i}) −▷^{+} C(M_{i}))

Proof: Assumption ⟨0⟩:2(a), Lemma 1(2), assumption ⟨0⟩:3, and Lemma 11. ⟨3⟩2. For i = 1, …, n: ⊧ M_{i}^{l} ⇒ (E_{i} ⇒ M_{i})

Proof: Assumption ⟨0⟩:2(b). ⟨3⟩3. Q.E.D.

Proof: ⟨3⟩1, ⟨3⟩2, and Lemma 2(2).

⟨2⟩2. For i = 1, …, n: ⊧ ( ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ (E −▷^{+} M_{i})

Proof: The Composition Theorem (Theorem 3), with M_{i} substituted for M, where hypothesis 1 of the Composition Theorem follows from assumption ⟨0⟩:1, and hypotheses 2(a) and 2(b) are vacuous when M_{i} is substituted for M.

⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩2, and propositional reasoning. ⟨1⟩2. Conclusion (a) holds.

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

⟨2⟩1. For i = 1, …, n: ⊧ ( ⋀_{j=1}^{n}C(M_{j}^{l})) ⇒ (C(E) −▷^{+} C(M_{i}))

Proof: ⟨1⟩1, substituting C(E) for E, C(M_{j}^{l}) for M_{j}^{l}, and C(M_{i}) for M_{i}. Since C is idempotent, this instantiation changes only assumption 2(b), which becomes ⊧ C(E_{i}) ∧ C(M_{i}^{l}) ⇒ C(M_{i}). This assumption follows from 2(a), since ⊧ P ⇒ P_{+v}, for any P.

⟨2⟩2. For i = 1, …, n: ⊧ ( ⋀_{j=1}^{n}C(M_{j}^{l})) ⇒ (C(E)_{+v} −▷ C(M_{i}))

Proof: ⟨2⟩1, assumption ⟨0⟩:3, and Lemma 11. ⟨2⟩3. Q.E.D.

Proof: ⟨2⟩2 and Lemma 1(2) (conjoining over all i). ⟨1⟩3. Conclusion (b) holds.

⟨2⟩1. ⊧ E ∧ ( ⋀_{j=1}^{n}M_{j}^{l}) ⇒ M_{i}

Proof: ⟨1⟩1 and Lemma 2(2). ⟨2⟩2. Q.E.D.

Proof: ⟨2⟩1 (conjoining over all i). ⟨1⟩4. Q.E.D.

Lemma 18. Assume: For i = 1, …, n:

0. M_{i} is a safety property.

1. E and E_{i} are safety properties.

2. ⊧ (E ∧ ⋀_{j=1}^{n}M_{j}) ⇒ E_{i}

Prove: ⊧ ( ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ (E −▷^{+} ( ⋀_{j=1}^{n}M_{j}))

Proof: ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ (⋀_{j=1}^{n} E_{j}) −▷^{+} (⋀_{j=1}^{n} M_{j}) Lemma 5 and assumptions ⟨0⟩:0 and ⟨0⟩:1 ⇒ E −▷^{+} (⋀_{j=1}^{n} M_{j}) assumption ⟨0⟩:2 and Lemma 7, substituting E for R, ⋀_{j=1}^{n} E_{j} for P, and ⋀_{j=1}^{n} M_{j} for Q.

Theorem 3. Assume: For i = 1, …, n:

1. ⊧ C(E) ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ E_{i}

2. a. ⊧ C(E)_{+v} ∧ ⋀_{j=1}^{n}C(M_{j}) ⇒ C(M)

b. ⊧ E ∧ ⋀_{j=1}^{n}M_{j} ⇒ M

Prove: ⊧ ⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j}) ⇒ (E −▷^{+} M)

⟨1⟩1. ⊧ (⋀_{j=1}^{n}(C(E_{j}) −▷^{+} C(M_{j}))) ⇒ (C(E) −▷^{+} (⋀_{j=1}^{n} C(M_{j})))

Proof: Assumption ⟨0⟩:1 and Lemma 18, since ⊧ E_{i} ⇒ C(E_{i}) (because C is superdiagonal).

⟨1⟩2. ⊧ (C(E) −▷^{+} (⋀_{j=1}^{n} C(M_{j}))) ⇒ (C(E) −▷^{+} C(M))

Proof: Assumption ⟨0⟩:2(a) and Lemma 12.

⟨1⟩3. ⊧ (⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ (E ⇒ M)

⟨2⟩1. ⊧ C(E) ∧ (⋀_{j=1}^{n}(C(E_{j}) −▷^{+} C(M_{j}))) ⇒ ⋀_{j=1}^{n} C(M_{j})

Proof: ⟨1⟩1 and Lemma 3(2).

⟨2⟩2. ⊧ E ∧ (⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ ⋀_{j=1}^{n} C(M_{j})

Proof: ⟨2⟩1, since ⊧ E ⇒ C(E) (because C is superdiagonal) and ⊧ (E_{j} −▷^{+}

M_{j}) ⇒ (C(E_{j}) −▷^{+} C(M_{j})) by Lemma 2.

⟨2⟩3. ⊧ E ∧ (⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ ⋀_{j=1}^{n} E_{j}

Proof: ⟨2⟩2 and assumption ⟨0⟩:1, since C is superdiagonal.

⟨2⟩4. ⊧ E ∧ (⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ ⋀_{j=1}^{n} M_{j}

Proof: ⟨2⟩3 and Lemma 3(2).

⟨2⟩5. ⊧ E ∧ (⋀_{j=1}^{n}(E_{j} −▷^{+} M_{j})) ⇒ M

Proof: ⟨2⟩4 and assumption ⟨0⟩:2(b). ⟨2⟩6. Q.E.D.

Proof: ⟨2⟩5. ⟨1⟩4. Q.E.D.

Proof: ⟨1⟩1 and ⟨1⟩2, which imply

⊧ ⋀_{j=1}^{n}(C(E_{j}) −▷^{+} C(M_{j})) ⇒ (C(E) −▷^{+} C(M))

⟨1⟩3, and Lemma 2(2).

A–20 · Martín Abadi and Leslie Lamport

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Index □, 7 ◇, 7 ∃ ∃ ∃ ∃ ∃ ∃, 8 +, 13–14 ∘, 5 ′ (prime), 7 ⊥, 14–15 =_{...}, A–1 ≃_{...}, A–2 ⇒, precedence of, 8 −▷, 14

−▷^{+}, 2, 14

⊧, 7, A–1 … |_{...}, A–1 | … |, 5 ⟨…⟩

enclosing atomic operation, 3 sequence notation, 5

[…]_{...}, 7 ⟨…⟩_{...}, 7 [[…]], A–1 ∧, list of, 8 ∨, list of, 8

action, 7

next-state, 11 angle brackets

enclosing atomic operation, 3 sequence notation, 5

antimonotonic, A–2 assumption, environment, 2, 5, 22 assumption/guarantee specification, 5,

22

behavior, 7

intuitive interpretation of, 8 Berthet, Christian, 26 Boolean operator, 7 brackets, angle

enclosing atomic operation, 3 sequence notation, 5

C, 12, A–1 canonical form, 8 Cerans, Karlis, 26 Cerny, Eduard, 26 Chandy, K. Mani, 26 channel, 4 circuit description as low-level speci-

fication, 1 circular reasoning, 19 closure, 12 closure, machine, 13 Collette, Pierre, 26 complete system, 2

decomposition of, 2–4, 15–22 component guarantee, 2 composition, 2, 4–7, 22–24 Composition Theorem, 23 conditional implementation, 12 conjunction of components, 17–19 conjunction, list notation for, 8 COSPAN, 26 CSP, 26

decomposition, 2–4, 15–22 Decomposition Theorem, 19 Decomposition Theorem, General, 21 Disjoint, 8 disjunction, list notation for, 8

enabled, 7 Enabled …, 7 environment assumption, 2, 5, 22

fairness strong, 7 weak, 7

flexible variable, 7 form, canonical, 8 formula, TLA, 7 function, state, 7

GCD program, 3–4, 8, 16, 18, 20 General Decomposition Theorem, 21 guarantee, 2, 5, 22

Head, 5 hiding, 2, 13 Hoare triple, 26

iff, 3 A–21 implementation, 1

conditional, 12 indentation, eliminating parentheses

with, 8 inductively defined system, 21 Init, 8 input variable, 15, 17 interface refinement, 12 interleaving representation, 8–9 internal variable, 8 invariant under stuttering, A–1

Joseph, Mathai, 26

last, A–1

machine closure, 13 mapping, refinement, 11 Merz, Stephan, 26 Misra, Jayadev, 26 monotonic, A–2 multiplier

recursive definition, 21

verification, 26

next-state action, 11 noninterleaving representation, 8–9 number, statement (in proof), A–2

open system, 4 operator

Boolean, 7 precedence of, 8

output variable, 15, 17

Pandya, Paritosh K., 26 Plotkin,Gordon, 26 Pnueli, Amir, 1, 26 predicate, state, 7 program as low-level specification, 1 proof style, explanation, A–2

queue, 4–6, 9–10, 16–18, 24

implemented by two queues, 11– 12

real-time specification, 12 refinement mapping, 11 refinement, interface, 12

safety property, 6, 12 semantics of TLA, 7–8 sequences, notation for, 5 SF, 7 specification

assumption/guarantee, 5 higher-level, 1 low-level, 1 real-time, 12 Stark, Eugene W., 26 state, 7 state function, 7 state predicate, 7 statement number (in proof), A–2 step, 7

stuttering, 1 strong fairness, 7 stutter-free version of a behavior, A–1 stuttering equivalent, A–1 stuttering step, 1 stuttering, invariant under, A–1 subaction, 13 superdiagonal, A–2 syntax of TLA, 7–8 system

defined inductively, 21

open, 4 system guarantee, 5, 22 system, complete, 2

Tail, 5

Temporal Logic of Actions, 1

TLA, 1, 7–8

Unity, 26 universe, 8

valid, 7 variable

flexible, 7 hiding of, 2, 13 history, 26 input, 15, 17 internal, 8 intuitive interpretation of, 8 output, 15, 17

ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.

Conjoining Specifications · A–23

primed, 7 weak fairness, 7 WF, 7 Yu, Yuan, 26