BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1409
ENTRY:: 1994-03-17
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Reasoning About Programs by Exploiting the Environment
AUTHOR:: Fix, Limor 
AUTHOR:: Schneider, Fred B. 
DATE:: February 1994
PAGES:: 41
ABSTRACT::
A method for making aspects of a computational model explicit in the formulas 
of a programming logic is given. The method is based on a new notion of 
environment -- an environment augments the state transitions defined by a 
program's atomic actions rather than being interleaved with them. Two simple 
semantic principles are presented for extending a programming logic in order 
to reason about executions feasible in various environments. The approach is 
illustrated by (i) discussing a new way to reason in TLA and Hoare-style 
programming logics about real-time and by (ii) deriving the first TLA and 
Hoare-style proof rules for reasoning about schedulers.
END:: CORNELLCS//TR94-1409
BODY::
Reasoning About Programs by
Exploiting the Environment*
Limor Fix
Fred B. Schneider
TR 94-1409
February 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
* This material is based on work supported in part by the Office of Naval Research
under contract N00014-91-J-1219, AFOSR under proposal 93NM312, the National
Science Foundation under Grant No. CCR-8701 103, and DARPNNSF Grant No.
CCR-9014363. Any opinions, findings, and conclusions or recommendations
expressed in this publication are those of the author and do not reflect the views of
these agencies. Limor Fix is also supported, in part, by a Fullbright post-doctoral
award.
Reasoning about Programs by
*
Exploiting the Environment
Limor Fix
Fred B. Schneider
Department of Computer Science
Cornell University
Ithaca, New York 14853
February 2, 1994
ABSTRACT
A method for making aspects of a computational model explicit in the formulas of a pro-
gramming logic is given, The method is based on a new notion of environment--Han en-
vironment augments the state transitions defined by a program's atomic actions rather than
being interleaved with them. Two simple semantic principles are presented for extending a
programming logic in order to reason about executions feasible in various environments.
The approach is illustrated by (i) discussing a new way to reason in TLA and Hoare-style
programming logics about real-time and by (ii) deriving the first TLA and Hoare-style proof
rules for reasoning about schedulers.
This material is based on work supported in part by the Office of Naval Research under contract N00014-91-J-1219,
AFOSR under proposal 93NM312, the National Science Foundation under Grant No. CCR-8701 103, and DARPAiNSF
Grant No. CCR-9014363. Any opinions, findings, and conclusions or recommendations expressed in this publication are
those of the author and do not reflect the views of these agencies. Limor Fix is also supported, in part, by a Fullbright post-
doctoral award,
1. Introduction
What behaviors of a concurrent program are possible may depend on the scheduler, instruction
timings, and other aspects of the environment in which that program executes. For example, consider
the program of Figure 1.1. Process P1 executes an atomic action that sets y to 1 followed by one that
sets y to 2. Concurrenfly, process P2 executes an atomic action that sets y to 3. If all behaviors of
this concurrent program were possible, then the final value of y would be 2 or 3. The environment,
however, may rule out certain behaviors.
0
0
Suppose P1 has higher-priority than P2 and the environment selects between executable atomic
actions by using a priority scheduler. Behaviors in which actions of P2 execute before those of
P1 are now infeasible, and the final value ofy cannot be 2.
Suppose the environment uses a first-come first-served scheduler to select between executable
atomic actions. Behaviors in which P2 executes after the second action of P1 are now infeasi-
ble, and the final value ofy cannot be 3.
Thus, changing the environment can affect what properties a program satisfies.
Programming logics usually axiomatize program behavior under certain assumptions about the
environment. Logics to reason about real-time, for example, axiomatize assumptions about how time
advances while the program executes. These assumptions abstract the effects of the scheduler and the
execution times of various atomic actions. A logic to reason about the consequences of resource con-
straints would similarly have to axiomatize assumptions about resource availability.
If assumptions about an environment are made when defining a programming logic, then
changes to the environment may require changes to the logic. Previously feasible behaviors could
become infeasible when the assumptions are strengthened; a logic for the original environment would
then be incomplete for this new environment. Weakening the assumptions could add feasible
behaviors; the logic for the original environment would then become unsound. For example, any of
the programming logics for shared-memory concurrency (e.g. [OG76j) could be used to prove that
program of Figure 1.1 terminates withy=2 ory=3. But, these logics must be changed to prove that
y =2 necessarily holds if a first-come first served scheduler is being used or that y =3 necessarily holds
if a priority scheduler is used. As another example, termination of the program in Figure 1.2 depends
on whether unfair behaviors are feasible. (Usually they are not.) Logics, like the temporal logic of
[MP89j, that assume a fair scheduler become unsound when this assumption about the environment is
relaxed.
cobegin
P1: y:=l; y:=2
II
P2: y:=3
coend
Figure 1.1. A concurrent program
-1-
cobegin
P1: b :=false
/1
P2: dob? skipod
coend
Figure 1.2, Termination with fairness
This paper explores the design of programming logics in which assumptions about the environ-
ment can be given explicitly. Such logics allow us to prove that all feasible behaviors of a program
satisfy a property, where the characterization of what is feasible is now explicit and subject to change.
We give two semantic principles--Hprogram reduction and property reduction--Hfor extending a pro-
gramming logic so that explicit assumptions about an environment can be exploited in reasoning.
These principles allow extant programming logics to be extended for reasoning about the effects of
various fairness conditions, schedulers, and models of real-time; a new logic need not be defined
every time a new model of computation is postulated. We illustrate the application of our two princi-
ples using TLA [1,91] and a Hoare-style Proof Outline Logic [594]. In TLA, programs and properties
are both represented using a single language; in Proof Outline Logic these two languages are distinct.
The remainder of this paper is structured as follows. In section 2, our program and property
reduction principles are derived. Then, in section 3, program reduction is applied to TLA. In section
4, property reduction is used to drive an extension to a Hoare-style logic. Section 5 puts this work in
context. The appendix contains the completeness proof for the extended Hoare-style logic.
2. Formalizing and Exploiting the Environment
A programming logic comprises a sound and complete deductive system for verifying that a
given program satisfies a property of interest. We write (5, "s? E Sat to denote that a program 5
satisfies a property "s; each programming logic will have its own syntax for saying this. In any given
programming logic, a program language is used to specify 5 and a property language, perhaps identi-
cal to the program language, is used to specify "s.
Usually, both the program 5 and the property "s define sets of behaviors, where a behavior is a
mathematical object that encodes a sequence of state transitions resulting from program execution,
and a state is a mapping from variables to values. Notice that
o+ the set [[5 ? of behaviors for a program 5 constrains only the values of program variables', and
o+ the set [["sJI of behaviors for a property "s may also constrain the values of variables that are
not program variables.
A program 5 satisfies a property "s exactly when all of the behaviors of 5 are behaviors permit-
ted by"s:
1Program variables include all those declared explicitly in the program Ils well as others, lilte program counters and
message buffers, concerning aspects of the state implicitly involved in executing the program.
-2-
(5, `P?E Sat ifand only if `[SJIa'[W?
(2.1)
The environment in which a program executes defines a property too. This property contains
any behavior that is not precluded by one or another aspect of the environment. For example, a prior-
ity scheduler precludes behaviors in which atomic actions from low-priority processes are executed
instead of those from high-priority processes. As another example, the environment might define the
way a distinguished variable time (say) changes in successive states, taking into account the processor
speed for each type of atomic action.
For E the property defined by the environment, the feasible behaviors of a program 5 under E
are those behaviors of 5 that are also in E: `[S j]n'[E JI. A program 5 satisfies a property `P under an
environment E, denoted (S, E, W? E ESat, if and only if every feasible behavior of 5 under E is in "I:
(S,E,W??ESat if and only if (`[SJI?'[E?)a?'[W]I (2.2)
Thus, a sound and complete deductive system for verifying (5, E, W?E ESat would permit us to
prove properties of programs under various assumptions about schedulers, execution times, and so on.
Defining a separate logic to prove (5, E, `I'?E ESat is not always necessary if a logic to prove
(S, `P?E Sat is available. For properties 4' and `I', let property 4'(m'P be [[4'?n'[ `PJI and let property
4'?? be `[4' ??`[ "I ?. Then, one reduction from ESat to Sat is derived as follows.
(5, E, `P?E ESat
iff definition (2.2) of ESat
iff definition (2.1) of Sat
(5r?E, `I'?E Sat
Thus we have:
Program Reduction: (5, E, ?`? E ESat if and only if (5rmE, `I'? E Sat.
(2.3)
Program Reduction is useful if the logic for (5, ?P? E Sat has a program language that is closed under
intersection with the language used to define environments. Section 3 shows this to be the case for
Lamport's TLA; it is also the case for most other temporal logics.
A second reduction from ESat to Sat is based on using the environment to modify the property
(rather than the program).
(5, E, `P?c ESat
iff definition (2.2) of ESat
(`[5 jIrm'[E j])a?'[WJI
iff set theory _____
`[5?a4'['PJI ? `[ETh
iff definition (2.1) of Sat
(5, `P?E? E Sat
This proves:
Property Reduction: (5, E, `P? E ESat if and only if (5, W&jE? E Sat.
(2.4)
Property reduction imposes no requirement on the program language, but does require that the pro-
perty language be closed under union with the complement of properties that might be defined by
environments. An example of a logic whose property language satisfies this closure condition is
-3-
cTL* [EH86].
When neither reduction principle applies, then we can reason about the effects of an environ-
ment by extending the logic being used to establish (5, ?) E Sat. Extensions to the program language
allow Program Reduction to be applied; extensions to the property language allow Property Reduc-
tion to be applied. Section 4 illustrates how this might be done, by extending the property language
of a Hoare-style logic called Proof Outline Logic.
3. Environments for TLA
The Temporal Logic of Actions (TLA) is a linear-time temporal logic in which programs and
properties are represented as formulas. Thus, the program language and property language of TLA
are one and the same. This single language includes the usual propositional connectives, and the
TLA formula F A G defines a property that is the intersection of the properties defined by F and G.
TLA is, therefore, an ideal candidate for Program Reduction.
3.1. TLA Overview
A TLA state predicate is a predicate logic formula over some variables.2 The usual meaning is
ascribed to s?p for a state s and a state predicate p: when each variable v in p is replaced by its value
s(v) in state s, the resulting formula is equivalent to true. For example, in a state s that maps y to 14
and z to 22, sky+l <z holds because s(y)+ l<s(z) equals 14+1<22, which is equivalent to true.
A ThA action is a predicate logic formula over unprimed variables and primed variables.
Actions are interpreted over pairs of states. The unprimed variables are evaluated in the first state s of
the pair (s, t) and the primed variables are evaluated, as if unprimed, in the second state t of the pair.
For example, if s(y) equals 13 and t(y) equals 16 then (s, t)ky+l <y' holds because s(y)+l <t(y) is
equal to 13+1 <16, or, true.
In order to facilitate writing actions that are invariant under stuttering, TLA provides an abbre-
viation. For action A and list k of variables x1, x2X?, the action3 [?x is satisfied by any pair
(s, t) of states such that (s, t)kA or the values of the Xj are unchanged between s and t. Writing x' to
denote the result of priming every variable in xTh we get:
[Aj?-: A v
ThA actions define state transitions. Therefore, they can be used to describe the next-state rela-
tion of a concurrent program, a single sequential process, or any piece thereof. For this purpose, it is
useful to define a state predicate satisfied by any state from which transition is possible due to an
action A. That state predicate, Enbl(A), is defined by:
s?Enb1(A) if and only if Exists t: (s, t)?A
Each formula ? of TLA defines a property If ? JI, which is the set of behaviors that satisfy ?,
where a behavior is represented by a sequence of states. Let a be a behavior 8o5 1.. , let p be a state
predicate, let A be an action, and let x be a list of variables. The syntax of the elementaryformulas of
2We assume that variable names do not contain the character (prime).
?LA actually allows subseript X to be an arbitr&y state function whose value will remain unchanged.
-4-
TLA, along with the property defined by each, is:
?E [[p?			iff So?P
CE ff E][A\x? iff Foralli,i>?O: (Si,Si+i)?[A]x
The remaining formulas of TLA are formed from these, as follows. Let ? and `I' be elementary TLA
formulas or arbitrary ThA formulas.
iff a?[[(t'Jj
a?I[?v'I']j iff a?([[???I[??
CE I[?A'I'? iff ?E (I[?JI(Th[['I'?
oE[[??'I'? iff ?E???v'P]j
iff Foralli,i>O: SjS?+1...k?
iff ?E[[?E]???
A ThA formula ? is valid if and only if for every behavior ?, (3E ? ? JI holds. Validity of
? "I implies that every behavior ? is in [[? ? `P?. From the definition above for ? E ? "I
we have that if ? ? `1' is valid then every ? in ff ? JI is also in I[ `+`JJ. Accordingly, we conclude:
??Wisvalid ifand only if (?,`P??Sat
To prove that a program S satisfies a property `I' using TLA, we
(1) construct a TLA formula ?s such that [[?? J] is the set of behaviors of S, and
(3.1)
(2) prnve(t)5?'f'valid.
As an example, we return to the program of 1. It is reproduced in Figure 3.1, with each atomic
action labeled. The ThA formula ?s that characterizes behaviors for this program is
??: mit5 A ?[As]y,pc1,pc2			(3.2)
where mit5 is a state predicate defining initial states of the program's behavior and A5 is a ThA
action that characterizes the program's next-state relation. In defining the effect of each atomic
action, variable ?Cj denotes the program counter for process Pj and value "$" is assumed to be dif-
ferent from the entry (control) point for any atomic action of the program.
cobegin
P1: o:: y =1;
?: y =2
1/
P2: y: y:=3
coend
Figure 3.1. A concurrent program
-5-
mit5: pcl=(xAPC2=Y
A5:			? v			v
?: pci=L A A y'=l A pC2=pC2
?:			pci=I3 A pci,=$ A			A pC2=pC2
A?: pC2=? A pc2,=$ A y'=3 A pC1=?C1
3.2. Exploiting an Environment with TLA
If the property defined by an environment can be characterized in TLA, then Program Reduc-
tion can be used to reason about feasible behaviors under that environment. We prove ? A E => W to
establish that behaviors of the program characterized by 4' under the environment characterized by E
are in the property characterized by W:
4' A E ?`P is valid
iff			definition (3.1)
(4'AE,W?E Sat
iff			definition (2.1)
iff <([FAGjj=[fF??[fGj1
(I[4'JI?[[E jj)a?[['PJ]
iff definition (2.1)
(4'c?, `P?E Sat
iff Program Reduction (2.3)
(4', E, `P?? ESat
The utility of this method depends on (i) being able to prove 4' A E => `V when it is valid and
(ii) being able to characterize in TLA those aspects of environments that interest us. A complete
deductive system for TLA (see [L9l], for example) will, by definition, be complete for proving
4' A E ? `V. In fact, this is one of the advantages of using Program Reduction to extend a complete
proof system for Satinto a proof system for ESat--Hthe complete proof system for ESatcomes at no
cost. Examples in the remainder of this section convey a sense for how an environment is represented
by a TLA formula.
3.3. Schedulers as TLA formulas
If there are more processes than processors in a computer system, then processors must be
shared. This sharing is usually implemented by the scheduler of an operating system. To use Pro-
gram Reduction with TLA and reason about execution of a program under a given scheduler, we
write a TLA formula E to characterize that scheduler.
Many schedulers implement safety properties--Hthey rule out certain assignments of processors
to processes. Formalizations for these schedulers have much in common. Let fi be the set of
processes to be executed in a system with N processors. For each process It, two pieces of informa-
tion are maintained (in some form) by a scheduler:
acnve?: whether there is a processor currently allocated to It
rank?: a value used to determine whether a processor should be allocated to It
-6-
Only a single atomic action from one process can be executed at any time by a processor. This
restriction is formalized as predicate Alloc (N), which bounds the number of processes to which N
processors can be allocated at any time:4
Alloc(N): (#itE fi: acnve?)?<N
The restriction that processes that have processors allocated are the only ones that advance is
formalized in terms of A? the next-state relation for a process ?. We assume that these next-state
relations are disjoint.
Pgrs(?): Ait ? acnve?
Finally, we formalize as Run(::) the requirement that acnve? holds only for those processes
with sufficiently large rank.
Run(?): acflve? ? Iarger(it)
where:
1arger(?: (it' rnnk?<rank?J
In afired-pnonty scheduler, there is a fixed value v? associated with each process it. A process
that has not terminated and has higher priority is executed in preference to a process having a lower
priority. This is ensured by assigning ranks as follows.
? (rank?=v?)) A (pc?=$ => (rank?=O))
Prio(it):
A fixed-priority scheduler is thus characterized by
Fixedpno: EI[AIloc(N) A (Vit E H: Pgrs(it) A Run (it) A Prio(it))]?-
where xis a list of all the variables in the system. For example, x for the program of Figure 3.1 would
havepc1,pc2,y, acttve?1, rankp1, acdve?2, and rankp2.
In a first-come first-served scheduler, processes are ranked in accordance with elapsed time
since last executed. We can model this by assigning ranks that are increased for processes that have
not had an action executed.
Age(H): (VitE H: (A? ? (rank?'=O)) A (rnA? ? (rank?'=rank?+l)))
A first-come, first-served scheduler is therefore characterized by
FCFS: (VitE H: rank?=O) A EI[Alloc(N) A (VitE H: Pgrs(it) A Run(it)) ?Age(H)%-
where xis a llst of all the variables in the system.
Both of these schedulers can allocate a processor to a process, even though that process may he
unable to make progress. It is wasteful to allocate a processor to process it when Enb1(??) does not
hold (because it has terminated or because its next atomic action is not enabled). A variant of Fix-
edPrio that allocates processors only to non-terminated and enabled higher-priority processes is:
EnblFixedPrio: EI[Alloc(N) A (VitE H: Pgrs(it) A Run(it) A EnblPflo(it))]x?
where
4We use the notation (#x e P: R) for "the number of distinct values of x in P for which R holds"
-7-
Enbl"'n'o(it): (Enbl(A?) ? (rnnk?=v?)) A (?,Enbl(??) ? (rank?=O))
As before, xis a list of all the variables in the system.
A difficulty with assigning fixed priorities to processes is that execution of a high-priority pro-
cess can be delayed awaiting progress by processes with lower-priorities. For example, suppose a
high-priority process itH is awaiting some lock to be freed, 50 itH is not enabled. If that lock is owned
by a lower-priority process itL, then execution of itH cannot proceed until itL executes. This is known
as a pn'on'? inversion [SRL9O][BMS93], because execution of a high-priority process depends on
resources being allocated to a lower-priority process.
Pn'on'? Inheritance schedulers give preference to low-priority processes that are blocking
high-priority processes. This is done by changing process priorities. The low-priority process inher-
its a new, higher priority from any higher-priority process it blocks. Priority inheritance schedulers
exhibit improved worst-case response times in systems of tasks [SRL9O], and they have become
important in the design of real-time systems.
A priority inheritance scheduler must know what processes are blocked and how to unblock
them. In systems where acquiring a lock is the only operation that blocks a process, deducing this
information is easy: execution of the process that has acquired a lock is the only way that a process
awaiting that lock becomes unblocked.
To describe systems with locks in TLA, we employ a variable lOCkj for each lock; ThA actions
for acquiring and releasing a lock by process it are:
acquire(lock?, it): l0ck?=FREE A lOCkj'=it
release(lock?): lock?'=FREE
Notice that lock?=FREE is implied by Enbl(A?) when process it is waiting to acquire lock?.
In a priority inheritance scheduler, each process it is assumed to have a priority v1t. The rank of
a process it is the maximum of v1t and the priorities assigned to processes that are blocked by it.
Thus, rnnk1t is the maximum of Vp for the process p satisfying lock?=p (i.e. the priority of the current
lock holder) and Vq for the process q satisfying Enbl(p')? (lock?=FREE) (i.e. the priority of the pro-
cess attempting to acquire lock?). For simplicity, we assume a system having a single lock, lock.
Prioinher(it):
?(?Enbl(A1t) ? (rnnk1t=O)) A
(lock=it A Enbl(A1t)
? (rnnk1t=(maxp E H: (Enbl(p) ? lock=FREE) v lock=p: Vp))) A
(lock?it A Enbl(A1t) ? (rank1t=v1t))?
Again, x is a list of all the variables in the system. A priority inheritance scheduler is thus character-
ized by
InhPrio: E][Alloc(N) A (VitE H: Pgrs(it) A Run(it) A Pn'oThher(it))J?-
Not all schedulers are safety properties. Even schedulers that implement safety properties are
often abstracted in programming logics as implementing (weaker) liveness properties. Such a live-
ness property gives conditions under which an action or process will be executed eventually. A sim-
ple example is the following, which implies that an enabled process with sufficiently high priority
will execute,
FAIR: (VitE fi: ?[Z1(itE TOP(n, fi) A Enbl(it)): ??? H A1th)
-8-
Other examples of such liveness properties include weakfairness WFx?(A) and strongfairness SFx(A)
of TLA.
TLA Reasoning about Schedulers
In section 3.2, we showed that given TLA formulas ?s and E for a program and scheduler
respectively, ?5 A E W is valid iff behaviors of S under E satisfyW. Returning, for example, to
the program of Figure 3.1, we prove as follows that assuming a fixed-priority scheduler, a single pro-
cessor (i.e. N=1), Vp1 =2 and vp2 =1 implies that y=3 will hold upon termination. The property that
y=3 holds upon termination of S is formulated in ThA as:
5(?Enb1(A5) ?
Thus, for ?? as defined by (3.2), we must prove:
?5?FixedPno?!Z1(N=1?vp=2?Vp2=l?H=(P?,P?))
? [rn](?Enb1(A5) ?y=3).
(3.3)
In general, one proves a TLA formula iflit A (ZI[A] A ? EIC by finding a predicate 1, called
an invariant, and proving5 init ? 1, I ? C, and I A A A B A ? I'. The first obligation establishes
that I holds initially, the second implies that C holds whenever I does, and the third ensures that I
holds throughout.
For proving (3.3), we choose6:
init:			mit5
?[A]: ?[Asiy,pc PC2 A FixedPrio
B: N=1 AVp1=2AVp2=l
For I, the following suffices--Hthe proof is left to the reader:
I: (?,Enb1(As) ?y=3) A ((pcp1 ?$) => (pcp2=y))
3.4. Real time in TLA
The correlation between execution of a program and the advancement of time is largely an
artifact of the environment in which that program executes. The scheduler, the number of processors,
and the availability of other resources all play a role in determining when a process may take a step.
To reason with TLA about properties satisfied by a program in such an environment, we simply
characterize the way time advances and then use Program Reduction. Various models of real-time
one finds in the literature differ only in their characterization of how time advances.
When only a single processor is assumed, then process execution is interleaved on that proces-
sor. One way to abstract this is to associate two constants with each atomic action ot:
e?: the fixed execution time of atomic action ot on a bare machine
5A' denotes the formula obtained by priming each un-primed free variable in A.
?fhe choice of B is based on applying the Temporal Logic axiom (E]E A ElF)=tml(E A
-9-
8?: the maximum time that can elapse from the time that the processor is allocated for
execution of CL until CL starts executing.
Execution of CL is thus correlated with the passage of between ea and ea+5? time units.
The following TLA formula is satisfied by such behaviors. Variable T is the current time and
ATOM(S) is the set of atomic actions in 5. Recall that ? defines atomic action CL.
T=O A E[ A (??(T+ea<T'<?T+ea+5?))li?
AT0M(S)
As before, xis a list of all variables in the system.
Another common model of how time advances abstracts the case where each process is exe-
cuted on its own processor. We assume that the next action to be executed at process ? is uniquely
defined at each control point (Other assumptions are possible, and these can be formalized also.)
We formalize this environment in TLA, by using a separate variable T? for each process it:
T?: the time process it arrived at its current state.
System time T is the maximum of the T?:
SysTme: T=????n?(Th)
And each individual process it must execute its next action CL (say) before e +5a has elapsed from
the time it reached its current state. Let the label on action CL be "CL".
LclTme: ?itE II: pc1t=CL. T?Th<ea+5a)
The range pc7t=CL is satisfied by states in which the program counter for process it indicates that CL is
the next atomic action to be executed; the body requires CL to be executed before the system's time
has advanced too far.
Finally, the value of T? changes iff an atomic action from process it is executed:
LclTmeUpdt: (VitE H: (VCLE ATOM(S): ?: m+e?<Th'<?Th+ea+&
A (V?E H: ??it: T?'=T?)))
Here, the range is satisfied only by steps attributed to atomic action CL of process it; the body causes
all of the T? to be updated.
Putting all these together, we get a TLA formula characterizing this model of real time:
T=O A (VitE fl: Th=O) A A (SysTme A LclTme A LC?meUPdt)ix (3.4)
(lE AT0M(S)
An Old-fashioned Recipe
The scheme just described works by restricting the transitions allowed by each action. These
restrictions ensure that an action only executes when its starting and ending times are as prescribed by
the real-time model. Thus, the approach regards the environment as augmenting each action of the
original system. The environment executes simultaneously with the system's actions.
A somewhat different approach to reasoning about real-time with TLA is described by Lamport
and Abadi in "An old-fashioned recipe for real-time" [AL9l]. That recipe is extended for handling
schedulers in [LJJ93]. Like our scheme, the recipe does not require changes to the language or
deductive system of TLA. However, unlike our scheme, additional actions are used to handle the
passage of time. These new actions interleave with the original program actions, updating a clock
-10-
and some count-down timers.
There seems to he no technical reason to prefer one approach to the other. In the examples we
have checked, the old-fashioned recipe is a bit cumbersome. A variable now analogous to our vari-
able T is used to keep track of the current time, and a variable, called a timer, is associated with each
atomic action whose execution timing is constrained. Timers ensure (i) that the new actions to
advance now are disabled when actions of the original program must progress and (ii) that actions of
the original program are disabled when now has not advanced sufficiently. The timers, now, and
added actions implement what amounts to a discrete-event simulation that causes time to advance and
actions to he executed in an order consistent with timing constraints. To write real-time
specifications, it suffices to learn the few TLA idioms in [AL9 I] and repeat them. However, to prove
properties from these specifications, the details of this discrete event simulation must be mastered.
4. Environrnents for a Hoare-style Proof Outline Logic
We now turn our attention to a second programming logic?ne that is quite different in charac-
ter from TLA. The formulas of a Hoare-style logic are imperative programs in which an assertion is
associated with each control point. This niles out Program Reduction (2.3), because imperative pro-
gramming languages are generally not closed under intersection of any sort.7 Similarly, Property
Reduction (2.4) is ruled out hecause the property language, annotated program texts, also lacks the
necessary closure. However, it is not difficult to extend the property language of a Hoare-style logic
and then apply Property Reduction (2.4). An example of such an extension is given in this section.
4.1. A Hoare-style Logic
Consider a simple programming language having assignment, sequential composition, and
parallel composition statements.8 An example program is given in Figure 4.1; it is equivalent to the
program of Figure 1.1.
The syntax of programs in our language is given by the following grammar. There, ? is a label,
x is a program variable, and E is an expression over the program variables.
X: [S /1 S]
S::=			X:[x:=E]			X:[S; Si I
Every label in a program is assumed to be unique. In the discussion that follows, the lahel on
the entire program is used to name that program. In addition, for a statement ?: [...],we call "X: ["the
X: [ X1: [ X11: [y =1];
X12: [y =2]]
/1
X2: ty =3]]
Figure 4.1. Simple Program
7Constraint?maintenance languages are the obvious exception.
8Handling an ianperative language with if and do is not fundamentally different.
-11-
opening of ?, call "i" the closing, and define Lab(? to be the set containing label ? and all labels
used between the opening and closing of X.
A program state assigns values to the program variables and to control variables. The control
variables for a program ? are at(?), in(X'), and after(?) for every label ? in Lab(?).
The set ? of program states contains only those states satisfying certain constraints on the
values of control variables. These constraints are given in Figure 4.2. They ensure that the control
variables encode plausible values of program counters. For example, the constraints rule out the pos-
sibility that control variables at(X) and after(? are both true in a state. As another example, the con-
straints imply that any state for program ? of Figure 4.1 assigning true to after(?11) must also assign
true to at(?i?).
The executions of a program ? defines a set of behaviors. It will be convenient to represent a
behavior using a triple ?a, i, I') where o is an infinite sequence9 of states, i is natural number, and I is
a natural number satisfying i<?j or is oo. Informally, behavior (o, i, j? models a (possibly partial) exe-
cution starting in state o[i i that produces sequence of states a[i..j]. Prefix ?[..i --H 1] is the sequence of
states that precedes the execution; suffix ?U..] models subsequent execution.
Each state 5 of a program ? satisfies:
CO: 5 k(in(X)?after(X))
Cl: sk?(at(? A after(X))
C2: s?(at(X) in(?)
C3: For every assignment statement ?: [x := EJ:
st=(at(? =
C4: For every sequential composition X: [??: [S 1]; ?2
sk(at(X) = at(?1))
s?(after(? = afler(X2))
sk(after(?1) = at(?2))
s?((in(?1) v in(?2)) =>
sk??n(?1) A
C5: For every parallel composition ?: [??: [S 1] /1 ?2 [S2]]:
= (at(?1) A
st=(after(X) = (after(?j) A after(X2)))
= ((in(?1) v after(X1)) A (in(?) V after(X2)) A (after(X1) A after(X2))))
Figure 4.2. Constraints on control variables
9For an infinite sequence o=S? Si we write: ?[i] to denote S?; ?[..i] to denote prefix s0s1 ... &j; ct[i..j to denote suffix
s 5			and o[i..j], where i<j, to denote subsequence 5
-12-
Formally, we define the set [[X ? of behaviors for a program ? in terms of relations R ?: [x
for the assignments ? in ?:
?, t)E R?: [x :=E] iff s?at(X'), tt=after(X'), t(x)=s(E), and (4.1)
s(v)=t(v) for all program variables v different from x.
Let Assig(?) be the subset of Lab(?) that are labels on assignment statements in X. Behavior (?, i, i?
is defined to be an element of I[ X JI iff
For all k, i<k<j: Exists X'E Assig(?: (?[k], c[k+l]?E R? [x :=E] (4.2)
`Thus, each pair of adjacent states in o[i.j] models execution of some assignment statement and the
corresponding changes to the target and control variables.
Proof Outlines
Having defined the program language, we now define the property language of Proof Outline
Logic. A proof outline for a program X associates an assertion with the opening and closing of each
label in Lab(?. The assertion associated with the opening of a label X is called the precondition of X
and is denoted pre(?; the assertion associated with its closing is called the postcondition of ? and is
denoted post(?.
Here is a grammar giving a syntax of proof outlines for our simple programming language.
(p) ?
(pJ X:
PO			[x:=E](qJ
[PO1; PO2j (q)
[P01 I/P02J (qJ
P01 and PO2 are proof outlines, and p and q are assertions. A concrete example of a proof outline is
given in Figure 4.3. It contains a proof outline for the program of Figure 4.1. Easier to read nota-
tions10 for proof outlines do exist; this format is particularly easy to define formally, so it is well
(true)
X: [(true)
??: [ (true)
X11: [y := 1] (y=l vy=3J;
(y=l vy=3)
X12: [y :=2j (y=2vy=3)
(y=2vy=3)
1/
(true)
[y:=3? (y=2vy=3)
(y=2 vy=3)
Figure 4.3. Example Proof Outline
10For example, we sometimes write (p ? Po(X) (q to denote a proof outline that is identical to PO(? but with p re-
placing pre(? and q replacing pos(X).
-13-
suited to our purpose
Assertions in proof outlines are formulas of a first-order predicate logic. In this logic, terms and
predicates are evaluated over traces, finite sequences of program states. A trace ?o?i . s? that is a
prefix of a program behavior defines a current program state s? as well as a sequence 5o5 1.. 5n-1 of
past states. Thus, assertions interpreted with respect to traces can not only characterize the current
state of the system, but can also characterize histories leading up to that state. Such expressiveness is
necessary for proving arbitrary safety properties and for describing many environments.
The terms of our assertion language include constants, variables, the usual expressions over
terms, and the past term e'T for `T any term [594j?11 The e operator allows terms to be constructed
whose values depend on the past of a trace. For example, x+Q- evaluated in a trace ?o 5j ?2 equals
s2(x)+s1 (y). More formally, we define as follows the value 9?f[ `T\T of a term `Tin trace T, where c is
a constant, v is a variable, and "i and `T2 are terms.
term'T 9?4t `Tiso ?i ... sn
c			c
V
`T1+'T2 ?`Ti isosi ...5?
+ ?`T2 isosi ...sn
ifn>O
Predicates of the assertion language are formed in the usual way from predicate symbols, terms,
propositional connectives, and the universal and existential quantifiers. It is also convenient to regard
Boolean-valued variables as predicates. This allows control variables to be treated as predicates. It
also allows etrue to be treated as a predicate whose value is true in any trace having more than one
state. Assertions are just predicates.
Proof outlines define properties. Informally, the property defined by a proof outline PO(?
includes all behaviors (a, i, j? in which execution of X starting in state a[i] does not cause proofout-
line invariant I??? to be invalidated. The proof outline invariant implies that the assertion associ-
ated with each control variable is true whenever that control variable is true:
Ipo?) ?E ?A???((?t(X') ?pre(?)) A (afler(?) ?post(X')))
(4.3)
It is easier to reason about proof outlines when the precondition for each statement ? summar-
izes what is required for 4o? to hold when at(X') is true. For a proof outline PO(X), this self con-
sistency requirement is:
For every label X' E Lab(?:
If? labels a sequential composition X': [X1: [S1]; ?2 [S2i] then:
11The Proof Outline Logic of [594] also allows recursively-defined terms using 0-. This increases the expressiveness
of the assertion language, but is independent to the issues being addressed in tius paper. Therefore, in the interest of simpli-
city, we omit such terms from the assertion language.
-14-
pre(?) ?pre(?1)
post(?1) ?pre(X2)
If? labels aparallel composition X': [X1: [51] 1/ ?2 [S2]j then:
pre(?) ? (pre(?1) ?pre(?2))
We can now formally define the set [PO (X) ji of behaviors in the property PO (?:
e if PO (? is not self consistent
I[PO(??:			((a,i,j? a[..i]?jp0? or forallk, i<?kSj: a[..k]k40?)			(4.4)
Thus, [[PO(?) ji is empty if PO(? is not self-consistent. And, if PO(?) is self consistent, then
I[ PO(X) ? includes a behavior (a, i, ]? provided either (i) 1F0(S) is not satisfied when execution is
started in state a[i] or (ii) 1P0(S) is kept true throughout execution started in state a[i]. In the
definition, proof outline invariant 1P0(S) is evaluated in prefixes of a because assertions may contain
terms involving 0-.
A proof outline is defined to be valid iff (?, PO (?) E Sat holds, where
(? PO(?) E Sat if and only if [[X?a?[[PO(? JI			(4.5)
as prescribed by (2.1). Appendix A contains a sound and complete proof system for establishing that
a proof outline is valid. Such logics have become commonplace since Hoare's original proposal
[H69]. The particular axiomatization that we give is based on [594], which, in turn, builds on the
logic of [L80].
4.2. Exploiting an Environnient with Proof Outlines
Our program language does not satisfy the closure conditions required for Program Reduction
(2.3), nor does the property language (proof outlines) satisfy the closure conditions required for Pro-
perty Reduction (2A). To pursue property reduction, we define a language EnvL that characterizes
properties imposed by environments. We then extend the property language so that it satisfies the
necessary closure condition for property reduction.
We base EnvL on the assertion language of proof outlines. Every formula of EnvL is of the
form (ZIA where A is a formula of the assertion language. [TIA defines a set of behaviors as follows.
[[OA]j: ((a,i,j?			Forallk,i<?k<1: a[..k]kA)
Thus, [ZIA contains behaviors (a, i, j) for which prefixes a[..i], a[..i+lja[..]] do not violate A.
Formulas in EnvL define safety properties, and EnvL includes all of the scheduler and real-time exam-
pies of 3.3 and 3.4. A more expressive assertion language (e.g. the one with recursive terms in
[594]) would enable all safety properties to be defined in this manner.
In order to close the property language of Proof Outline Logic under union with the comple-
ment of [[E]A]l, we introduce a new form of proof outline. A constrained proofoutline is a formula
? PO(X), where A is a formula of the assertion language and PO(X) is an ordinary proof outline.
The property defined by a constrained proof outline is given by:
[?A?PO(X)JI: [PO(X)]]Q)[[?A?
(4.6)
I[ 5A]l denotes the complement of [[?A JI. Generalizing from ordinary proof outlines, a constrained
proof outline EJA H PO(X) is considered vahdiff(X, E]A ? PO(??E Sat. Thus, if?A ? PO(X) is
-15-
valid then [[?j] ? I[E]A ? PO(X)JI holds.
The set of properties defined by constrained proof outlines and proof outlines does satisfy the
necessary closure condition for property reduction. Given a program ?, let L? be the set of con-
strained proof outlines and proof outlines for ?. The required closure condition is equivalent to:
Lemma: For any assertion A and any ? E L?, there exists a constrained proof outline ?` in
? suchthat
= ??]i?[[E1AJJ
Proof. The proof is by cases.
Case: ? is an ordinary proofoutline. In this case, choose ?` to be ElA H
Case: ? is a constrained proof outline ?B ? PO(?. In this case, choose ?` to be
E](A A ? PO(X). This choice is justified by the following.
?,i,j')E [[[1(A AB)?PO(X)j]
iff definition (4.6) of [[ E](AAH PO(X) ?
(o,i,j?E([[PO(X)JIYI[?(AAB)JI)
iff definition of [[ E](A AB)JI ______
(o,i,j?E (I[PO(X)]I y [[ElAJI `jI[?BJj)
iff definition (4.6) of [[ ?B ? PO(?JI
((3,i,j?E(I[E]B ?Po(X)JjyI[?ATh
Logic for Constrained Proof Outlines
Q.E.D.
Our goal is to prove that a program ? satisfies a property PO(? under an environment ?A:
?, E]A, PO(?? E ESat
(4.7)
Using Property Reduction (2.4), we see that to prove (4.7), it suffices to be able to prove that X
satisfies property ?A ? PO(X).
(? ?A, PO(??E ESat
iff Property Reduction (2.4)
(? PO(? Q) ?A?E Sat
iff definition (2.1)
?
iff [[F?)G ?=[[F J]?[[ G ? and definition (4.6) of EJA ?
I[XJIa?[[?A ?PO(X)?
iff definition (2.1)
(? DA ? PO(X)?E Sat
The deductive system of Appendix A enables us to prove that (?, ?`) E Sat holds for ? an ordi-
nary proof outline. Extensions are needed for the case where ? is a constrained proof outline. We
now give these; a soundness and completeness proof for them appears in Appendix B.
For reasoning about assignment statements executed under an environment E]A, we can assume
that A holds before execution and, because the environment precludes transition to a state satisfying
?A, any postcondition asserting ?A can be strengthened.
-16-
cristrAssig:			ipAA)?[x:=E](qv?AJ
5A?(p) ?[x:=E] (q)
Sequential composition under an environment ElA allows a weaker postcondition for the first
statement, since the environment ensures that A will hold.
Cnstr-SeqComp:			?A ? PO(X1), ElA ?
(A Apost(?1)) ?pre(?2)
E]A ? (pre(?1)J ?: [PO(?1); PO(?)] (post(?))
Parallel composition under an environment E]A also allows weaker assertions. A can be
assumed in the preconditions of the interference-freedom proofs.
Cnstr-ParComp: E]A ? PO(?1), ?A H
E]A ? PO(?1) and [ZA ? PO(?2) are interference free
H (pre(?1) ?pre(X2)J ?: [PO(?1) 1/ PO(?2)] (post(?1) Apost(?2)1
We establish that E]A ? PO(X1) and ?A ? PO(?) are interference free in much the same way as
for ordinary proof oudines.
For all			E Assig(?1), where ?a is the assignment ??: [x
E]A ? (at(?a)AIpo?? A40?)) ??: [x :=E] (jpo?x??)
For all ?? E Assig(?), where ?a is the assignment ?a: [x			El:
? (at(X?)?4o??? A40?)) ??: [x :=E] (4o(?)J
As with ordinary proof oudines, two rules allow us to modify assertions based on deductions
possible in the assertion language. For a constrained proof oufline ZA ? PO(?, we can assume A
in making those deductions.
Cnstr-Conseq:
Cnstr-Equiv:
ZAHPO(?, (p?A)?pre(?, (post(??A)?q
ZA ? ip) PO(? (q)
ZA?PO(?, A?(!Po?=4o'?))PO'(X)isself consistent
ZA H PO%)
Example Revisited
We illustrate the deductive system for constrained proof outlines by proving that y =3 holds
upon termination, when the program of Figure 4.1 is executed by a single processor using a fixed-
priority scheduler with process ?i having higher priority than ?.
Recall that a fixed-priority scheduler rules out allocating a processor to any but the highest-
priority processes, where a fixed priority value v7t is associated with each process it. The formulation
of this restriction using the assertion language of our Proof Outline Logic closely parallels our TLA
-17-
formulationin3.3.
As before, forN the number of processors, we define:
Alloc(N): (#?E 11: acn.ve?)<?N
Run(it): active? ? itE TOP(N, fi)
`fliese state that variable active is true for the N highest ranked different processes ?. To stipulate
that active? be true in order for a process to execute an atomic action, let Lab(??) be the set of labels
for process Ic. Execution of an atomic action from it causes control variables to change for some
E
Pgrs(n:): (?true A			V			(at(?)?O-at(A!))) ? eacn.ve?
?E LAb(?,?)
The rank rnnk? of a process depends on whether or not that process has terminated. Since we assume
that process it has label ?, that process has not terminated if in(?) is true, We thus can assign
values to rnnk? using v7t as follows,
Pn'o(it): (in(?) ? (rnnk7t=v7t)) A (?in(?) => (rank7t =0))
Combining these, we obtain an asseflion FixedPrio which characterizes a fixed-priority scheduler.
FbcedPrio: Alloc(N) A (VitE fi: Run(it) A Pgrs(it) A Prio(it))
To conclude that y =3 holds upon termination of program ? in Figure 4.1, we prove
?FixedPn'o ? PO(X) a theorem, wherepost(? ?y=3 We assume N= 1, v? =2, and v? = 1.
Using Assig2 (of Appendix A), we get:
(at(X2)) ??1: [y =1] (at(?2))
(at(?)) ?12: [y =2] (at(?))
(4.8)
(4.9)
With Conseq (of Appendix A), we can strengthen the precondition of (4.8) and (4,9) as well as weak-
ening the postconditions of both--Hin preparation for using Cnstr-Assig with E]FixedPrio
(at(?)?Fuc'edPn'o) ???: [y:= 11 (at(?)v?FixedPn'o)			(4.10)
(at(X2) A FbcedPrio) ?i2 [Y:=2j (true V ?FixedPn'o)			(4.11)
Using Cnstr-Assig we now obtain:
?FixedPn'o ? (at(X2)) ???: \y := 1] (at(?2))			(4.12)
E]FixedPrio ? (at(?2)) X12: [y := 2] (true)			(4.13)
We combine these, using Cnstr-SeqComp to obtain a constrained proof outline for process X1.
X11: [y =1] (at(X?))			414
?i2 [Y =2] (true))
EIFixedPrio ?
X1: [ (at(?2))
(at(?2) 1
(true)
A proof oufline for process X2 is constructed by starting with Assigl (of Appendix A).
(3=3) X2: [y:=3) (y=3)			(4.15)
In preparation for using Cnstr-Assig, the precondition is strengthened and postcondition is weakened.
-18-
(true A FixedPrio) X2: ty:=3j (y=3 v ?FtxedPno)
We now can use Cnstr-Assig to obtain a constrained proof oufline for process X2
EIFixedPrio ? (true) ?2 [Y:=3j (y=3)
Finally, we use Cnstr-ParComp to combine (4.14) and (4.17):
5FtxedPno ?
?: [(at(??))
??: [ (at(?2)) ???: [y := 1] (at(X2))
(at(?)) ??:ty:=2] (true)]
(true)
1/
(true) X2: ?y:=3] (y=3)]
This requires that we discharge the following interference-freedom requirements:
E]FixedPrio ? (at(?1i) AlPo(?) ?jpo???) ??: [y := 1] (i#o?))
?FixedPno ? (at(?12) ATho?) AIPo?)) ?i2 [Y:=2] (Tho???))
E]FixedPrio ? (at(X2) A 40Q) A Tho?)) ?: [y := 3] (4oQ))
where:
4oQ)
A
A
(at(X1) => at(?2)) A (4ter(?1) => true)
(at(X11) ? at(X2)) A (after(?11) => at(X2))
(at(X12) ? at(X2)) A (afler(X12) ? true)
(4.16)
(4.17)
(4.18)
(4.19)
(4.20)
(4.21)
4o??: (at(X2) => true) A (after(X2) ?y =3)
4O?i) and 1PO???) can be simplified, using ordinary Predicate Logic, resulting in:
Ipo?) (at(?i) v at(?11) v after(?11) v at(?i?)) ? at(X?)
jro??: after(?)?y=3
To prove formula (4.19), observe that according to the definitions of 4o?) Tho???) and Fix-
edPrio:
(at(?ii) A 1PO?1) A 1PO(??) A FixedPrio) ?
at(X2) ? (4o(?) v FixedPrio)
Applying Conseq and then Cnstr-Assig to (4.8) we obtain (4.19). The proof of (4.20) is virtually
identical.
Proving formula (4.21) illustrates the role of environment E]FixedPrio. Using Assig3, Equiv,
and Conseq it is not difficult to prove:
(at(?2)) ?2 [y =3] (Q: O-at(X2) A mat(?2) A at(?1)=O-at(?1) A (in(?1) v after(?))
(in(?1) => (acnve? A ?active?)) ?2 [y :3] (R: O-(in(?j) ? (active? A ?aaive?)))
Each of these preconditions is implied by at(?) A 1PO?) A 40Q) A FixedPrio, so we can use
-19-
Conseq to strengthen each and deduce:
(at(?)AIpo?? A4o?) ?FixeaPno) ?: [y =3] (Qi
(at(X?)ALpo?? AIFo?) ?FixeaPnoJ X2: [y:=3] fRi
Therefore, by Conj, we obtain:
A 4o?) A 1P0?) A FixedPrio) ?: [y:= 3] fQ AR)
We now use Conseq to infer that 40?i) or FixedPrio holds whenever Q A R does by proving:
(in(?1) A Q AR) ? ?FixedPno
(after(?) A Q AR) ? i#o?)
Using these with Conseq, we conclude:
fat(?) A 4o?) A 4oQ) A FixedPrio) X2: [y =3] f40?i) V ?FixedPno 1
Cnstr-Assig now allows us to conclude (4.21), as is desired.
4.3. An Even Older Recipe
The notion of a constrained proof outline is not new. In [LS85] a similar idea was discussed in
connection with reasoning about aliasing and other artifacts of variable declarations. The aliasing of
two variables imposes the constraint that their values are equal; the declaration of a variable imposes
a constraint on the values that variable may store. Constrained proof outlines, because they provide a
basis for proving properties of programs whose execution depends on constraints being preserved, are
thus a way to reason about aliasing and declarations. An even earlier call for a construct like our con-
strained proof outlines appears in [L8O]. There, Lamport claims that such proof outlines would be
helpful in proving certain types of safety properties of concurrent programs.
5. Discussion
Related Work
Our work is perhaps closest in spirit to the various approaches for reasoning about open sys-
tems. An open system is one that interacts with its environment through shared memory or communi-
cation. The execution of such a system is commonly modeled as an interleaving of steps by the sys-
tem and steps by the environment. Since an open system is not expected to function properly in an
arbitrary environment, its specification typically will contain explicit assumptions about the environ-
ment. Such specifications are called assume-guarantee specifications because they guarantee
behavior when the environment satisfies some assumptions. Logics for verifying safety properties of
assume-guarantee specifications are discussed in [FFG92j, [J83J, and [MC8l]; liveness properties are
treated in [AL9l], [BKP84], and [P85]; and model-checking techniques based on assume-guarantee
specifications are introduced in [CLM89] and [GL9 1].
Our approach differs from this open systems work both in the role played by the environment
and in how state changes are made by the environment. We use the environment to represent aspects
of the computation model, not as an abstraction of the behaviors for other agents that will run con-
currently with the system. Second, in our approach, every state change obeys constraints defined by
the environment. State changes attributed to the environment are not interleaved with system actions,
as is the case with the open systems view.
-20-
Our view of the environment and the view employed for open systems are complementary.
They address different problems. Both notions of environment can coexist in a single logic. Open
systems and their notion of an environment are an accepted part of the verification scene. This paper
explores the use of a new type of environment. Our environments allow logics to be extended for
various computational models. As a result, a single principle suffices for reasoning about the effects
of schedulers, real-time models, resource constraints, and fairness assumptions. Thus, one does not
have to redesign a programming logic every time the computational model is changed.
In terms of program construction, our notion of an environment is closely related to superposi-
tion [K87j [BF88] [CM88j. The superposition of two programs 5 and T is a single program, each of
whose steps comprises a step of 5 and a step of T performed simultaneously. Thus, in terms of TLA,
the superposition of two actions is simply their conjunction. Our work extends the domain of appli-
cability for superposition by allowing one component of a superposition to characterize aspects of a
computational model.
Redefining Feasible Behaviors
The definition of 2 for the feasible behaviors of a program 5 under an environment E is not the
only plausible one. Every infeasible behavior of 5 ruled out by E has a maximal finite prefix (possi-
bly empty) that agrees with a prefix of some behavior in E. Such a prefix can be regarded as model-
ing an execution of 5 that aborts due to the constraints of E, and this prefix might well be included in
the set of feasible behaviors.
For example, consider executing the program
T: x:=O; do i:=ltoS: x:=x+1 od
in an environment that constrains x to be between 0 and 3 (i.e., x is represented using 2 bits). The
alternative definition of feasible behaviors would include prefixes of behaviors of T up until the point
where an attempt is made to store 4 into x. Using the definition of 2, the set of feasible behaviors
would be empty.
The alternative definition of feasible behaviors for a program 5 under an environment E,
(j[5 JI?[[E]I) ? (prefix([[5 ?) nprefix([[E ?)),
(5.1)
admits reasoning about feasible, but incomplete, executions of a program under a given environment.
Unfortunately, we have been unable to identify reduction principles for definition (5.1). It remains an
open question how to extend a logic for Sat into a logic for ESat given this definition.
6. Conclusion
In this paper, we have shown that environments are a powerful device for making aspects of a
computational model explicit in a programming logic. We have shown how environments can be
used to formalize schedulers and real-time; a forthcoming paper will show how they can be applied to
hybrid systems, where a continuous transition system governs changes to certain variables.
We have given two semantic principles, program reduction and property reduction, for extend-
ing programming logics to enable reasoning about program executions feasible under a specified
environment. Having such principles means that a new logic need not be designed every time the
computational model served by an extant logic is changed. For example, in this paper, we give a new
way to reason about real4ime in TLA and in Hoare-style programming logics. We also derive the
-21-
first Hoare-style logic for reasoning about schedulers.
The basic idea of reasoning about program executions that are feasible in some environment is
not new, having enjoyed widespread use in connection with open systems. The basic idea of aug-
menting the individual state transitions caused by the atomic actions in a program is not new, either.
It underlies methods for program composition by superposition, methods for reasoning about aliasing,
and proposals for verifying certain types of safety properties. What is new is our use of environments
for describing aspects of a computational model and our unifying semantic principles for reasoning
about environments. Extensions to a computational model can now be translated into extensions to
an existing programming logic, by applying one of two simple semantic principles.
Acknowledgments
We are grateful to Leslie Lamport and Jay Misra for discussions and helpful comments on this material.
References
[AL9l]
[BMS93]
[BKP84]
[BF88j
[CM88]
[CLM89]
[EH86]
[FFG92]
[GL91]
[H69]
[J83j
[K87]
[L80]
[L91]
[LS84j
[LS85j
[LJJ93]
[MP89]
Abadi, M. and L. Lamport. An old-fashioned recipe for real-time. Real-nme: Theory in Practice, J.W.
de Bakker and W.-P. de Roever and G. Rozenberg eds., Lecture Notes in Computer Science Vol. 600,
Springer-Verlag, New York, 1989, 1-27.
Babaoglu, 0, K. Marzullo, and F.B. Schneider. A formalization of priority inversion. Real-Time Systems
5 (1993), 285-303.
Barringer, H., R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. Proceed-
ings 16th Annual ACM Symposium on Theory ofComputing (Washington, D.C., April 1984), 51-63.
Francez, N. and L. Bouge. A Compositional Approach to Superimposition. Proceedings 15th ACM
Symp. on Principles ofprogramming Languages (San Diego, Ca, Jan. 1988), 240-249.
Chandy, M. and J. Misra. Parallelprogram design. Addison-Wesley, 1988.
Clarke, E.M., D.E. Long, and K.L. McMillan. Compositional model checking. Proceedings 4th IEEE
Symposium on Logic in Computer Science (Palo Alto, CA. June 1989), 353-362.
Emerson, E.A and J.Y. Halpem. Sometimes and Not Never Revisited: Cn Branching Versus Linear
Time. JournaloftheACM33, 1(1986), 151-178.
Fix, L., N. Francez, and 0. Grumherg. Program composition via unification. Automata, Languages and
Programming, Lecture Notes in Computer Science VoL 623, Springer-Verlag, New York, 1989, 672-684,
Grumberg, 0. and D.E. Long. Model checking and modular verification. CoNCUR'91, 2nd Interna-
tional Co#erence on Concurrency Theory, Lecture Notes in Computer Science Vol. 527, Springer-
Verlag, New York, 1991, 250-265.
Hoare, C.A.R. An axiomatic basis for computer programming. Communications ofthe ACM 12, 10 (Oct.
1969), 576-580.
Jones, C.B. Specification and design of (parallel) programs. Information Processing `83, R.E.A. Mason
ed., Elsevier Science Publishers, North Holland, The Netherlands, 321-332.
Katx, 5. A Superimposition Control Construct for Distributed Systems. MCC Technical Report STP-
268-87, 1987.
Lampor? L. The "Hoare Logic" of concurrent programs. Acta Informatica 14 (1980), 21-37.
Lamport, L. The temporal logic of actions. Technical report 79, Systems Research Center, Digital
Equipment Corp. Palo Alto, CA. Dec, 1991.
Lamport, L. and F.B. Schneider. The "Hoare Logic" of CSP and all that. ACM TOPIAS 6, 2 (April
1984), 281-296.
Lamport, L. and F.B. Schneider. Constraints: A uniform approach to aliasing and typing. Conference
Record of Twelfth Annual ACM Symposium on Principles of Programming Languages (New Orleans,
Louisiana, Jan. 1986), 205-216.
Liu, Z., M. Joseph, and T. Janowski. Specifying schedulability for real-time programs. Technical report,
Department of Computer Science, University of Warwick, Coventry, United Kingdom.
Manna, Z and A. Pnueli. The anchored version of the temporal framework. Linear time, branching time
and partial order in Logics and models for concurrency, J.W. de Bal:ker and W.-P. de Roever and G.
Rozenberg eds., Lecture Notes in Computer Science Vol. 354, Springer-Verlag, New York, 1989, 201-
284.
-22-
[MC8lj
[OG76j
[P85j
[S94j
[SRL9O]
Misra, I. and M. Chandy. Proofs of networks of processes. IFEE Transactions on Software Engineering,
SE-l 4 (July 1981), 417A26.
Owicki, 5. and D Gries. An axiomatic proof technique for parallel programs. Acta Informatica 6 (1976),
319-340.
Pnueli, A. In transition from global to modular temporal reasoning about programs. Logics and models
ofconcurrent systems, K.R. Apt e&, NATO ASI Series, Vol. F13, Springer-Veilag. 1985, 123-144.
Schneider, F.B. On concurrentprogrannring. To appear.
Sha, L, R. Rajkumar, and I. Lehoczky. Priority inheritance protocols: An approach to real-time syn-
chronization. JEEE Transactions on Coniputers C-39, 1175-1185.
-23-
Appendix A: A Logic of Proof Outlines
The deductive system for reasoning about assenions includes the axioms and inference rules of
first-order predicate logic. It also axiomatizes theories for the datatypes of program variables and
expressions. Perhaps the only aspect of this axiomatization that might be unfamiliar concerns e. It
will include axioms like:
e?e ?			??) = ?eT10
In order to reason about control variables in program states, each program X gives rise to a set of
axioms. These axioms characterize the constraints of Figure 4.2. For every label ? E Lab(?):
CPO; in(??c?fter(?
CP1: (at(?) A after(X'))
CP2: at(X') ?
cP3: If ? labels [x := Ej: at(?)=in(?)
cP4: If?'labels [X1: [S]; ?2:[T]]:
(a) at(X')=at(?1)
(b) at(X2)=aftu(?1)
(c) after(X')=after(X2)
(d) in(X')=((in(X1) A in(X2)) v (? in(X1) A
(e) (in(?1) v in(?2)) => in(X')
CP5:
If?'labels [??: [Sill ?2:[TJ]:
(a) at(X')=(at(?1) A at(?2))
(b) after(?)=(after(?j) A after(?))
(d) in(?)=((in(X1) v after(?j)) A (in(X2) v after(?2)) A (after(X1) A after(?2)))
(d) (in(?1) v in(X2)) ?
For reasoning about proof outlines, we have the following. First, here are the axioms for
assignment statements.
Assigl:
Assig2:
If no free variable in p is a control variable and pXE denotes the predicate logic
formula that results from replacing every free occurrence of x in p that is not in
the scope of 0- withE:
(PEX) X:[x:=E] fp)
If ? is a label from a program that is parallel to that containing X, and cp (?)
denotes any of the control variables at(X'), after(X'), in(?) or their negations:
(cp(X')) X: [x :=EJ (cp(?))
Assig3: fpj ? [x :=Ei fOp)
Sequential composition is handled by a single inference rule.
-24-
SeqComp:
PO(?1), PO(?),
post(?i) =>pre(?2)
(pre(?1)J ?: [PO(?); PO(?)] (post(X2))
The parallel composition rule is based on the formulation of interference freedom [OG76] of proof
outlines given in [LS84]. Two proof outlines PO(?1) and PO(?) are inteiferencefree iff
For all ?? E Assig(?1), where ?? is the assignment ??: [x Ej:
(at(??)?Ipo??AIpo??) ?a: [x:=E] (4o?))
For all ?? E Assig(?), where ?? is the assignment Xa: [x Ej:
(at(Xa) A4o(?) AIPo?)) Xa: [x :=Ej (Tho?))
Parcomp:
PO(?1), PO(?),
PO(X1) and PO(X2) are interference free
(pre(?j) ?pre(?2)) X: [PO(X1) 1/ PO(X2)j (post(?j) ?post(X2))
Finally, three rules allow us to modify asseflions based on the deductive system for the asser-
tion language. Recall, (p) PO(? (q 1 denotes a proof outline that is identical to PO(? but with p
replacing pre(X) and q replacing post(X).
Conj:			(pil X:[x:=E] (q1)
fP2J ?[x:=Ej fq2)
(pjAp?) ?[x:=E] fq1?q2J
Conseq: PO(?,p?pre(?,post(X) ? q
(pi PO(X) (qJ
Equiv:
PO(X),4o?)=4o'??4o'?self consistent
Appendix B: Soundness and Completeness for Constrained Proof Outlines
We now prove soundness and relative completeness for the Logic of Constrained Proof Outlines
given in section 4.2. Specifically, we prove that Cnstr-Assig, Cnstr-SeqComp, Const-ParComp and
Cnstr-Equiv are sound. We also prove that Cnstr-Assig, Cnstr-SeqComp and Const-ParComp
comprise a complete deductive system relative to the deductive system of Appendix A for ordinary
proof outlines. (Cnstr-Conseq and Cnstr-Equiv of section 4.2 are not necessary for completeness.)
-25-
Lemma (Soundness of Cnstr-Assig): The rule
Cnstr-Assig:			A A)?[x:= Ej(qv ?A 1
EIA?(p) ?[x:=E] (q)
is sound.
Proof. Assume that
?a, i,])EI[?Jj holds,
5A?(p) ?[x:=E]
hypothesis (p AA) ?: [x :=Ej fq v?A) is valid. We show that if
then (o,i,j)EI[E]A?(p) ?[x:=Ej (q)? holds, and thus that
(qJ is valid.
If (pA A) ? [x E] (q v ?A) is valid then, by deimition, I[??a?I[PO(? ? holds, where
PO(? is (PA A) ? [x :=E] (q v ?A). This implies that for any (a, i,j)E I[?JI one ofthe follow-
ing must hold:
a[..i]?4o?
ForaIlk, i<?k<j: a[..kjk!p0?
where 4o?: (at(X)?p AA) A (after(??q v?,A)
We consider two cases.
Case 1: Assume (a,i,j)?[[E]A?.
[[E]A?(P) ?[x:=EJ (q)Th
Case 2: Assume (a, i, j)E If ?A ?. According to the definition of [[ElA JI:
Forallk, i<?k<j: a[..k]kA
It suffices to prove that
(a,i,j)cIf[ZiA?(p) X:[x:=E] (q)JI.
Case 2.1: Assume (B.l.l) holds. Thus
a[..i]? ((at(X) A (?? v?A)) v (after(X) A (?q A A)))
holds. Conjoining (B.1.3), we conclude
(B.1.1)
(B.1.2)
According to definition (4.6), (a, i, I) is in
(B. 1.3)
if (B.l.l) holds or (B.l.2) holds, then
a[..t]? ((at(? A ?p) v (after(? A
which implies a[..i]?(at(X)?p) A (aftu(X)?q). Because (P) X: [x :=Ej (q) is self
consistent, by definition (4.4) we have that (a, t, j)E If (p) X: [x := E] fq) Ii holds. Hence,
by definition (4.6) of the propefly defined by a constrained proof outline,
(a,i,i?If?A? (PJ ?[x:=E] fq)JIholds.
Case 2.2: Assume (B.l.2) holds. Conjoining (B.l.3), we conclude
For all k, i<?k<j: a[..k]k ((at(X)?p) A (afler(??q)).
self consistent,
holds,			so
(q 1 ? holds as well.
by definition (4.4) we have that
by			definition			(4.6)
EJ
Because fPJ X: [x :=E] (q) is
(a,i,j)?If(p) ?[x:=E] (q)?
(a,i,j?IfE)A?(P) ?[x:=E]
-26-
Lemma (Soundness of Cnstr-SeqComp): The rule
Cnstr-SeqComp:			E]A ? PO(X1), [ZIA H
(A Apost(?j)) ?pre(?2)
E]A ? (pre(?1)) ?: [PO(?1); PO(X2)j (post(?2))
is sound.
Proof. Assume that the hypotheses are valid. Therefore, we have that PO (?i) is self consistent,
PO(?) is self consistent, and:
[[? JI a (I[PO(?)Jj?[[?A JI)
JI a--H (I[PO(X2)Ji?[[?A ?
(B.2.l)
(B.2.2)
(B.2.3)
(A Apost(?1)) ?pre(?2)
To establish validity of the rule's conclusion, we must prove that I[ ? 1] a I[ ?A H PO(X) ?, where
PO(?) is (pre(Xi)) ?:[PO(?1); PO(X2)] (post(?2)). We do this by proving (o, i, j)E I[?? implies
??, i, j)E I[PO(X) ??[[ [ZIA ji), where, according to definition (4.3) of 4o?? we have:
I???: 4o?) A 4o?) A (at(? ?pre(?j)) A (after(? ?post(?))
Let ?o, i, j)E [[? ? hold. We consider two cases.
Case 1: Assume ??, i, j?E ? EJA JI. According to definition (4.6) of a constrained proof outline,
?o, i,j?t[EJA ?PO(X)JI holds.
Case 2: Assume (o, i, j?E [[EJA ji. In order to conclude (? i, j)E [[EJA H PO(X) ? holds, we must
show that ??, i, j)E [[PO(? JI holds. According to the definition of sequential composition
I[ ?: [??; ?2i JI, there are three cases:
(2.1)			Forallk, i<k<?j: ?[k]?qn(?)vaftu(?2))			and			(a,i,j??[[?JI.
(2.2)			Forallk, i<?k<j: ?k]??n(?1)vaflu(?))			and			(o,i,j?EIf?iI.
(2.3)			Exists n, i<?n<j:
(?i,n)E[[?]j and
(?n,j')E[[X2? and
?[n]k(after(?1) A at(?)) and
for all k, l<k<n: ?[k]??n(?2) v after(?2)) and
for all k, n <k<?i: o[k]?(in(X1) v aftu(?1))
Case2.1: Assume that forallk, i<?k<?j: ?[k]t#(in(X2)vaftu(?2)) and (?,i,j?E [[X1JI
hold. According to (B.2.l), (? i, j)E ([[PO(X1) ?u[[ EJAjI). Given assumption (of Case 2)
(a, i,j? ([EJA ?, we conclude (a, i,j? ([PO(?1)JI. Thus, by definition (4.4) of [[PO(M)]1,
we have that either a[..i1\fr40?? or else for all k, i<?k<j: a[..k1kIp0??. Since
at(?1)=at(? due to Control Predicate Axiom CP4(a) of Appendix A and pre(? is pre(?j),
we conclude that either
A (at(?)?pre(?1))) or else
(B.2.5)
-27-
forall k, i<?k<j: ?[..k]k40?) A
(B.2.6)
From assumption (of Case 2.1) for all k, i<k<?j: o[k]?(tn(?) v after(?)), we con-
clude that for all k, i<?k<?j: a[..ki?40??. And, because after(?)=after(? due to Control
Predicate			Axiom			CP4(c)			of			Appendix			A,			we			have
for all k, i <k <?j: a[..k]?(4o?? A (after(? ?post(?))). Conjoining this with (B.2.5) and
(B.2.6) we get that either ?[..i]?j?0? or else for all k, i<k<?j: ?[..k]?Ip0? holds. Since
PO(? is self consistent (because (A Apost(Xi)) ?pre(X2) and both PO(X1) and PO(?)
are self consistent), we have (a, i, j?E t[ PO(X) ?. Thus, by definition (4.6) we conclude that
(a,i,j)?![[Z1A ?PO(X)?.
Case 2.2: Assume for all k, i<?k<j: a[k]?(in(?1)v after(?1)) and (a, i,]?E [[? JI hold.
According to (B.2.2), (a, i, j?E ([[PO(?) Jlu[[ [ZiA JI). Given assumption (of Case 2)
(a, i, j')E [[ DA ?, we conclude (a, i, j? I[ PO(X2)]1. Thus, by definition (4.4) of [[PO(X2) ?,
we have that either a[..i]?jpo?? or else 1orallk,i<?k<?j: a[..k]kIp0??. Since
after(X2)=*er(? due to Control Predicate Axiom CP4(c) of Appendix A, we conclude that
either
a[..ii?(ipo?? A (afler(X) ?post(X2))) or else
for all k, i<k<?j: a[..k?kjpo?? A (after(? ?post(X2)).
(B.2.7)
(B.2.8)
From assumption (of Case 2.2) for all k, i<?k<?j: a[k]?(in(X1) v ?ter(?1)) we con-
clude that for all k, i<k<?j: a[..k]?!po??. And, because at(X1)=at(X) due to Control
Predicate			Axiom			CP4(a)			of			Appendix			A,			we			have
for all k, i<k<?j: a[..k]k(Ip0?? A (at(??pre(?1))). Conjoining this with (B.2.7) and
(B.2.8) we get a[..iJ?4o?? or else for all k, i?<k<j: a[..kJ?40?? holds. Since PO(X) is
self consistent (because (A A post(X1)) ? pre(X2) and both PO(?1) and PO(X2) are self
consistent), we have (a, i, j')E [tPO(X) ?. Thus, by definition (4.6) we conclude that
(a, i,j?[[[Z1A ?PO(??.
Case 2.3: Assume that there exists n, i <? <I, such that:
(a, i, fl?E I[??
(a,n,j?? [[X2j1
a[n]k(after(?1) A
forallk, l<?k<n: a[k]?(in(?)vafter(X2))
for all k, n <k<i: a[k]?(in(?1) v after(X1))
(B.2.9)
(B.2.lO)
(B.2.l 1)
(B.2.12)
(B.2.13)
If a[..i]?Ip0? then, by definition, (a, i, j? [[PO(X) ?. By definition (4.6), we con-
clude that (a, i, j? If ?A ? PO(X) JI.
Now suppose a[..i]kIp0? holds.
First observe that due to Control Predicate Axiom CP4(a) and CP4(c) of
Appendix A we have at(?=at(?1) and after(X)=after(?). Therefore, choosing
pre(?1) lorpre(X) and choosingpost(X2) 1orpost(? we have:
-28-
!eoQ) = (4o?) A (at(? =>pre(?1))
1PO(??) = (!?o?) A (after(X) ?post(?))
(B.2. 14)
(B.2.15)
Because Tho? implies Jeo?) (3[..i]?jpo?) holds. From (B.2.9) and (B.2.l)
we have ((3,i, n? [[?A ? PO(X1 ) JI. Given the assumption (of Case 2) that
((3,i, j? [[E]A JI we conclude that ((3, i, n)e I[PO(X1) 1].
From ((3, I, fl)E [[PO(?1) JI and assumption (above) (3[..iikJpoQ) we have:
For all k, i<k<?n: (3[..k]kIp0Q)
By narrowing the range, we get:
For all k, i<k <n: a[..k]kIp0Q)
And, from (B.2.14) we get
Forallk,i<?k<n: (3[..k?k1p0?) ?(at(??pre(Xj))
(B.2.l6)
According to (B.2.12), 4o?) is trivially true in states a[..k] where i<k <n. More-
over, from (B.2. 15), 1PO?) A (after(X) ?post(?2)) is also true in those states:
Forallk, i<k<n: (3[..k]??po?? ?(at(X)?pre(?1)) A
4o?) A (after(?) =>post(?2)))
Equivalently, we have for all k, i<k <n: (3[..kJ?40?.
From (B.2.16), again by narrowing the range, we conclude o[..n]?IPo?). By
definition, Jpo?) implies after(X1) ?post(?j), so by conjoining (B.2.ll), we infer
(3[..fl]?jpo(?) A after(X1) ?pa?t(X1) A at(X2)
And, because of the assumption (Case 2) that ((3,i, j? [fElA ?, we have (3[..n]kA.
Thus we conclude:
A 4O(?i) A after(?1) Apost(Xj) A
Using (B.2.3) we get:
(3[..fl]k40?) A after(Xj) Apost(X1) A at(X2) ?pre(X2)
PO(X2) is self consistent, so at(?2) A pre(?2) implies 4o?) and we have:
(3?..n]?jpoQ) A 1PO(?)
Using (B.2.14) and (B.2.15), we get
(3[..n]kIp0? A (at(X)?pre(X1)) A40(?) A (after(X)?post(X2)))
or equivalently (3[..fl]k40(?.
From (B.2.lO) and (B.2.l) we have ((3,n,j)E[[E]A ?PO(X2)?. Given the
assumption (of Case 2) that ((3,i, j)E [f?A JI we conclude that
((3,n, i? [fPO(X2) ?.
From ((3, n, j)E [fPO(?) ji and (3[..n]?40? we have:
-29-
For all k, n<?k<?j: Ot..k1k40???)
And, from (B.2.15) we get
For all k, n<?k<j: a[..k]?4o???? A (after(??post(?))
According to (`3.2.13), 1PO?) is trivially true in traces o[..k] where n<?k<?f More-
over, from (`3.2.14), 4O?i) A (at(X) ?pre(?1)) is also true in those traces:
For all k, n?<k<?j: O[..k]k(40?) A (at(X)?pre(X1)) A
4o?) A (after(X) ?post(?2))),
orequivalently for all k, n<?k<j: ?[..k]kIp0?.
Having			proved			fbrallk,i<?k<n: ?[..k]k40?			and
for all k, n<k<?j: o[..k]?40? we conclude forall k, i<?k<?j; ?[..k]?40?. This
means that (? i, j? [[5A H PO(? ? holds.			5
-30-
Lemma (Soundness of Cnstr-ParComp): The rule
E]A ?PO(?), [ZIA ?PO(?),
? PO(?1) and ElA ? PO(?) are interference free
E]A ? (pre(?1) ?pre(?)) X: [PO(?1) II PO(?)] (post(?j) Apost(X2))
is sound.
Proof. Assume that the three hypotheses are valid.
sistent, PO(?) is self consistent, and:
ii ?(I[PO(?)]]?[[5A ii)
[[?JI a([[PO(?)?uI[?AJI)
Therefore, we have that PO (X1) is self con-
For all ?? E Assig(X1), where ?? is the assignment ?a: [x Ej:
c: ([[ (at(??) A 4o?) A 4o?)) ??: [x :=E] (i#o?) 1 JI?[[ ElA Ji)
For all ?? E Assig(X2), where ?a is the assignment X?: [x := Ej:
I[ ??]] a (I[ (at(X?) A 1PO?) A 1PO(??)) ??: [x := E] (!#o(?)) j]?[[ EJA JI)
(B.3.l)
(B.3.2)
(B.3.3)
(B.3.4)
To establish validity of the rule's conclusion, we must prove that If a If [ZIA ? PO(X) ii, where
PO(?) is fpre(X1) ?pre(?2)) ?: [PO(?1) II PO(?2)] fpost(X1) Apost(?2)). We do this by prov-
ing ?o, i, ]?E If ? JI implies ?(3, i, j)E If PO(X) JJ?If E]A ?).
Let (? t, j? IfXJl hold.
Case 1: Assume (o, i, j?E If E]A ?. According to definition (4.6) of a constrained proof outline,
(a, i,j?If E]A ?PO(?Jj holds.
Case 2: Assume (a, i, j')E If ElA Ji. In order to conclude (0, i, j?E If E]A H PO(X) ii holds, we must
show that (a, i, j')E If PO(? JJ holds. We consider two cases.
Case 2.1: Assume a[..i]?4o??. According to definition (4.4) of the property defined by
we conclude (0, t, j?E If PO(? JI holds.
Case 2.2: Assume a[. .i]?1po? We prove
For all k, i<?k<j: a[..k]?jp0?
by induction. This establishes that (a, i, j?E If PO(? Ji holds, due to definition (4.4) of the
property defined by PO(X).
For the induction hypothesis we use
i<?h
A (h<j ? tbrallk,i<?k<--Hh: 0[..k?k4o(x))
Base Case: Prove P(i). P(i) holds because it is implied by the assumption of (this) Case
2.2.
Induction Case: Prove P(h) ?P(h+l). We assume that P(h) holds and prove P(h+l). If
i<h then P(h+l) is trivially valid, so P(h)?P(h+l) is proved. We now consider the case
-31-
where h <I.
According to the definition (4.2) of [[?J], we have (a[h], a[h+li)ER?: [x :=E] for some
X'E (Assig(?1 )?Assig(X2)). Without loss of generality, suppose X'E Assig(X1) holds. Thus,
wehave(a,h,h+1)E[[?? and(a,h,h+l?I[? ?.
Given assumption (a, i, j)E [[ElA ? of (this) Case 2 and (B.3.l), we conclude
(a,h,h+l?([PO(?1)? holds. From assumptions P(h) and h<j we have a[..h??40?.
Thus, a[..h]kIpo?? because Ipo? implies 1PO?1) by definition:
4o?) A 1PO(??) A
(at(??(pre(?j) ?pre(?)) A
? (post(?1) A post(?))
definition
(B.3.5)
Since a[..h]k40?1?, according to (4.4) of [[PO(?1) Ji we have that
forall k, i<?k<j a[..k]?Ipo?? holds, because we know (a, t,]? I[PO(?1)?. And, since
i<h <j we conclude
a[..h+lJk40??.
Given (a, h, h + l? [[?]], we conclude from (B.3.3) that:
(a, h, h+1? (If fat(X') A 4o?) A 4o???) I ? f4o?)) j1?[[ E]A ?)
Thus, from the assumption (a, i, ]?E If E]A ji of (this) Case 2, we obtain:
(a,h,h+l?If (at(?) AIPoQ) AIPo?)) Y
From assumptions P(h) and h <I we have a[..hjk40? so, from (B.3.5), we conclude
(B.3.6)
(B.3.7)
a[..h]k40??1? A i;p??).			(B.3.8)
Using definition (4.4) of the property defined by a proof outiine, we conclude from
(B.3.7) that either a[..h]?Ip0?? or else
For all k, h<k<?h+1 a[..k]k40??			(B.3.9)
where
Ipo?) (at(?) ? (at(?) A 4o?) A 4o???))) A (afler(X') ? Tho?))
Definition (4.1) and (a[hj, a[h+11)ERy: [x E] implies a[h]kat(?). Conjoining
a[h]?at(Y) and (B.3.8) allows us to rule out a[..h]?40?? so (B.3.9) must hold.
From (a[h], a[h+l])?R? [x :=EJ and definition (4.1), we have a[h+ljkafter(?). We,
therefore, conclude from (B.3.9) that
a[..h+l]k4o??
(B.3.lO)
Finally, observe that, by construction, 4O?i) A 4o???) is equivalent to i?p0(X) defined
in (B.3.5). Thus, proving (B.3.6) and (B.3.lO?as we have suffices for proving
a[..h+ljkjp0?, and P(h+l) is proved.
-32-
Lemma (Soundness of Cnstr-Equiv): The rule
Cnstr-Equiv: ?A? PO(?, A?(4o?=4o'?)?PO'(X)isself consistent
? POTh)
is sound.
Proof. Assume that the three hypotheses are valid. We prove that the rule's conclusion is valid by
showing [[? ?c::I[ ElA ? PO'(? II.
Let (a, t,]?E [[?]i. From the validity of E]A ?PO(?, we have [[?JIa?[[EIA ?PO(X)JI. We
consider two cases.
Case 1: Assume (a, t, j?E [[ElA]'. According to definition (4.6) for the propefly defined by a con-
strained proof outline, we have (a, i, j?E [f E]A ? PO'(? ?.
Case 2: Assume (a, t, j? [[?A ?. This means
Forallk, i<?k?<j: a[..kj?A
(B.4.l)
Assuming (a, I, j?E [[ElA ji also implies (a, i, i?E [[PO(? JI, due to definition (4.6) of the propefly
defined by a constrained proof outline. From definition (4.4) of I[ PO(? JI we conclude a[..i]?40?
or else for all k, i?<k<?j: a[..k]?Tho??. By conjoining (B.4.l) with these, we infer
A 1po?) or else for all k, i<k<j: a[..k?k(A A
The second hypothesis of Cnstr-Equiv implies that A A 4o? equals A A 4o'? Thus, we con-
clude a[..t]?(A A40?) or else forallk, t<?ksj: a[..k]?(A A4o'?) must hold. Given (B.4.l), if
A 40Th)) holds then a[..ii?4om) must. And, in that case, (a, i, j? [[PO,(x) I' according
to definition (4.4) applied to [[PO,(x) ? because, by hypothesis, PO'(? is self consistent. In the case
where for all k, i<k<j: a[..k]k(A A 4o'?) holds, we conclude that for all k, i<?k?<j: a[,,kj?40'?
must hold, because (A A IPo'(?) ? 40Th) Again, (a, i, j?E [[PO'(X) ? according to definition (4.4)
applied to [[PO `(? ? because, by hypothesis, PO'(? is self consistent.
Having proved (a, i, ]?E [[PO,(x) j), we conclude (a, i, j?E [[?A ? PO,(x) ? based on
definition (4.6) for the propefly defined by a constrained proof outline.			E]
-33-
Lemma (Relative Completeness of Cnstr-Assig): The rule
Cnstr-Assig:			(pAA)?[x:=E]fqv?A)
EiA?fp) ?[x:=E] fq)
is relatively complete.
Proof. Assume that conclusion ?A ? (p) ?: [x E] (q) is valid. We show that hypothesis
ip AA) X: [x :=E] fq v?AJ is valid as well, by showing that if (a,t,j?[[?JI holds, then
(a,i,j?[[(pAAJ ?[x:=E] (qv?AJ?holds.
Let (a, i, j')E I[ X]i hold. We consider two cases.
Case 1: Assume (a, i, j? [[?A ii. According to the definition of [[?A ?:
Forallk, i<k<?j: a[..k]?A			(B.5. 1)
Using this and the assumption that ElA ? (pJ ?: [x E] fq 1 is valid, we conclude that
(a, i, ]?E [[PO(? JI and due to (4.4) one of the following holds:
a[..i]?40?			(B.5.2)
for all k, i<k<?j: a[..k]?40?			(B.5.3)
where 4o???: (at(X) ?p) A (after(? ?
It			suffices			to			prove			that			if			(B.5.2)			holds			or			(B.5.3)			holds,			then
(a,i,j)?i[(p?A) ?[x :=E] (qv?AJ?.
Case 1.1: Assume (B.5.2) holds. Thus, a[..tJ?((at(? ?p) A (after(X) ?q) holds. Given
(B.5.1), this implies a[..i]k((ar(? A (?p v ?A)) v (aftu(X) A (? q A A)) holds. This
means a[..i]?((at(X) ?p A A) A (after(X) ? q v ?A), holds so, by definition,
(a,i,j?I[(p?A) ?[x:=E] (qv?AJ]jholds.
Case 1.2: Assume (B.5.3) holds. Given (B.5. 1), this implies that
for all k, i<k<?j: a[..k]k ((at(X)?p AA) A (aftu(??q v?A))
holds. Thus, by definition, (a, i, j?E I[ (p A A) ? [x := E] (q v ?A) JI holds.
Case 2: Assume (a, I, j? t[ E]A ?. According to the definition of ? ?A ?:
Existsk, i<k<?j: a[..kJ??A
We consider three cases, according to the definition
ip AAJ ? [x :=E] (q v?A) is self consistent,
(a,i,j?[[(p?A) ?[x:=E] (qv?AJJIhdds.
(B.5.4)
of If XJl given in (4.2). Since
it suffices to prove that
Case 2.1: Assume j=i and a[..i]kat(? A ??after(?. By (B.5A),
a[..i]?(at(X)?p AA), so a[..i]?((at(??p ?A)?(aftu(X)?q v?A)).
definition, (a, i,j?[[ ip AA) X: [x :=E? (q v?A) ? holds.
we conclude
Thus, by
Case 2.2: Assume j=i and a[..i]k?at(? A after(?. By (B.5.4), we conclude
a[..i]k(after(??q v?A), so a[..i]k((at(??p ?A)?(after(??q v??A)). Since i=]
holds, so does
for all k, i<?k<j: a[..k]k((at(? ?p A A) A ((4tu(X) ? q v ?A)).
-34-
Thus, by definition, (a, i, ])E [t(p A A) ? [x := E] fq v ?A J JI holds.
Case 2.3: Assume j=i+l and a[..i]kat(? A ?after(?. If o[..i]k(?p v ?A) then
at. .i]?((at(? ?p AA) A (after(??q v?A))			and,			by			definition,
(a, t, j? [[(pA A) ? [x E] jq v ?A) JI holds. If, on the other hand, aLJlk(p A A),
then we conclude from ]=i+l and (B.5.4) that at.j]k(q v ?A) holds, so
for alt k, i<k<?j: at..k]?((at(X) ?p A A) A (after(X)? q v
alsoholds. Again,(a,t,j)?[[(p?A) ? [x:=E] (qv??A)JIholds.			E]
-35-
Lemma (Relative Completeness of Cnstr-SeqComp): Assume that all valid constrained proof out-
lines ?A* H PO*(?1) and ?A* ? PO*(X2) are provable, and assume that all valid predicate logic
formulas are provable. Then
E]A?fp) ?[PO(?);PO(?)] (q)
is provable if valid.
(B.6.l)
Proof. Assume (B.6.l) is valid. Let
? fI) X: [PO'(?1); PO'(?2)] (I)			(B.6.2)
be a proof outline for ?: [X1; ?] in which every asseflion in PO'(X1) and PO'(?) is
I: 4o?) A 1PO?) A (at(? ?p) A (after(? ?
Observe that (B.6.2) is valid by Cnstr-Equiv because the proof outline invariant for (B.6. 1) equals I
and (B.6.l) is valid.
We show below that
H U) PO'(X1) (I)
(B.6.3)
(B.6.4)
H (1) PO'(X1) (1)
are both valid. This implies that (B.6.3) and (B.6.4) are provable by the assumptions of this lemma.
By construction, post(X1) andpre(X2) in (B.6.2) are both 1,50 A ?post(X1)?pre(X2) is valid and,
by the lemma's assumption, provable. The three hypotheses needed for using Cnstr-SeqComp to
deduce (B.6.2) are now discharged. We can thus use Cnstr-Equiv to deduce (B.6. 1)
We prove that (B.6.3) is valid by showing that [[?j ? a [[E]A H (I) PO'(?) (I) ji holds. Let
(?, i, j)E [f?i JI hold. This means that (?, i, i)E I[ X ji holds as well. We conclude
(?, i,j)E [[ElA ? (1) X: [PO'(?1); PO'(X2)] (I) JI (B.6.5)
because (B.6.2) was proved valid above.
Case 1: Assume ??, i, ])E If E]A ?. According to definition (4.6) for the property defined by a con-
strained proof outline, we have (? i, j?E [[E]A ? (I) PO'(?1) (I) ?.
Case 2:			Assume			(a, i, j)? [[E]A ?.			This			assumption			and			(B.6.5)			imply
(a,i,j)E [[(I) X: [PO'(?1);PO'(X2)] fliji.
The proof outline invariant for (B.6.2) is
1'
A			((at(X') ? I) A (after(X') ? 1))			(B.6.6)
?E Lab?)
where cp ranges over the control predicates of ?. From definition (4.4) of If PO(?) ? we infer that
or else for all k, i<?k<?j: a[..k]?1'.
Case 2.1: Assume a[..ij?!'. Thus, by definition, a[..i]??I' holds. According to
definition (B.6.6) for I', we conclude a[..ijk(( v cp) A ?!) holds, which implies that
cp
a[..i]?! holds. By definition (4.4) of If PO(?1)Jj, we conclude
(a, i, ]?E If (1) PO'(X1) fI) ?. And, according to definition (4.6) for the property defined by
a constrained proof outline, we have (a, t, j? If ?A H fI) PO'(?1) (I) ji.
-36-
Case 2.2: Assume for all k, i<?k<?j; c[..k]k!'. Since (? i,j)EI[?1 Ji we have
for all k, i<k<?j: ?[..k]k(in(?1) v after(X1)). By construction (1' A (in(?1) v
is valid. So we infer that for all k, i<?k<?i: o[..k]kL I implies 4o?)' and this allows us to
conclude for all k, i?<k<?j: ?[..k]?IPoQ). Thus, by definition (4.4) of I[PO(X1) ?, we con-
dude ?O, i, j?E [[(I) PO'(?1) (I)]I. According to definition (4.6) for the property defined
by a constrained proof outline, we conclude (?, i, j?E [fE]A ? (IJ PO'(?1) fi) JI.
A similar argument establishes that (B.6.4) is valid.			El
-37-
Lemma (Relative Completeness of Cnstr-ParComp): Assume that all valid constrained proof out-
lines E]A* ? PO*(?1) and [ZIA* ? PO*(?) are provable, and assume that all valid constrained
proof outlines involving the individual assignment statements in ?i and ? are provable. Then
DA ? (pre(?j) ?pre(?2)J X: [PO(?1) /1 PO(X2)] (post(?1) Apost(?)J (B.7.1)
is provable if valid.
Proof. Assume (B.7.l) is valid. Let
ElA ? fIJ ?: [PO'(X1) // PO'(?2)] (I) (B.7.2)
be a proof outline for ?: [?i // ?] in which every asseflion in PO'(?1) and PO'(?) is
I: 1PO(??) A 4o?) A ? (pre(?1) A pre(X2))) A (after(? ? (post(?j) A post(X2))).
Observe that (B.7.2) is valid by Cnstr-Equiv, because the proof outline invariant for (B.7. 1) equals!
and (B.7.l) is valid.
We show below that
fi) PO'(?1) (I)			(B.7.3)
E]A ? (I) PO'(X1) ill (B.7A)
are both valid. This implies that (B.7.3) and (B.7.4) are provable by the assumptions of this lemma.
We also show:
For all ?? E Assig(?) where ?? is the assignment ??: [x := Ej: (B.7.5)
E]A ? fat(X)?40?? AIp0?)) Xa: [x :=E] f4o?))
is valid.
For all ?a E Assig(Xi), where ?a is the assignment ??: [x :=Ej:
H (rn(X)?jpo?? AIPo(?)J ?a: [x :=Ej f1Po?))
is valid.
(B.7.6)
By the lemma's assumption, interference-freedom obligations (B.7.4) and (B.7.5) are thus provable.
The three hypotheses needed for using Cnstr-ParComp to deduce (B.7.2) are now discharged. We
can thus use Cnstr-Equiv to deduce (B.7. 1).
We prove that (B.7.3) is valid by showing that [[X1 JI a [[E]A ? (I) PO'(?1) (1)? holds. Let
(?, i, j? [[X1 ji hold. This means that (?, i, i?E [[X ? holds as well. We conclude
(? i,i?E [[?A ? fi) ? [PO'(X1) 1/ PO'(X2)] (I) ? (B.7.7)
because (B.7.2) was proved valid above.
Case 1: Assume (o, i, j?E [[E]A ?. According to definition (4.6) for the property defined by a con-
strained proof outline, we have (? i, j)E ([ E]A ? fJJ PO'(X1) fi) ?.
Case 2:			Assume			?o, i,j?? ??A ?.			This			assumption			and			(B.7.7)			imply
(?,i,j?E `[(I) X: [PO'(?);PO'(?)] (IJ?.
-38-
The proof outline invariant for (B.7.2) is
I': A (cp?I),
cp
(B.7.8)
where cp ranges over the control predicates of X. From definition (4.4) of It PO (?) JI we infer that
or else for all k, i <k<?j: a[..kJkI'
Case 2.1: Assume a[..i]?1'. Thus, by definition, a[..i]???!' holds. According to
definition (B.7.8) for I', we conclude a[..ij?(( v cp) A ?I) holds, which implies that
cp
a[..t]?I			holds.			By			definition			(4.4)			of			[[PO(?1) JI,			we			conclude
(a, i, ]`)E `[(I) PO'(X1) (I) ?. And, according to definition (4.6) for the property defined by
a constrained proof outline, we have (a, t, i?E I[ DA ? (I) PO'(?1) (I) Ji.
Case 2.2: Assume for all k, i<?k<j: a[..k]kI'. Since (a, t, i? [[X1 Ji we have
for all k, t<k<?j: a[..k]kqn(Xj) v after(X1)). By construction (1' A (in(?1) v after(?1)))?I
is valid. So we infer that for all k, i<?k?<i: a[..k]kL I implies 1POQ)? and this allows us to
conclude for all k, i<k<?j: a[..k]?!p0??. Thus, by definition (4.4) of [[PO(?1) ?, we con-
clude (a, i, j')E [[(I) PO'(?1) (I) ?. According to definition (4.6) for the property defined
by a constrained proof outline, we conclude (a, i, j)E [[ElA ? (I) PO'(?1) (I) JI.
A similar argument establishes that (B.7.4) is valid.
We prove that (B.7.5) is valid by showing that
? (at(??Ipo???AIpo???) X?:[x:=E? (Tho?))?
holds for all X? E Assig(Xi), where X? is an assignment Xa: [x :=
For arbitrary Xa, let (a, i, j)E [[?? ? hold. This means that (a, i, j?E [[X JI holds as well. We
conclude
(a, i,j)E [[5A ? (!J X: [PO'(?1) 1/ PO'(?)j (I) ii (B.7.9)
because (B.7.2) was proved valid above. Define
PO*(Xa): fat(X) A4o?) A40(??)) X?: [x :=E] f4o???))
Case 1: Assume (a, I, j?E It E]A ji. According to definition (4.6) for the property defined by a con-
strained proof outline, we have (a, i, j?E It E]A ? PO * (Xa) J].
Case 2:			Assume			(a, i, j)? It [ZIA ?.			This			assumption			and			(B.7.9)			imply
(a, i,j?E [[(IJ X: [PO'(?1) 1/ PO'(?2)] (IJ JI.
The proof outline invariant for (B.7.9) is
I':			A			((at(?) ? 1) A (afler(?) ? I))
?E Lab?)
(B.7.lO)
where cp ranges over the control predicates of ?. From definition (4.4) of [[PO (X) JI we infer that
or else for all k, i<?k<j: a[..k]?I'
Case 2.1: Assume a[..i]?#!' Thus, by definition, a[..ij??J' holds. According to
definition (B.7.8) for I', we conclude a[..ijk(( v cp) A ?J) holds, which implies that
cp
a[..i]?!p0?? ATho(??) holds. By definition (4.4) of [[PO*(Xa)?, we conclude
(a, i, ]?E It PO * (??) J]. And, according to definition (4.6) for the property defined by a
-39-
constrained proof outline, we have (a, i, j?E [[?A ? PO * (?a) ii
Case 2.2: Assume for all k, i<?k<j: a[..k]kI'. Since (a, i,]?E [[X?? holds we have
for all k, i<?k<?i: a[..k]k(at(Xa) v after(??)).
By construction (I' A (at(?a) v			? 1 is valid.			So we infer that
forallk,i<k<--Hj; a[..kj?L			I			implies
=> (4o(?i) A A (after(Xa) ? 4o(?)) and this allows us to conclude
for all k, i<?k<?j: a[..k]?Ip0'??. Thus, by definition (4.4) of I[PO*(?a)?, we conclude
(a, i, ]?E [[PO*(??)]]. According to definition (4.6) for the property defined by a con-
strained proof outline, we conclude (a, i, j? I[ E]A ? po *(Xa) II.
A similar argument establishes that (B.7.6) is valid.
5
-40-
Theorem (Relative Completeness): Cnstr-Assig, Cnstr-SeqComp and Const-ParComp comprise a
(relatively) complete deductive system.
Proof. The proof is by structural induction on programs.
Base Case: A program consisting of a single assignment statement. This case then follows by the
Relative Completeness of Cnstr-Assig Lemma.
Induction Case: This case then follows by the Relative Completeness of Cnstr-SeqComp and Rela-
tive Completeness of Cnstr-ParComp Lemmas.			El
-41-
