BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1397
ENTRY:: 1994-03-17
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Interprocedural Data Flow Analysis Based on Temporal Specifications
AUTHOR:: Poetzsch-Heffter, Arnd
DATE:: October 1993
PAGES:: 18
ABSTRACT::
This paper investigates the specification of data flow problems by temporal 
logic formulas and proves fixpoint analyses correct. Temporal formulas are 
interpreted w.r.t. programming language semantics given in the framework of 
evolving algebras. This enables very high-level specifications, in particular 
for history sensitive problems. E.g. the classical bit vector analyses can be 
refined by using information about conditions in branches without having to 
change their specifications. The general semantics framework makes the 
approach directly applicable to realistic programming languages.

We use the specifications to prove fixpoint implementations of data flow 
analyses correct. As an example, we develop a powerful interprocedural 
deadness analysis that uses constant information depending on the context 
where the active procedure was called. By proving such a combination of 
backward and forward analyses correct, we illustrate the use of specifications 
in correctness proofs.
END:: CORNELLCS//TR93-1397
BODY::
Interprocedural Data Flow Analysis
Based on Temporal Specifications*
Arnd Poetzsch-Heffter*
Tfl 93-1397
October 1993
Department of Computer Science
Cornell University
Ithaca NY 14853-7501
Supported by DFG grant Po 432/2-1. Author moving to Munich
Interprocedural Data Flow Analysis
Based on Temporal Specifications
Arud Poetzsch?Heffter I 2
Cornell University			Institut fiir Informatik
4112 Upson Hall			Technisd?e Universita?t
Ithaca, NY 14853			D--H80290 Mijuchen
poetzsd??cs.cornell.edu poetzschCclinforrnatik.tu-muenchen.de
Abstract
This paper investigates the specification of data flow problems by temporal logic formu-
las and proves fixpoint analyses correct. Temporal fi?rmulas are interpreted w.r.t. program-
ming language semantics given in the framework of evolving algbras. This enables very
high?evel specifications, in particular for history sensitive problems. E.g. the classical bit
vector analyses can be refined by using information about conditions in branches without
having to change their specifications. The general semantics framework makes the approach
directly applicable to realistic programming languages.
We use the specifications to prove fixpoint implementations of data flow analyses correct.
As an example, we develop a powerful interprocedural deadness analysis that uses constant
information depending on the context where the active procedure was called. By proving
such a combination of backw&d and torward ai?alyses correct, we illustrate the use of
specifications in correctness proofs.
1 Introduction
Motivation Data flow analysis (DIPA) is a well?established method to provide static info-
mation about programs. Such information is typically used in optimizing compilers ([AU77]).
The quality of DFAs usually has a major impact on the code quality. Therefore, a systematic
study of sophisticated analyses is a key issue in language implementation technology.
Many papers investigating data flow analysis (in particular of imperative programming
languages) use a fixed, often rather siinple flow graph model as basis for the program semantics.
Data flow analyses are specified by local rcThtions between the information that corresponds
to adjacent nodes in the graph. This approach was very successful to set up the fundamental
theory and to develop basic algorithms. However, this approach lias the following drawbacks
when it comes to the development of powerful data flow analyses for realistic programming
languages:
1. Realistic programming languages camiot be modeled with simple flow graphs.
2. Specifications of data flow analyses using local rdations between graph nodes often do
not capture the entire original problem: i.e. they are too restrictive.
Examples to illustrate the first drawback are e.g. recursive procedures, procedure parameters or
pointers, method selection techniques in object oriented languages, parallelism. Whereas there
is already some work done to find more expressive settings, the second drawback is almost not
touched (cf. related work). Ib illustrate the second drawback, let us consider deadness analysis
of variables: A variable V is called dead at a program point P, if it is not used until it is
defined in computations following P.
proc PC):			if y=o then z:=x else x:=y-1 fi
CI)			. . . y:=3 ; PC)
1Supported by DFG grant Po 432/2-1.
2currently moving to Munid?
According to this informal definition, the variable x is dead before the assignment to y in line
(1), because whenever P is called in line (1) the value of y is 3 so that the else--Hbranch in
P is executed where x is defined. But to give a formal account of this definition using local
relations between graph nodes leads to very complex specifications. The main reasons for that
are: Parts of the language sema?ftics has to be encoded in the analysis; and the analysis has to
use information from backward and forward analyses.
Approach We show how to specify data flow problems with temporal logic formulas. The
interpretation of such formulas is defined in terms of the programming language semantics,
which is given by evolving algebras, a very expressive semantics framework (cf. section 2).
The high--Hlevel temporal specifications directly reflect the informal definitions of data flow
problems. We use the specifications to prove fixpoint implementations of DFAs correct. As the
specifications are based on the set of computations of a program, the fiapoint implementations
are usually suboptimal (in general, semantic--Hbased specifications are undeddable; see [RL77]
for an example). And this is an advantage of our method because it enables refinements
and allows to stepwise approximate the specification by more and more sophisticated analyses.
As an example, we develop a powerful interprocedural deadness analysis that uses constant
information depending on the context where the active procedure was called. We show how to
prove such a combination of backward and forward analyses correct, thereby illustrating the
use of specifications in correctuess proofs.
Related Work The correctness of fixpoint analyses was classically proved correct w.r.t. cor-
responding merge over all path analyses (-MOP). In the abstract interpretation framework, the
corresponding correctness and optiniality results are expressed by the coincidence theorems3
(see [KU77] and [KS92] for an interprocedural setting). In these works, the correctness of the
MOP analyses is simply taken for granted. In [CC79], the correctuess of abstract interpretations
w.r.t. a strongest post--H/weakest precondition semantics over simple flow graphs is investigated.
F. Nielson developed a denotational framework for data flow analysis (see e.g. [Nie87]). Both
frameworks directly relate the analyses to the language semantics like we do here. But in con-
trast to our work, history sensitive analyses (like deadness or available expression) are difficult
to specify in those frameworks, in particular when it comes to realistic programming languages.
In [Ste9l], B. Steffen used modal logic to spedfy data flow analysis and to use model
checkers to perform the analysis. His work is similar to ours in that he looks for a higher
specification level. But in his framework, the formulas are interpreted w.r.t. programs and
not w.r.t. runs of programs as we do; i.e. the modAs do not capture the language semantics
sufficiently detailled to express history sensitive analyses in full generality.
The interprocedural analysis developed in this paper profited from [KSO2] and from the
idea of semantical refinement as it is e.g. used in [WZ85]. Many aspects of our practical goals
are similar to [Ven89] (cf. conchsions).
Overview Section 2 gives a short introduction into evolving algebras, our semantical frame-
work. It defines temporal logic formulas as specification language and introduces the basic
proof rule for computational induction. Section 3 explains the speciflcalion of different kinds
of data flow analyses and relates them to the specification of an example language with recur-
sive procedures. In section 4, we describe a flxpoint implementation of a deadness analysis and
prove it correct w.r.t. its specification. Section 5 reflnes that analysis. This reflnement provides
a very powerful interprocedural deadness analysis. In addition, it illustrates that sophisticated
analyses may have very complex fixpoint definitions whereas their specifications can be very
3Notice that the induction proofs used there only apply to backward analysis of tc'rminating computations,
whereas our approach applies as well to non-terminating computations.
2
simple. Section 6 contahis the conclusions and some remarks on implementation issues further
motivating the use of evolving algebras.
2 Specification Framework
This section describes the specification framework for programming language semantics and
data flow problems. After a short introduction to evolving algebras, we define temporal for-
mulas and their validity w.r.t. computations of an evolving algebra. Then, we define a weakest
precondition transformer on state formulas that relales the step semantics given by the evolving
algebra to the temporal nexttime operator.
2.1 Evolving Aigebras as Semantics `Framework
Evolving algebras are a powerful framework for specifying and reasoning about programming
languages (for an introduction see [Gur9t]). Evolving algebras have been used to specify the
semantics of many different programming languages including C ([G1192j), PROLOC4 ([BR92];),
and Occam ([GM89]). In contrast to e.g. denotational, action, or structural operational seman-
tics, they directly provide a trace semantics whidi can be used as the semantics for the linear
time temporal logic. Beside this, they force the language specifier to make explicite the data
structures controling execution, whereas in other frameworks these data structures are only
implicite in the richer formalism (e.g. in evolving algebras expression evaluation is done by a
store semantics (see [MS76]), the control stack for recursive procedures is visible). This is an
advantage for our purposes, because it allows to refer to these data structures from the logic.
Last not least, they provide a flexible basis for iniplementations (cf. section 5). On the other
hand, other semantics could be used as well, if they have a trace semantics (like most transi-
tion systems) or are refined to a trace semantics (which can at least be done for operational
semantics). In the following, we give the basic definitions of evolving algebras; an example is
presented in section :3.2. Informally, evolvitig algebras can be considered as a set of guarded
multiple assignments I hat allow pointwise updates of functions.
A signature is a family of finite sets (FUNCs)sEN of function symbols. A first--order struc-
ture 5 with signature ? is given by a set U called the universe of 5 and an interpretation y
of function symbols, ? = (Y?)sEJN.' ?? : F(TNCs ?(TTs, ??), where ?(U8, U) denotes the
functions from U? to ?J. A computation with signature ?? is given by a universe and a sequence
(Yi)iElN of interpretations; y?j is called the i-th stat( of the computation.
Let VAR be a set of variables. "?terms, ?--Hground?terms. and quantifier4ree ?JormuThs
over =, V, A, are defined as usual. ?Ve will use an interpretation ? as well to denote its
canonical extension to ground terms. Let i' be a valuation, i.e. 1' : VAR U. By ?[H we
denote the interpretation of terms under valuation v. Furthermore, we assume the classical
notions of validity in first--order logic with equality.
Definition 2.1 Let ? be a signature.
o+ An update (over ?) is an expression of the form f(ti,.. ., tn) := t where f(t1,..., tn) and
t are ?--Hground?-terms.
o+ A transition rule is an expression II of the form if gvard(R) then updates(R) where
guard(R) is a quantifier?free closed ??formula and updates(R) is a finite set of updates.
A transition rule R is called consistent, if its guard implies that for each pair of updates
(f(si,. , sn) := 5, f(ti,. . . ,tn) := t? the disjunction si $ ti V... V 5? $ t? holds.
o+ An evolving algebri (over ?) is given by a finite set of transition rules.
3
o+ An evolving algebra is called consistent if all its rules are consistent; it is called complete,
if the disjunction of the guards is a tautology.
o+ A computation of a consistent and complete evolving algebra EA is a computation such
that for each i E IN there is a rule R in EA transforming ? into ?+i, i.e.:
--H guard(R) is valid in the structure (U, ?).
--H Denoting the updates of R by fi(?i) := I?,..., j?(Jr) := tr, we have
Y%(15) if f =--H f5 and Th =
??+??u =dej			???f)? t7)			otherwise
where j ranges over 1- r and u ?
Definition 2.1 follows the introduction of evolving algebras in [GR92]. This setting is a bit
different from the one given in [Gur9l] where all rules with true guards are executed simul-
taneously. Whereas the latter setting provides more flexibility in writing down specifications,
the focus here is to keep formal definitions simple. Each evolving algebra EA can be made
consistent by adding the corresponding restrictions to the guards and complete by adding a rule
that has the conjunction of the negated guards of EA as guard and an empty set of updates.
A pfogramming Thnguage (11, EA) is given by a set II of V?structures and by a consistent
and complete evolving algebra EA over ?. Each element of II models one program together
with its initial state and the basic data types. The computations of a program P E II are those
computations of EA that start with P. The function symbols occurring in outermost position
on the left hand side of updates in an EA are called dynamic. Zero?ary dynamic function
symbols are often called as well dynamic or flexible4 vamabies.
2.2 The Specification Language: Temporal Logic Formulas
This section introduces temporal formulas and their semantics. ?Ve use a subset of the operators
defined in [MP92]. Our formulas (and semantics) are slightly simpler in that we do not allow
quantification over dynamic variables. On the other hand, the semantics here is a bit more
general5 in that computations can change the interpretation of n?ary function symbols for
n > 0, and not only that of dynamic vanables.
Definition 2.2 Let ? be a signature and VAR be a set of variables. The set of (temporal)
formulas over ? is inductively defined as follows:
o+ if Ii, 12 are ? terms, then Ii = 12 is a formula;
o+ if F & are formulas and X is a variable, then ??F, F G, oF F?until&, PsinceC,
VX.F are formulas.
El
The operators 0? until, since express temporal properties: oJ is valid in the current state if
F is valid in the next state; F until & is valid in the current state if F is valid until C becomes
valid; F since G is valid in the current state if F is valid since & was valid the last time (the
formal definitions are given below). A formula not containing a temporal operators is called
a state formula. In the following, we assume that the signatures contain the 0-ary function
symbol true (to denote the boolean value 4?true") and that the universes contain two distinct
4The term ?flenHe vanaHe? is often used in the temporal logic community.
?If necessary e.g. to use existing t?mporal calculi, this can be eliminated.
4
elements to represent the boolean values. To improve readability, we denote true = true by TT,
write ?....] for .... . )=true, use H, V, A, ? as abbreviations with their usual meaning, and call
boolean valued functions predicates; furthermore, we use the following temporal abbreviations:
o+ =--H TT until F , called ?ventuaWy",
o+ , called ?always",
o+ FunlessG ?F v (Puntil&).
Definition 2.3 Let C = (U, (?i)iEN) be a computation, v be a valuation, and F and C be
temporal formulas,
o+ The validity of formulas  w.r.t. v in state y (denoted by (?j, v) ? P) is inductively
defined:
(?, v) t			F			iff F is a state formula and is valid in y% w.r.t. v in the usual
sense of first--Horder logic with equality;
(?, v) #			iff (y'?j, v) ? F does not hold'
w--H			 o			iff(y?,v) ? F implies (?j,K) # 0
#			oF			iff(y?+1,v) ? P hoKl?;
(yj, v) ?			F until 0			iff there is a k > such that (y?. v) ? 0
and for allj, ? ? k: (,v) ?
(y%, v) W			F since 0			iff there is a k ? sudi that (?k v) ? 0
and for allj i >j > k: (?3,v) # F
w--H			vx.r			iff (y,v') ? F holds for all valuations v'
with v(Y) = v'(Y) for Y #
F is said to be valid in a computation C w.r.t. v (denoted by (C, v) ? F) if
?--H F holds for all states ? of C. P is said to be valid in C (denoted by
C ?--H F), if (C, v) = F holds for all valuations. F is said to be valid in a pro-
gram P (denoted by P ? P) if it is valid in all computations of P. P is said
to be valid in a programming language (fl.EA) (denoted by (11, EA) # P) if it is
valid in all its programs. F is said to be valid if it is valid in all computations.
It is easy to see that for a state formula F not cou? aining dynamic function symbols P ? F
holds iff P is valid in structure P in the sense of classical first order logic with equality.
2.3 Relating Evolving Algebras to the Logic
The proofs in the following sections are carried out by computational induction, either by
showing that the proposition holds in the first state and is invariant during the computation,
or by showing that the proposition holds always sometimes in the future and remains invariant
going back in the computation history. In order to proof the induction step, we have to refer to
the evolving algebra. Therefore, we define the weakest precondition transformer wp associated
with an evolving algebra. wp transforms a state formula F into the weakest state formula such
that wp[F] oF is valid in the programming language.
As it is sufficient for the purposes of this paper and technically simpler, we define wp here
only for state formulas that contain no function symbol with arity n > 0. (The general case can
be handled by a technique described in [GR92], p. 189). Under these restrictions, we can use
the predicate transformer technique associated with [bare logic, in particular the transformers
for multiple assignments and alternative commands (see e.g. [Gri8ij, p. l2lf and l31f). But it
5
should be clear that even though the technique is the same, the usage is quite different: There
the transformers apply to program parts; here the transformer applies to the whole program.
There the pre-/postconditions cannot refer to program counter, valuation, and control stacks;
here we refer to them in the formulas. There the so?called Hoare triples relate information
before a program part to information that holds after it; here we relale information of two
successive states in a computation.
Definition 2.4 Let EA = f R11?m ? be an evolving algebra and let us denote the vector
of dynamic variables occurring on the left hand side in the updates of R? by Xffi and the
corresponding vector of right hand sides by %7j. Furthermore, let F be a state formula not
containing a function symbol with arity n > 0. Denoting the simultaneous substitution of a
vector of 0-ary function symbol with x by a vector of terms ? in a formula F by P[rju?, the
weakest precondition transformer wp is defined as follows:
wp[P]			def At?i ( guard(B?)			F?[Xffi'/flffi] )
The characteristic property of wp, namely wp[F] H oF ,follows from defintion 2.1 and the
definition of the nexttime operator.
3 Specif?ing Data Flow Problems
The first part of this section explains how data flow problems can be specified by temporal
formulas. In the second part, we give the evolving algebra of a procedural example language
and show how specifications of data flow problems are made complete w.r.t. programming
language specifications.
3.1 Specifying Data Flow Problems by Temporal Formulas
Data flow analyses usually provide information that some proposition is true at a point of a
program whenever the program reaches this point durhig execution. E.g. constant propagation
determines that an expression  has alwa??s the same value 0 at program point P. Assuming
that the programming language specification (11, EA) provides a dynamic variable PC for the
program counter and the dynamic function VAL for the valuai ion of program variables and
expressions in a state, we can specify constant propagation as follows: Find a predicate
const : (Variables U Expressions) x PointsxValues Hool
that satisfies the specification:
(ll,EA) ? const[,P,CJ (PC = P VAL() = 0)
Assuming that const captures the information determined by a constant propagation imple-
mentation, the formula expresses the correctriess of that implementation: It requires that
const[E, P, 0] may only hold if VAL() = 0 holds in all states where the program counter
is at P (in all computations of all programs). Implementations are partially ordered by the
implication, i.e. we say an implementation consti is better/more precise than const2 if both
satisfy the specification and
(ll,EA) ? const2[,P,C] constl[E,P,C]
It is a well--Hknown fact that in general optimal solution according to our definition cannot be
computed ([RL77]).
6
Many data flow analysis determine whether something lias happened before a point is
reached or will happen in the future after a point is reached. Typical examples for the first
kind called forward analyses, as the analyses follow the normal flow of program execution
__ are available expression analysis (avexp), and initialization analysis (init). Typical examples
for the second kind --H- so called backward analyses --- are very busy expression analysis (vbe),
and liveness analysis. With the liveness specification we wm as well show how to handle so
called any?path problems. When looking at the data flow specifications, one should notice that
the form of the concliisions provide a fine classification for DFAs: A DFA is history insensitive
if the conclusion is a state formula (e.g. const); whether it is forward or backward, depends on
the used temporal operators.
An expression  is called available at a point P, if in every coniputation that reaches P,
was not killed since it was defined:
(11, EA) # avexp[, Pi			(PC			P			(?Kll?L() since DEF()))
where KILL(), DEF() alibreviate formulas expressing that  is killed/defined (see below).
Initialization analysis determines that whenever a computation reaches a point P, a variable
V was defined sometimes in the past:
(fl,EA) #			init[V,P]			--H			(PC=P			(TTsinceDEE()))
An expression -? is called very busy at a point P, if it is not killed until it is used:
(11, EA) # vbe[, Pi --H (PC P --H? ( ?Kfl?L(E) until USE()))
A variable V is called live at a program point P if there is a computation in which V is not
defined until it is used after the computation reached P. As linear temporal logic can only
express properties that hold in all computations. we specify the dual problem: A variable V
is called dead at a program point P, if it is not used unless6 it is defined in computations
following P:
(11, EA) # dead[V, Pi --H (PC = P --H ( ?IfSE(V) unless DEF(V)))
In the following, we use the deadness problem as example, because it allows us to show the
correctuess of a backward analysis even for non--terminating computations and because it is
more familiar than vbe.
3.2 Data Flow Problems and Language Specification
The specifications in the last section contain wholes": The formulas KILL(), USE(V),
DEF(V) are not specified. Whereas these properties are often trivial for toy languages, they
may be a rather complex in realistic programming languages: E.g. what does it mean precisely
that an expression containing a procedure call is not killed7; what does is mean in the presence
of aliasing that a variable is used. (And in both cases data flow analysis will be necessary to
determine approximate solutions.) Of course, these properties are usual language depend. In
this section we give examples how the specification of such properties can be done based on our
language specification framework. In order to do so, we first introduce an imperative example
programming language, called SPL (for simple procedural language) in the rest of this paper.
`To be precise: (?DEF(E) until USE(E)) is equivalent to USE() unless (DEF(E) A USE(E)); but we
assume here DEF() UsE(E) which gives us the above specification (cf. 3.2).
7This information is e.g. very helpful to optimize e'xpre?siuns computing the bound in a C for?tatement.
7
Language Specification This paragraph focuses on the relevant parts of the SPL specifica-
tion. Appendix A contains the abstract syntax and the function suce on points that defines the
relation between the syntax tree and the flow graph (we use the notation of the NIAX system
(cf. [PH93b]). SPL has recursive procedures and global variables; to keep it in manageable size,
SPL does not have parameters and local variables, and the language only deals with values of
type integer. The universes of the structures modeling programs (cf. section 2.1) contain the
nodes of the syntax tree and two program points for each expression, statement, and procedure
(declaration) node, representing the points before and after that construct. Boolean functions
are used to describe a sorting of the universe; in particular there are the sorting functions: Var
for the variable (declaration) nodes, Procedure for the procedure (declaration) nodes, IntConst
for the nodes that are constants, Exp for the expression nodes, CaIIStm for the call statements,
and Point for the program points.
The elements of the universe carrying values during runtime are called objects; in our
notation, we write
Object = Var I lntconst I Exp
meaning that an object is a variable, constant8, or expression node. The control flow of a
program is modeled by a graph the nodes of which are either program points or so called tasks
(cf. appendix A). Here are the sort defintions for the tasks:
Task			=			Branch
Succ			=			Point
Branch			(			Exp.cond
Nove			(			Object.src
Binop			(			Operator.op
Call			(			Point.contin
Start			(			Task.succ )
Return			(			Procedure.proc
End
Nove I Succ Call I Return I End
Binop I Start
Task.ttsucc Task.ffsucc )
Object.dst Task.succ )
E::p.left Exp.right Exp.dst
Task.succ )
Task.succ )
The subsort Suce is introduced for later use. A branch task has three components: The
expression node representing the condition in a loop or ifstatement (selected by cond), and
the successor task for the true and false case. -? move task has as well three components: the
source and destination object and the successor task. A binary operation task has the operator,
the two argument and the result expression and its successor as components. A call task has
the point where execution continues after the call and the entry in the called procedure (succ)
as component. The return task has the procedure where it returns from as component.
The SPL specification contains the dynamic function VAL and two dynamic variables: PC,
the program counter; and CTR, the control stack.
VAL : Object -> Int
PC			:			->			Task
CTR_5			:			->			Stack(Task)
The evolving algebra of SPL defines for each task sort how to change the Qvnamic func-
tions/variables. The function eval evaluates a binary operator on the given arguments.
if			Branch[PC] A VAL(cond(PC)) = i			then			PC := ttsucc(PC)
if			Branch[PC] A VAL(cond(PC)) = 0			then			PC := ffsucc(PC)
if			Point(PC]			then			PC := succ(PC)
if			Nove[PC)			then			PC := succ(PC),
if			BinOp(PC]			then			PC := succ(PC),
VAL(dst(PC)) := VAL(src(PC))
VAL(dst(PC)) := eval( op(PC),
VAL(left(PC)), VAL(right(PC)) )
if Call[PC) then PC := succ(PC)? CTR?S push(contin(PC),CTR?S)
8To treat constants as (read only) objects makes the semantics a bit simples
if
if
if
Start(PC] then PC			succ(PC),			CTR?S			push( End()? EmptyStack()
Return(PC] then PC			top(CTR?S), CTR?S			pop( CTR?S
End[PC]			then skip
Filling the Wholes The notable aspect of formal language specifications as the one sketched
in the previous subsection is that they provide a powerful basis for specifying a wide variety
of static and dynamic properties. E.g. they provide the sets of program variables, program
points, and expressions for a given program (compare this to frameworks where the program is
modeled by an element of a term algebra). These sets are very important for the specification
of properties like KILL(), USE(1'), DEF(U). In order to complete the deadness specification
given in 3.1, we have to specify what USE(IJ) and DEF(v) mean in SPL:
USE(v)			=def			Var[V] A Alove[PCj A src(PC) =
DEF(V)			def			Var[V] A Move [PC] A dat(PC) = 1
i.e. a variable V is used/defined in a state if the program counter is at a move task and the
source/destination of that task equals V. In SPL, there is never a read and write to a variable
in one step, i.e. (DEF(V) A USE(V)) is valid in SPL. This is due to the fact that we use a
store semantics where the value of a variable on the right hand side of an assignment is first
moved to the corresponding expression node (see appendix A).
4 Correctness of Fixpoint Implementations
As shown in the last section, a temporal specification of a data flow problem is given by a
temporal logic formula with say free variables ..... ., Un. A corresponding implementation is
considered to be a n-?ary predicate dfa; we say dfa captures the implementation. To be more
precise, each program structure in TI is extended by the dfa predicate and possibly some auxil-
iary predicates; the extension of II is denoted by fl?dJa?...) The properties of an implementation
are expressed by a finite number of state formulas ..... ., Pm over ?` U fdfr?(n),. .J where ?`
is the signature of the programming language without the dynamic symbols; i.e.:
(ll?d1a,..4,EA)# P1A...APn
Usually, the axioms ?? express the well--Hknown fixpoint properties of data flow analyses (see
below) and can often be directly used as an input to a fixpoint finding evaluator (see the
remarks in the conclusions). Proving correctness of an implementation then means to prove
that
(H?dJa..?,EA) # dfa[ViUn]			SPEC(U1,. .
holds where SPEC(U1?..., Un) denotes the temporal specification of the problem. Usually the
axioms Fj do not uniquely characterize the implementation. but define necessary conditions
for the correctness of an implementation. 1?.g. the implementor may choose the fixpoint that
provide the "best" information.
This section gives a fixpoint characterization of a simple deadness analysis for SPL, called
sdead, and proves it correct w.r.t. the specification of the previous section. The following
section investigates more complex implementations providing better information. The analysis
sdead satisfies the following axiom:
sdead[U, T] --H? Var[I7] A Task[7?
A ( Aiove[TI V = dat(T) V (V # a?c(T) A sdead[U,s'ucc(T)]) )
A ( BranchjT]			sdead[V, ttsucqT)] A sdead[U,ffsucc(7?)] )
A ( Succ[T] sdead[V, succ(T)] )
A (CalI[T] sdead[U, succ(T)])
A ( J?eturn[7?			VP: CONTINP(P,proc(T))			sdead[U,P] )
9
where CONTINP(P, PROC) hotds if P is the point after a call site of procedure PROC (the
formal definition of CONTINP is given in appendix A). Recalling that proc yields ---Hgiven a
return task?the returning proa?dure, the last line says that a variable is dead at a return task
if it is dead after all call sites of the returning procedure in the program. Let us denote this
axiom by FIXPDEAD(V, T); it essentially spells out a simple graph based fixpoint specification
of deadness using our logical framework. Obviously, FIXPDEAD(V, T) is a state formula not
containing dynamic symbols. And, there are predicates satisfying FJXPDEAD(U, T) because
sdead occurs only positive on the right hand side of the equivalence (cf. [GS?6]). The correctuess
of sdead is expressed by the following theorem where SPL?sdead) denotes the extension of SPL.
Theorem 4.1 Each implementation sde(?d satisfying EIXPDEAD(V, T) is correct w.r.t. to the
temporal specification of the section 3; i.e. if
SPL4sdead) # FIXPDEAD(U,T)
then
SPL?sdeady ? sdead[V, T] (PC = `7 (?USE(U) unless DEF?( V)))
E
The proof of theorem 4.1 is given in some detail to demonstrates the basic proof principles
needed for showing data flow analyses correct. In particular, the proof demonstrates bow
correctness can be established even for non--Hterminating computations.
Proof Assuming that FIXPDEAD(U,T) is valid in 8PL4sd?ad), we have to show
SPL4sd?d) # sdead[V, PC] ?USE(U) unless DEF(U)
Let us abbreviate this formula by CORR(U). The proof runs by backward computational
induction, i.e we show
1. SPLlsdeady # ? CORR(V)
2.			SPi?8d?d) # oCORR.(V)			CORR(U)
Ad 1: In order to show ?CORR(U), we consider the cases ??USE(U) and ?USE(U).
Case1: The definition of unless gives E) USE(U) ( ?USE(U) unless DEF(L)) which
implies ??USE(V) CORR(U) ; by the law P ?F and the transitivity of the
implication we get E]?USE(V) ? CORR(U).
Case2: Using the fact that variables are not simultaneously read and wntten, i.e. USE(U)
?DEF(V) and expanding the definition of USE we get
USE(V) ?DEF(V) A Var[U] A Move[PC] A src(PC) = V
By expanding DEF and propositional simplification, we get
USE(V) Var[V] A Move[PC] A V ? dst(PC) A V = src(PC)
As the conclusion implies the negated right hand side of FIXPDEAD(V PC), we conclude
USE(V) sdead[V, PC] ; and because of F 0 F <>F --H ?0 we have
?USE(V) --H ?CORR(V)
As E]?USE(V) V ?USE(V) is valid, proposition 1 is proved.
10
Ad 2: The prove of the backward induction step consists of two parts: First we show that
INV =?q ?DFF(V) A sdead[V, PC] wp[sdead[V, PC]]
is valid in SPL?8deady. Then, it is shown that INV implies a CORR(V) --H CORR(V).
Step1: Using FIXPDEAD and performing some simple propositional simplifications, it is easy
to see that the premise of INV imphes
A
A
A
Branch[PC]
Move[PC] v
(1?etttrn[PC]
sdead[V, PC]
--H sd?ad[U, ttsucqPC)] A sdead[V,ffsuc?(PC)] )
Succ[PC] V CaiI[PC] sdead[V, succ(PC)]
--H VP: CONTINP(P.proc(PC)) --H sdead[V?,P]
The weakest precondition of sd?ad[?) PC] is
Branch[PC] A VAL(cond(PC))			1			--H			sd?ad[V, it?ucc(PC)] )
A			( Branch[PC] A VAL(cond(PC))			0			--H			sdead[U,ffsucc(PC)] )
A			( Point[PC]			--H			sd?ad[V, succ(PC)]
A			( Illove[PC]			--H			sd?ad[V, ?ncc(PC)]
A			( BinOp[PC]			--H			sdead[V, a'?cc(PC)]
A			( Caii[PC]			--H			sd?ad[V.sz?cc(PC)]
A			( Start[PC]			--H			sd?ad[V,succ(PC)] )
A			(J?eturn[PC]			--H			sdead[V, top(CTR)]
A			( nd[PC]			--H			sdead[?') PC]
For all cases except the return case propositional reasoning is sufficient to show the implication.
The return case is shown using the kmma
Return[PC] --H CONTINP( iop(CTR), proc(PC))
which simply says that on return of a procedure J) there is a call site of P on top of the control
stack. The prove of this lemma is sketched in appendix B.
Step2: The prove that INV implies a CORR(U) --H CORR(??) uses the basic property of wp,
i.e. wp[sdead[V, PC]] --H asdead[V, PC] ; uses USE(V) --H sdead[V, PC] (which was proved in
Ad 1); and uses the inductive characterization of unless. Details are given in appendix B.
Thd.
5 Refining Fixpoint Implementations
Of course, the simple fixpoint solution presented in the previous section provides a rather rough
approximation to the specification. E.g. in the program
proc ?() : if y=O then z:=y else y:=y-1 ; ?() fi
(I)			. . .			?() ; x:=O
(2)			...			?() ; z:=::
the variable x is dead before the call to ? in line (1), but this cannot be detected by sdead,
because sdead "identifies" all continuations of ? and x is obviously live after the call in line (2).
This section presents two refinements of the simple deadness anakvsis. The first one makes
use of an idea underlying most interprocedural data flow analyses; the second uses information
from constant propagation to improve the result. For both refinements, we will sketch how to
prove them correct w.r.t. the temporal specification.
ii
Interprocedural Analysis ??e main idea of interprocedural data flow analysis is to first
compute the mapping procedures perform on data flow information and then to use these
mappings to compute the data flow information itself (cf. [KS92]). For the refined deadness
analysis ipdead (for interprocedural deadness), we introduce an auxiliary predicate pdead that
tells us that a variable V is dead at a task in a procedure P assuming that it is dead at the
end of P. The characterization for ipdead is identical to that of sdead except for the call case:
ipdead[V,T] H
A (Call[T]
A
pdead[V,T] H
A (Move[T]
A (Branch[T]
A (Succ[T]
A (Call[T]
ipdead[V, succ(T)]
v (pdead[V, 6ucc(T)] A ipdead[V, cont?n(T)j )
ipdead[V, Tj v ( Var[Vj A Task[T]
V = dst(T) v (V # src(T) A pdcad[V, succ(T)])
pdead[V, ttsucc(T)] A pdead[?) ffsucc(T)]
pdead[V, svcc(J?)] )
pdead[V, svcc(T)] A pdead[V, cont?n(T)] )
An analysis that computes the greatest fixpoint of the above axioms determines that variable
x is dead before the call to q in line (1), as pdead[x, Qo] holds for Qo being the first point in
procedure ?. The correctness proof for ipdead has the same structure as the correctness proof
of sd?ad. The difference is that instead of CORR(V) we have to use
ipdead[V,PC] v (pdead[V,PCj A ipdcad[V,top(CTR?)]) ?VSE(V) unless DEF(V)
ill the induction step.
Two Refinements Using Constant Infomation Even though the above analysis gives us
optimal results (in the sense of [KS92]) for fixpoint specifications that take only uses and defi-
nitions of variables into account, it is obviously not the best solution we can get. Here, we show
how to use information obtained by constant propagation to produce better approximations
to the temporal deadness specification. Of course, other analyses could be used as well (or in
addition) like e.g. interval analysis. The main point here is that the simple temporal specifica-
tion remains the valid reference to prove correctness whatsoever sophisticated the analysis is.
In addition to this, the refinement exemplifies how to combine data flow analyses and how to
use their specifications in proofs.
The two refinements discussed in this section will solve the problem illustrated by the
program fragment in the introduction. To focus on the main issues, we refine here the simple
deadness analysis of section 4. The corresponding refinements for ipd?ad are spelled out in
appendix C. The first refinement uses the constant information captured by const introduced
in section 3. The refined version of sdead is obtained by replacing the branch case in its fixpoint
characterization by
A (Branch[T]
A ( Branch[T]
A (Branch[T]
A const[cond(T), T, 1] sdead[V., ttsucc(T)] )
A const[cond(T), T, 0] sdead[V,ffsucc(T)] )
A ?const[cond(T), T, 1] A ?`const[co??d(T), T, 0]
H sdead[V, tlsucqT)] A sd?ad[V,ffsucc(T)] )
i.e. whenever we know the outcome of the test, we claim the deadness only for the taken
branch. The correctuess proof of implementations characterized by this axiom differs from
that of theorem 4.1 only in that we have to use lemmas of the form sconst[cond(PC), PC, 1]
12
VAL(cond(PC)) ? 0 to prove ?DEF(V) A sd?ad[V, PC] --H wp[sdead[V, PC]] . And they
are almost direct consequences from the const specification.
Assuming a reasonably powerful implementation for const, our refined deadness analysis
detects the deadness of x in the program fragment of the introduction at least if the call to
P is the only call of P in the program. If there is a second call to P with a different context for
y, e.g.
(2)
y:=O ; P()
sdead again fails to detect the deadness of x at the beginning of line (1), because the constant
propagation const can not distinguish different calling contexts of P. But in applications, it is
by far more interesting to analyse a procedure in its different calling contexts (in particular
to take actual parameter values into account) than to profit only from dead code elemination
as the above analysis does. The following refinement provides such an analysis by making the
constant and deadness information at a task depend on the call site from which the procedure
enclosing the task was called. By giving this refinement, we not only present a very powerful
deadness analysis (in particular in the interprocedural version), but provide as well a good
example to show the power of our framework. It goes without saying that the used technique
applies as well to refine other data flow analyses.
For the refinement, we need a constant propagation satisfying the following specification:
cconst[E,T,SITE,C]			(PC = T A top(CTR) = SITE			VAL(E) =
i.e. if cconst[E, T, SITE, C] holds, then expression I; has the value C whenever control reaches
task T and the active procedure was called from site SITE (cconst stands for context sensitive
constant propagation). To reuse above definitions, we represent call sites by the corresponding
continuation point, i.e. the point after the call statement; accordingly, the call site of the
main procedure is represented by the end task (this was til now hidden in the definition of
CONTINP). The refined deadness analysis is characterized by two axioms: The first axiom is
the fixpoint equivalence for the deadness analysis csdead where calling contexts are taken into
account. The second axiom expresses that a variable is dead if it is dead according to all call
sites:
csdead[V,T,Sj
A (Move[T]
A (Branch[T]
A (Branch[T]
A (Branch[T]
A (Succ[T]
A (CaIl[T]
A (Return[T]
dead[V,T] H
A ( Starl[7?]
A (Stafl[T]
A
A
A
Var[V] A Task[T] A CONTlNP[S, ?nc'?proc(T)]
V = dst(T) V (V # src(T) A cad?ad[V, succ(T), 5]))
cconst[cond(T), T, 5,1] --H csdcad[V, itsuc?T), 5]
cconst[cond(T), T, 5.0] cadead[V,ffsucc(T), 5]
?cconst[cond(T). T, 5, I] A ?cconst[cond(T), T, 5,0]
--H c.sdead[V, !t.succ(T), 5]) A csd?ad[V,ffsucc(T), 5]
--H csdead[V, s?cc(T), 5]
--H c?dead[V, succ(T), coni?n(T)]
--H VS': CONTINP(5',enciproc(5)) --H csdead[V,S,S']
Var[V] A Task[T]
VS : CONTINP(S, ?ncl?prnc(T)) --H csdead[V, T, 5])
csdead[V, succ('F). 1nd()]
The interesting cases of the axiom for csdcad are he call and return task. For the call case
it is required that the variables have to be dead at the beginning of the called procedure
w.r.t. the call site (represented by the continuation point). For the return case, variables are
required to be dead after the current call site in all possible calling contexts 5' of the procedure
enclosing 5. The function enc1?proc yields for each task the enclosing procedure, and the
dumn? element nil for the start and end task; i.e. for the rel urn task of the main procedure
13
we get that CONTINP(S', enci?proc(End())) is not valid for any 5'. This means that every
variable is dead at the return task of the main procedure and is the desired behaviour. The
special treatment of the start task in the axiom for dead is necessary, because there is no calling
context for the start task.
Again the correctuess prove for csdead follows the lines of 4.1; but instead of CORR(V)
we have to show csdead[V, PC, top(CTR?S)j ?I?SE(V) unless DEF?(V) using the
specification of econsi.
6 Conclusions
The development of data flow analyses can benefit from high--Hlevel semantics--Hbased specifica-
tions. Such specifications allow to formally define the general goal of a data flow problem in
an intuitive way based on the programming language semantics whereas graph--Hbased speci-
fications often exclude interestirig solutions from the very beginning. Complex and powerful
analyses can then be proved correct w.r.t. the high--Hlevel specification. We chose evolving al-
gebras as semantics framework. because they were successfully used for the specification of
many different, realistic programming languages (cf. sect ion 2.1) and provide a trace semantics
which is helpful if not necessary to handle history sensitive analyses. As specification language
for data flow problems we proposed formulas of linear time temporal logic and defined their
validity w.r.t. evolving algebras.
After showing how to use temporal formulas to specify some classical data flow analyses,
we stepwise refined a deadness analysis. The development of this example analysis had four
goals: It should
1. illustrate correctness proofs in our framework;
2. show how different analyses (here a forward and backward analysis) can be combined;
3. demonstrate that sophisticated fixpoint--Hbased data flow analyses can become very com-
plex even for simple data flow problems which is here understood as a motivation for
using higher--Hlevel specifications;
4.
give an idea how refinements can be constructed by approximating state information;
first, we approximated the function VAL, then the top of the control stack; therefore it
is necessary to have all state information explicite in the language specification as it is
the case for evolving algebras.
The presented work should be understood as a further step towards semantic--Hbased devel-
opment of efficient language implementation. As [Ven???9], we are interested in constructing
tools to support such developments. Currently, we are implementing a system that generates
interpreters from a combination of an attribute grammar like formalism arid evolving algebras
(cf. [PH93a] and the specification in appendix A). This system provides all the notions we have
used throughout this paper. In a next step, we want to integrate a fixpoint evaluator to the
system that allows prototyping data flow analysis based on special forms of axioms. Concern-
ing the correctness proofs, our goal is to apply proof development systems; the use of a formal
logic framework is a first step in this direction.
References
[AU77] A. V. Aho and J. D. Uliman. Princ?Ths of Co?npiThr Design. Addison-Wesley, 1977.
[BR92] E. B5rger and D. Rosenzweig. A simple mathematical model for full Prolog. Technical
Report TR--H33/92, Dipartimento di Informatica, Universita di Pisa, 1992.
14
[CC79]
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. Con-
ference Record of the 6th ACAl Symposium on Principles of Programming Languages,
1979.
[GH92j Y. Gurevich and J. Huggins. The semantics of the C programming language. In
E. B5rger el al., editor, Computer Science Logic, pages 274--H308,1992. LNCS 702.
[GM89] Y. Gurevich and L. Moss. Algebraic operational semantics and Occam. In E. B6rger
et al., editor, Computer Science Logic, pages 176--H192, 1989. LNCS 440.
[GR92] P. Glavan and D. Rosenzweig. Communication evolving algebras. In E. B5rger et al.,
editor, Computer Science Logic, pages 182--H215,1992. LNCS 702.
[Gri8l] D. Gries. The Science of Programming. Springer, 1981.
[GS86] Y. Gurevich and 5. Shelali. Fixed--point extensions of first--Horder logic. Annals of
pure and applied logic, 32, 1986.
[Gur9l] Y. Gurevich. Evohing Algebras, volume 43, pages 264-284. EATCS Bulletin, 1991.
[KS92] J. Knoop and B. Steffen. The interprocedural coincidence theorem. In P. Pfaliler
U. Kastens, editor, Compiler Construction. 1992. LNCS 641.
[KU77] J. B. Kam and J. D. Ullman. Monotone data flow analysis frameworks. Acta Infor-
matica 7, pages 309--H317,1977.
[MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems.
Springer--HVerlag, 1992.
[M576] R. Milner and C. Stratchey. A Theory of Programming Language Semantics. Chapman
and Hall, 1976.
[Nie87]
F. Nielson. Denotational theory of abstract interpretation. In 5. Abramsky and
C. Hankin, editors, Abstract Interpretation of Declarative Languages. Ellis Horwood
Limited, 1987.
[PH93a] A. Poetzsch-Heffter. Developing efficient interpreters based on formal language spec-
ifications. To appear, 1993.
[PH93b]
A. Poetzsch-Heffter. Programming language specification and prototyping using the
MAX system. In J. Penjam M. Bruynooghe, editor, Programming Language Imple-
mentation and Logic Programming, 1993. LNCS 714.
[RL77] J. H. Reif and R. Lewis. Symbolic evaluation and the global value graph. Conference
Record of the 4th ACAl Symposium on Principles of Programming Languages, 1977.
[Ste9l] B. Steffen. Data flow analysis as model checking. In T. Ito and A. R. Meyer, editors,
Theoretical Aspects of Computer Sofiware, 1991. LNCS 526.
[Ven89]
G. A. Venkalesh. A framework for construction and evaluation of high--Hlevel specifi-
cation of program analysis techniques. ACAL Conference on Progamming Language
Design and Implementation, 1989.
M. N. ?Vegman and F. K. Zadek. Constant propagation with conditional branches.
Conference I?ecord of the 12th ACA? Symposium on Principles of Programming Lan-
guages, 1985.
[WZ85]
15
A Specffication of SPL
This part of the appendix contains the abstract syntax of SPL and the function 8ucc on points
that defines the data flow graph. We use the notation of the MAX system (cf. [P1193a] for
details). Besides this, we define the initial state of the dynamic valuation function VAL and
CONThNP(P, PROC).
Program			(			DeciList )
DeciList			*			Deci
Deci			Var I Procedure
Var			ident
Procedure			ident StatList )
StatList			Stat
Stat			While I lfStat
While			Exp StatList
lfStat			Exp StatList
Assign			ident Exp
CaliStat			ident )
*
Assign I CaliStat
StatList )
Exp lntConst I Varid I Call I BinEip
lntConst Int )
Varid ident )
BinExp			Operator
Operator Add I
Exp Exp
Sub I Nul I Div I Eq I Lt
The following function succ defines the successors to program points and thereby the data
flow graph. It uses the functions before and after yielding the point before and after a node;
the function node yielding the node corresponding to a point; the function next yielding the
next point according to a left to right tree traversal; and the function dcci yielding for each
identifier the corresponding dec]aration node. Let us explain the used not al ion for the case
I Assign<1D?N> A
Nove( N? decl(1D)? after(A) )
where the parameter P is a point after its corresponding node N and N represents the right hand
side of an assignment statement A. If this is the contexi of P than its successor is the utove task
that has N as source, the variable decl(TD) as destination. and the poini after the assignment
as successor.
FCT succ( Point P ) Task:
LET N == node(P)
IF NOT ( ProcedureEN]
I P = before(N)
IF Procedure<?,???,SL> N
I			Assign<ID,E> N
I			Varid<ID> N
I			CallStat<ID> N
I			BinExp?<?,LO,?> N
ELSE next(P)
I			P =			after(N)
IF			Procedure N
I			While<N?BD> W
I			While<E?N>
I			IfStat<N,TB,EB>
IfStat<?,N,?> IS
I			Assign<ID,N> A
I			BinExp<O,L,N> E
ELSE next(P)
ELSE nil()
OR Exp[N] OR Stat[N3 OR StatList[Nj ) : nil()
before(SL)
before(E)
Nove( decl(lD), N? after(N) )
Call( after(N), before(decl(ID))
before(LO)
Return( N
Branch( N, before(BD), after(W)
before(E)
Branch( N, before(TB), before(EB)
after(IS)
Nove( N? decl(lD), after(A) )
BinOp( term(O) L? N? E, after(E))
16
The initial state of the dynamic valuation function is as follows:
FCT vAL( Object OBJ ) Int:
IF Var OBJ			:			0
Intconst<I> OBJ : I
ELSE nil()
Finally, we give the defInition of CONTINP(P, PROC):
CONTINP(P, PROC) =dej
Procedure[PROC] A ( (Paint[P] A PROC = decl(flrstson(node(P))) ) v End[P]
B Proof Refinements
This part of the appendix provides the steps left out in the proof of theorem 4.1.
The Lemma: First, we skc'tch the proof of the lemma
Ret'urn[PC]			CONTINP( top(CTR), poc(PC))
which says that on return of a procedure P = proc(PC) there is a call site of P on top of the
control stack. The idea is to prove
SPL ? i> 0 A 5 = pttsk(PC,CTR)
CONTINP(top(i + 1, 5), fw:nci4?roc(top(?, 5)))
v top(i + 1,5) = nil v Start[PC]
by computational induction where top(i, 5) stands for applying top `i-times to 5 (i > 0). Let
us denote the above formula by INV2. For i = 1, INV2 simplifies to
CONTINP(top( CTR)), encl?proc(PC )))
and because of Return[PC] proc(PC) = encl?proc(PC) this is sufficient to proof the lemma.
The base case of the computational induction is trivial as Start [PC] holds in the initial
state. Because of wp[fNV2] a INV2 it suffices to show for the induction step that JNV2
wp[INV2] is valid in SPL. The proof of that is straightforward, but rather technical and
therefore not carried out here.
Second Step of Ad 2: Because of wp[sdead[V, PC]] osd?ad[V, PC] the formula INV
implies
?DEF(V) A sdead[V, PC]			osdead[I) PC]
implying
osdead[V,PC] v ?sd?ad[V,PC] v DEF(V) v a( USE(1')unlessDEF(17))
which is equivalent to
(osdead[V, PC] A a (USE(V)unless DEi'(v))) v C()NCL
where CONCL =d?J ?sdead[V, PC] v DEF(V) V o( USE(V)unless DF(V)). As
?sdead[V? PC] v ?USE(W) is valid in C (s. above), CONCL is equivalent to
(?s&ad[V, PC] v mUSE(V)) A CONCL
17
Applying distributivity twice, we get
?sdead[V, PC] v (?USE(v)) A DEF(V)) v (?USE(v) A o( USE(V)unless DEF(V)))
Because of (DEF(V) --H ?USE(V) this implies
?sdead[V, PC] v DEF(V) v (?USE(V) A o( USE(W)unless DEF(v)))
Using the inductive formulation of unless, we get
?sdead[V, PC] v USE(V)unless DEP(v)
And it is easy to sea that
(?sdead[V,PC] v ?USE(V)) A ?sdead[V,PC] v USE(V)unless DFP(17)
is equivalent to CONCL.
C
Interprocedural Deadness Analysis Using Context Depen-
dent Constant Propagation
This part of the appendix provides the fixpoint axioniatization for the refinement of
ipdead/pdead by context dependent constant information as illustrated for sdead in section
5. The resulting predicates are called cipdead/cpdead:
cipdcad[V, T, 5] --H
A (A'Iove[T]
A (Branch[T] A
A (Branch[T] A
A (Branch[T] A
A (Sncc[T]
A (Call[T]
A ( Return[T]
cpdead[V, T, 5]
A ( Alove[T]
A ( Branch[T]
A (Branch[T]
A (Branch[T]
A ( Succ[T]
A ( Call[T]
)v
dead[V?T] H
A ( Start[T]
A ( Start[T]
A
A
A
Var[V] A Task[T] A CONTINP[5, enc1?p?oc(T)]
v = dst(T) v (V $ ?rc(T) A cipdead[??succ(T), 5]))
ccoust[cond(T), T, 5,1]			--H			c'ipd?ad[V, iisucc(T), 5])
ccor?st[cond(T), T, 5, 0]			c?pd?ad[V,ffsucc(T), 5])
?cconst[cond(T), T, 5, 1] A ??cconst[cond(T) T, 5,0]
c'ipdead[V, ilsucc(T), 5]) A c?pdead[V,ffsucc(T), 5])
cipdead[V. succ(T), 5])
cipdead[V, sttcc(T), cont?n(T)]
v (cpdead[V, succ(T), con??n(T)] A cipdcad[V, conl?n(T), 5]))
VS': CONTINP(5',enc!proc(5)) cipdead[Th5,5'] )
V?zr[V] A Ta'sk[T] A CONTINP[5, encI?p'roc(T)]
V = d?t(T) v (V $ src(T) A cpdead[V, s?cc(T), 5]))
cconst[cond(T), T, 5,1]			--H			cpdead[V, tt.succ(T), 5])
cconst[cond(T), T, 5,0]			--H			cpdead[V,ffsucc(T), 5])
?cc??nsI[cond(T), T, 5,1] A ?`cconst[cond(T). T, 5,0]
--H cpdead[V, ttsucc(T), 5]) A cpd?ad[V,ffsucc(T), 5])
--H cpd?ad[V,succ(T),5]
--H cpd?ad[V, succ(T), contin(T)] A cpdead[V, conlin(T). 5])
cipd?ad[V, T, 5]
Var[V] A Task[T]
--H VS: CONTINP(5,enc!proc(T)) --H cipdead[V,T,5])
--H c?pdead[V, succ(T), Lnd()] )
