Conjoining specifications.
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.
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 \Pi i by a formula S i so that the parallel composition usually
denoted cobegin \Pi coend is represented by the formula S 1 -Sn .
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
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.
c
ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995, Pages 507-533.
508 \Delta Mart'in Abadi and Leslie Lamport
the logic. Still later, it was noticed that the formula 999 999x : 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
\Gamma. M . To show that a composition of reusable components satisfies a
specification S, we must prove a formula of the form
\Gamma.
\Gamma.
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 \Delta 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
loop-endloop keywords enclose an infinite loop; cobegin-coend key-words
enclose parallel statements, separated by k; and semicolon has its usual
meaning. When writing processes, we will also mark variables as output, input, or
a process cannot change its input variables or access the internal variables
of another process.
Program GCD
var a initially 233344, b initially
cobegin loop h if a ? b then a := a \Gamma b i endloop
loop h if b ? a then b := b \Gamma a i 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 prop-
erty, 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
\Pi a and \Pi b . We can write \Pi a and \Pi b as
Process \Pi a Process \Pi b
output var a initially 233344 ; output var b initially
input var b ; input var a ;
loop h if a ? b then a := a
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 \Pi a to
Process \Pi l
a
output var a initially 233344 ;
internal var ai ;
input var b ;
loop h ai := b
and refining \Pi b to the analogous process \Pi l
b .
The composition of processes \Pi l
a and \Pi l
correctly implements program GCD.
This is expressed in TLA by the assertion that M l
implies M a - M b , where
l
a and M l
b are the formulas representing \Pi l
a and \Pi l
b .
We would like to decompose the proof of M l
into proofs of
l
a ) M a and M l
. These proofs would show that \Pi l
a implements \Pi a and
that \Pi l
b implements \Pi b .
initial
statesentackedsentackedsent
Fig. 1. The two-phase handshake protocol for a channel c.
Unfortunately, \Pi l
a does not implement \Pi a because, in the absence of assumptions
about when its input b can change, \Pi l a can behave in ways that process \Pi a cannot.
Process \Pi a can decrement a only by the current value of b, but \Pi l a can decrement
a by a previous value of b if b changes between the assignment to ai and the
assignment to a. Similarly, \Pi l
b does not implement \Pi b .
Process \Pi l
a does correctly implement process \Pi a in a context in which b does
not change when a ? b. This is expressed in TLA by the formula E a - M l
where E a asserts that b does not change when a ? b. Similarly,
holds, for the analogous E b . The Decomposition Theorem of Section 4.3 allows us
to deduce M l
b )M a - M b from approximately the following hypotheses:
a )M a
(1)
The third hypothesis holds because the composition of processes \Pi a and \Pi 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 \Pi l
b needed to guarantee that \Pi l
a
implements \Pi a . In a more complicated example, E a will be significantly simpler
than M l
b , the full specification of \Pi l
b . Verifying these hypotheses will therefore be
easier than proving M l
a -M l
b )M a -M b directly, since this proof requires reasoning
about the specification M l
b of the complete low-level program.
One cannot really deduce M l
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 l
arbitrary M l
a and M l
b . 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 two-phase
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 hc:sig; c:vali. Figure 1 shows the sequence of states assumed in
sending the sequence of values 37, 4, . The channel is ready to send when
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.
Conjoining Specifications \Delta 511
oe
i.snd
i.ack
oe
o.snd
o.ack
Queue Fig. 2. A queue.
Process Queue
output var i.ack , o.sig initially 0,
internal var q initially h
input var i.sig, i.val, o.ack ;
cobegin
loop \Theta
\Theta
if (i:ack 6= i:sig) - (jqj ! N)
\Theta
\Theta
then q := q ffi hi :vali;
i:ack
loop \Theta
\Theta\Theta
\Theta
\Theta\Theta
then o:val := head (q);
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:
jaej denotes the length of sequence ae, which equals 0 if ae is empty; Head(ae) and
Tail(ae) as usual denote the head (first element) and the tail of sequence ae, if ae is
nonempty; and ae ffi - denotes the concatenation of sequences ae and - . Moreover,
angle brackets are used to form sequences; so h i denotes the empty sequence, and
hei 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 behav-
ior, 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
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.
System
System
oe
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
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
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:
c asserts that c always equals 0.
d asserts that d always equals 0.
We can implement these specifications with the following two processes.
Process \Pi c Process \Pi d
output var c initially
input var d ; input var c ;
loop h c := d i endloop loop h d := c i endloop
Process \Pi c guarantees M 0
assuming M 0
d , and process \Pi d guarantees M 0
d assuming
c . Clearly, their composition leaves c and d unchanged, so it implements M 0
d .
In the second example:
c asserts that c eventually equals 1.
d asserts that d eventually equals 1.
The same processes \Pi c and \Pi d implement the specifications in this case too; process
assuming M 1
d , and process \Pi d guarantees M 1
assuming M 1
c .
However, since their composition leaves c and d unchanged, it does not implement
d .
Our conclusion in the first example does not depend on the particular choice of
processes \Pi c and \Pi d . We can deduce directly from the assumption/guarantee specifications
that the composition must implement M 0
d , 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
c and M 1
d 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 0
d 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.
Conjoining Specifications \Delta 513
the environment violates its assumption. In other words, we interpret the assump-
tion/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
\Gamma. 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/guar-
antee specifications M 0
c
\Gamma. M 0
d and M 0
d
\Gamma. M 0
implies M 0
d . 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
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 is true of every behavior. Syntactically, TLA formulas are
built up from state functions using Boolean operators (:, -, ) [implication],
and the operators 0 , 2, and 999 999, as described below.
A state function is like an expression in a programming language. Semantically,
it assigns a value to each state-for example 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 is true for hs; ti iff the value
of 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 hs; ti is an A step-for example, 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 0 for the expression obtained by priming all the variables
of the state function v, and [A] v for A - (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 2F is a formula that means that
F is always true, and 3F , an abbreviation for :2:F , means that F is eventually
true. In addition, if A is an action and v is a state function then 2[A] v is a
is an abbreviation for :2[:A] v . Using 2 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 (23hAi v ) - (23:Enabled hAi 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.
The formula 999 999x : 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
as "F with x hidden" and call x an internal variable of 999 999x : F . Both x and
x 0 are bound by 999 999x in 999 999x : F . If x is a tuple of variables hx
The standard way of specifying a system in TLA is with a formula in the "canon-
ical 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 \Delta
(b ? a) - (b
(2)
Intuitively, a variable represents some part of the universe, and a behavior represents
a possible complete history of the universe. A system \Pi is represented by a
that is true for precisely those behaviors that represent histories
in which \Pi is running. We make no formal distinction between systems, specifica-
tions, 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 ob-
jects, 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
We 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.
Conjoining Specifications \Delta 515
oe
i.snd
i.ack
oe
o.snd
o.ack
Queue
e
d
e
r
R
e
c
e
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 hc:sig ; c:vali
for a channel c; we also write c for the triple hc:sig; c:ack ; c:vali.
A channel is initially ready for sending, so the initial condition on wire c is the
predicate CInit(c) defined by
CInit(c) \Delta
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.
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 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: QM , describing the steps taken by the
component, and QE - (q describing steps taken by the environment (which
leave q unchanged). Action QM 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 QE is the disjunction of Put , which
ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.
Environment
Actions
Get \Delta
Init M
Component
Actions
Specification
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 hi; o; qi of all relevant variables. 2
-L is the weak-fairness condition ICL, which is defined to be WF hi; o; qi (QM ), 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 hi; o; qi (Enq ) - WF hi; o; qi (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
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 \Pi l represented
by M l implements the system or property \Pi 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 \Pi l .
The formula M l )M is proved by applying a handful of simple rules [Lamport
1994]. When M has the form 999
M , a key step in the proof is finding a refinement
Informally, we write hi; o; qi for the concatenation of the tuples i, o, and hqi.
Conjoining Specifications \Delta 517
oe
i.snd
i.ack oe
z.snd
z.ack
Queue1
e
d
e
r
oe
o.snd
o.ack
Queue2
R
e
c
e
e
r
Fig. 7. A complete system containing two queues in series.
26 4
Fig. 8. Specification of the complete double-queue system of Figure 7.
mapping-a tuple of state functions x such that M l implies c
M is the
formula obtained by substituting x for x (and therefore (x) 0 for x 0 ) in c
M . Under
reasonable assumptions, such a refinement mapping exists when M l ) 999
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 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
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
any formula F . This is proved by showing ICDQ ) ICQ [dbl] , with the refinement
ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.
mapping defined by
else
The formula ICDQ ) 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
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 2 R) - 2[now 0 2
(now ; 1)] 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 ex-
ample, 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
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 ae, we say that ae satisfies F iff ae can be
extended to an infinite behavior that satisfies F . For convenience, we say that the
empty sequence h i satisfies every formula (even false).
A safety property is a formula that is satisfied by an infinite behavior oe iff it
is satisfied by every prefix of oe [Alpern and Schneider 1985]. For any predicate
Init , action N , and state function v, the formula Init -2[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 oe satisfies C(F ) iff every prefix of oe
satisfies F . Formula C(F ) is the strongest safety property such that
Proposition 1 below implies that C(Init - 2[N
is the conjunction of suitable fairness properties.
Conjoining Specifications \Delta 519
3.4.2 Machine Closure. When writing a specification in the form Init -2[N
we expect L to constrain infinite behaviors, not finite ones. Formally, this means
that the closure of Init - 2[N should be Init - 2[N ] v . A pair of properties
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
A is enabled in state r n , then there exists a state r n+1 such that hr
satisfies P and hr is an A step. It follows from this definition of subaction
that, if A implies N , then A is a subaction of Init - 2[N ] v .
Proposition 1. If P is a safety property and L is the conjunction of a countable
number of formulas of the form WFw (A) and/or SFw (A) such that A - (w 0 6= 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
The obvious first step in proving such a formula is
to compute the closures C(M 1 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
to the proof of a formula in which the closures can be computed
with Proposition 1.
Proposition 2. Let x, x be tuples of variables such that for each i,
no variable in x i occurs in M or in any M j with i 6= j.
If
Proofs are in the appendix.
Some of our results also have hypotheses of the form C(M 1
where we expect E to be a safety property. If we can verify that E is a safety
property, so 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.
Additional Temporal Operators
We now define some additional temporal operators. Although they can be expressed
in terms of the primitive TLA operations 0 , 2, and 999 999, we define them semantically.
3.5.1 The Operator. The formula E+v asserts that, if the temporal formula
then the state function v stops changing. More precisely, a
behavior oe satisfies E+v iff either oe satisfies E, or there is some n such that (1) E
holds for the first n states of oe 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
d
Init \Delta
then
Init -2[ b
We need to reason about + only to verify hypotheses of the form
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 \Gamma. Operator. For temporal formulas E and M , the formula E \Gamma. M
asserts that M holds at least as long as E does [Abadi and Plotkin 1993]. More
precisely \Gamma. M is true of a behavior oe iff E )M is true of oe and, for every finite
prefix ae of oe, if E is true of ae then M is true of ae. It follows from this definition
of \Gamma. that E \Gamma. M equals (C(E) \Gamma. C(M The operator \Gamma. acts
much like ordinary implication. In fact, is equivalent to
course, it is not in general true that
3.5.3 The
\Gamma. Operator. As we observed in the introduction, we interpret the
specification that M is guaranteed under assumption E as the formula
\Gamma. M ,
which means that M holds at least one step longer than E does. More precisely,
\Gamma. M is true of a behavior oe iff is true of oe and, for every n - 0, if
holds for the first n states of oe, then M holds for the first n+1 states of oe. It
follows from this definition of
\Gamma. that
\Gamma. M equals (C(E)
\Gamma. C(M
The
\Gamma. M is stronger than E \Gamma. M , which asserts that M holds as
long as E does. It can be shown that, if E is a safety property, then
\Gamma. M
equals (M \Gamma. E) \Gamma. 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 ,
\Gamma. M equals E+v \Gamma. 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
and M to be orthogonal (?), where is true of a behavior oe iff there is no
are both true for the first n states of oe and both false for
the first n+1 states of oe. It can be shown that
are safety properties, then
\Gamma.
If no step falsifies both E and M , and M remains true as long as E does, then
must remain true at least one step longer than E does. Hence,
the equivalence of
\Gamma. M . In fact, we prove in the appendix that
ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.
Conjoining Specifications \Delta 521
\Gamma. valid. From this and the relation between
\Gamma.
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
imply
This proposition enables us to use orthogonality to remove + from proof obliga-
tions. 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
then
E) ? C(9
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. more general situation is discussed below.)
The specification of a component has the same form 999 999x : Init - 2[N as that
of a complete system. For a component specification:
-v is the tuple hx; m; ei.
-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 Nm . In an interleaving rep-
resentation, the component's inputs and outputs cannot change simultaneously,
so Nm implies e In a noninterleaving representation, Nm does not constrain
the value of e 0 , so the variables of e do not appear primed in Nm . 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 hm; xi 0 equals hm; xi. (Below, we describe more general specifications
in which an environment action can change x.) Therefore, N should equal
-L is the conjunction of fairness conditions, each of the form WF hm; xi (A) or
SF hm; xi (A). For an interleaving representation, which by definition does not
allow steps that change both e and m, the subscripts hm; xi and he; m; xi yield
equivalent fairness conditions.
522 \Delta Mart'in Abadi and Leslie Lamport
This leads us to write M in the form
By simple logic, (3) is equivalent to
For the specification M a of process \Pi 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
N a
M a
Init a - 2[N a ] a - WF a (N a )
For the specification M l
a of the low-level process \Pi l
a , the tuple x is
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
l
a
a - 2[N l
a
a
for appropriate initial condition Init l
a and next-state action N l
a . The specifications
M b and M l
b 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 hi :ack ; o:sndi, the tuple e of input variables is
hi :snd ; o:acki, and the specification is
The specification of the environment as a separate component is
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 0 or
o:ack 0 .
-Define an action DeqEnq that simultaneously enqueues an input value and dequeues
an output value, and change the definition of QM 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 simultaneously. A nonin-
terleaving 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.
Conjoining Specifications \Delta 523
Init M
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
but may just imply 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 0 6= m, let v equal
he; mi, and observe that [NM ] hm; xi equals [NM -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
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
. 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.
524 \Delta Mart'in Abadi and Leslie Lamport
shown in Figure 5. Recall that
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 h i,
so
Proposition be tuples of variables, and let
If, for all
(1) no variable of x
(3)
then
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
implies 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 ha; bi (N a
instead of WF ha; bi (N ). It can be shown that these two fairness conditions are
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: 999 999
2nd queue: 999 999
To obtain an interleaving representation, we have conjoined
M in the
ACM Transactions on Programming Languages and Systems, Vol. 17, No. 3, May 1995.
Conjoining Specifications \Delta 525
first queue's next-state action, because Q [1]
M does not mention o. Similarly, we
have conjoined 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 represen-
tations. For arbitrary representations, a straightforward calculation shows
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
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
We would like to prove that this system is implemented by a lower-level
one, consisting of components \Pi l
by proving that each \Pi l
be the specification of \Pi i and M l
i be the specification of \Pi l
. We must prove that
implies
This implication is trivially true if M l
all i. However, as we saw in the GCD example, M l
i need not imply M i .
Even when M l
does not hold, we need not reason about all the lower-level
components together. Instead, we prove
includes just
the properties of the other components assumed by component i, and is usually
much simpler than
k . Proving
reasoning only about
component i, not about the entire lower-level system.
In propositional logic, to deduce that
implies
l
may prove that
each i. However, proving this
still requires reasoning about
k , the specification of the entire lower-level
system. The following theorem shows that we need only prove that E i is implied
by
, the specification of the higher-level system-a formula usually much
simpler than
k .
Proving
each i and deducing (
reasoning, and is not sound in general. Such reasoning would
allow us to deduce (
l
equal To break the circularity, we need to add some C's and one hypothesis:
violated then, for at least one additional step, M l
implies M i . This
hypothesis is expressed formally as
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
(2) (a)
526 \Delta Mart'in Abadi and Leslie Lamport
(b)
then
l
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 l
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,
The definition of E b is analogous. We let v be ha; bi.
In general, the environment and component specifications can have internal vari-
ables. 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 proper-
ties. 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
For interleaving representations, we can then use Proposition 6 to write
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
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 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,
will not follow from C(M j ) for any single j.)
To prove part (a) of the second hypothesis, we first eliminate the +. For non-
interleaving 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.
Conjoining Specifications \Delta 527
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
implies C(M l
i ), we can infer from part (a) that
implies
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
a
a )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 l
a is an interleaving representation, its next-state action N l
a implies
that no step changes both a and b, so C(M l
a ) implies Disjoint(a; b). Hence, applying
Propositions 4 and 5, we reduce our task to proving C(E a
a
a )M a . Applying Proposition 2 to remove the quantifier from C(M l
a ) and
Proposition 1 to remove the C's, we reduce proving C(E a
a
proving
a - 2[N l
a
Using simple logic and (11), we reduce proving E a - M l
a to proving
a - 2[N l
a
a
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 spec-
ification. 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
(1)
(2) (a)
(b)
(3) v is a tuple of variables including all the free variables of M i
528 \Delta Mart'in Abadi and Leslie Lamport
then
(a)
C(M l
(b)
l
Conclusion (b) of this theorem has the same form as hypothesis 2(b), with M l
and M i replaced with conjunctions. To make the corresponding hypothesis 2(a)
follow from conclusion (a), it suffices to prove
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 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
\Gamma. 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
. The formula
\Gamma. 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
\Gamma. M therefore allow the
same implementations. We take
\Gamma. 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
\Gamma. M is equivalent to C(E)
\Gamma.
so we can in principle convert any assumption/guarantee
specification to one whose assumption is a safety property. 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 EL ) 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
is also machine closed [Abadi and Lamport 1994, Proposition 3].
Conjoining Specifications \Delta 529
5.2 The Composition Theorem
Suppose we are given n devices, each with an assumption/guarantee specification
\Gamma. M j . To verify that the composition of these devices implements a higher-level
assumption/guarantee specification
\Gamma. M , we must prove
\Gamma.
\Gamma. M ). We use the following theorem:
Theorem 3 (Composition Theorem). If, for
(1)
(2) (a)
(b)
then
\Gamma.
\Gamma. M ).
This theorem also allows us to prove conditional implementation results of the form
G-
\Gamma.
\Gamma. M ); we just let M 1 equal G and E 1 equal true, since
true
\Gamma. 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
has the form of the specification of a complete system, with
component specifications P , 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,
\Gamma.
\Gamma. 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)
(b)
then
\Gamma.
\Gamma. M ).
5.3 The Queue Example
The assumption/guarantee specification of the queue of Figure 2 is QE
\Gamma. 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
\Gamma. QM by substitution; they are QE [1]
\Gamma. QM [1] and QE [2]
\Gamma. QM [2] .
We want to show that their composition implements the (2N +1)-element queue
specified by QE [dbl]
\Gamma. QM [dbl] . The obvious thing to try to prove is
\Gamma. QM [1]
\Gamma.
\Gamma. QM [dbl] )
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 rea-
son. 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
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
\Gamma. QM [1]
\Gamma.
\Gamma. QM [dbl] )
where G is the formula
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
\Gamma. 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.
Conjoining Specifications \Delta 531
1. C(QE [dbl]
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.
2.1.
2.1.1. C(IQM [1]
Proof: Follows easily from Proposition 1 and the definitions.
2.1.2. C(QM [1]
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.
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
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 as-
sumption/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
\Gamma., 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/guar-
antee 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 ex-
amples. 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 ex-
ample: 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.
Conjoining Specifications \Delta 533



--R



Composing specifications.
The existence of refinement mappings.
A logical view of composition.
Games and full completeness for multiplicative linear logic.
Defining liveness.
An algebraic model for asynchronous circuits verification.
IEEE Trans.
Application of the composition principle to Unity-like specifications

Specification and design of (parallel) programs.
Verification of a multiplier: 64 bits and beyond.
In Computer-Aided Verification
The temporal logic of actions.
A simple approach to specifying concurrent systems.
What good is temporal logic?
Introduction to VLSI Systems.
Proofs of networks of processes.

In transition from global to modular temporal reasoning about programs.
The temporal semantics of concurrent programs.
A proof technique for rely/guarantee properties.
Conjunction as composition.
revised July
--TR
An Algebraic Model for Asynchronous Circuits Verification
A simple approach to specifying concurrent systems
In transition from global to modular temporal reasoning about programs
The existence of refinement mappings
Composing specifications
A logical view of composition
Conjunction as composition
The temporal logic of actions
An old-fashioned recipe for real time
Games and full completeness for multiplicative linear logic
Introduction to VLSI Systems
Application of the Composition Principle to Unity-like Specifications
A Proof Technique for Rely/Guarantee Properties
Verification of a Multiplier

--CTR
Jonathan S. Ostroff, Composition and refinement of discrete real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.1-48, Jan. 1999
Carlo A. Furia , Matteo Rossi , Dino Mandrioli , Angelo Morzenti, Automated compositional proofs for real-time systems, Theoretical Computer Science, v.376 n.3, p.164-184, May, 2007
Fei Xie , Guowu Yang , Xiaoyu Song, Component-based hardware/software co-verification for building trustworthy embedded systems, Journal of Systems and Software, v.80 n.5, p.643-654, May, 2007
Krishnendu Chatterjee , Thomas A. Henzinger , Marcin Jurdziski, Games with secure equilibria, Theoretical Computer Science, v.365 n.1, p.67-82, 10 November 2006
J. Niehren , J. Schwinghammer , G. Smolka, A concurrent lambda calculus with futures, Theoretical Computer Science, v.364 n.3, p.338-356, 8 November 2006
Marc Shapiro, Practical proofs of concurrent programs, ACM SIGPLAN Notices, v.41 n.9, September 2006
de la Riva , Javier Tuya, Automatic generation of assumptions for modular verification of software specifications, Journal of Systems and Software, v.79 n.9, p.1324-1340, September 2006
Arnaud Bailly , Mireille Clerbout , Isabelle Simplot-Ryl, Component composition preserving behavioral contracts based on communication traces, Theoretical Computer Science, v.363 n.2, p.108-123, 28 October 2006
Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, ACM SIGPLAN Notices, v.40 n.9, September 2005
Ralph D. Jeffords , Constance L. Heitmeyer, A strategy for efficiently verifying requirements, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September
Ansuman Banerjee , Pallab Dasgupta, The open family of temporal logics: Annotating temporal operators with input constraints, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.3, p.492-522, July 2005
Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338
Viktor Vafeiadis , Maurice Herlihy , Tony Hoare , Marc Shapiro, Proving correctness of highly-concurrent linearisable objects, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA
Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.2, p.339-369, March 2004
Harry C. Li , Shriram Krishnamurthi , Kathi Fisler, Modular Verification of Open Features Using Three-Valued Model Checking, Automated Software Engineering, v.12 n.3, p.349-382, July      2005
Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
Juergen Dingel, Computer-assisted assume/guarantee reasoning with VeriSoft, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Natasha Sharygina , James Browne , Fei Xie , Robert Kurshan , Vladimir Levin, Lessons Learned from Model Checking a NASA Robot Controller, Formal Methods in System Design, v.25 n.2-3, p.241-270, September-November 2004
Leila Barakatain , Sofine Tahar , Jean Lamarche , Jean-Marc Gendreau, Practical approaches to the verification of a telecom megacell using FormalCheck, Proceedings of the 11th Great Lakes symposium on VLSI, p.1-6, March 2001, West Lafayette, Indiana, United States
Hakan Erdogmus, Architecture-driven verification of concurrent systems, Nordic Journal of Computing, v.4 n.4, p.380-413, Winter 1997
Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
Sagar Chaki , Sriram K. Rajamani , Jakob Rehof, Types as models: model checking message-passing programs, ACM SIGPLAN Notices, v.37 n.1, p.45-57, Jan. 2002
Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, An assume-guarantee rule for checking simulation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.1, p.51-64, January 2002
Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999
variables to prove simulation of specifications, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.175-201, January 2005
L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997
Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.390-402, January 19-21, 2000, Boston, MA, USA
Michel Charpentier, Composing invariants, Science of Computer Programming, v.60 n.3, p.221-243, May 2006
Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, Decomposing refinement proofs using assume-guarantee reasoning, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
Leslie Lamport, TLA in Pictures, IEEE Transactions on Software Engineering, v.21 n.9, p.768-775, September 1995
Thomas A. Henzinger , Xiaojun Liu , Shaz Qadeer , Sriram K. Rajamani, Formal specification and verification of a dataflow processor array, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.494-499, November 07-11, 1999, San Jose, California, United States
Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997
Carl A. Gunter , Elsa L. Gunter , Michael Jackson , Pamela Zave, A Reference Model for Requirements and Specifications, IEEE Software, v.17 n.3, p.37-43, May 2000
concurrent programming;safety properties;composition;liveness properties;modular specification;decomposition;temporal logic