A Formal Representation for Plans in the Programmers Apprentice

Abstract

A pl1n c1lculus is presented which is being used to represent programs 1nd a library of standard data and ccmlrol abstractions in the progr~mmer's apprentice. Important features of this formalism include : programming lan~uage independence, additivity, verifiability and multiple points of view. The logical foundations of the represent a lion are specified formally using a situational calculus in which side effects and overlapping mutable data structures are accounlet;l lor . The plan calculus is compared·with other formalisms,. such as program schemas, and its advantages pointed out.

I . Introduction

1 n1s paper reports on recent developments in a lormalism called the plan calculus which is being used in the programmer's apprentice [27) to represent and reason about programs. The plan calculus was originally developed by Rich and Shrobe [25] and wu subsequently el1boraled by Shrobe [34] and Waters [38]. Most recently the author has extended the plan calculus by adding

data .. ustraclion and multiple points of view, as well as by providing 1 formal semantics.

The goal of the programmer's apprentice project is to develop a knowledge-based tool lor program development . The programmer's apprentice attacks the complexity barrier (41] in programming in several ways :

(i) by prov~ing an on-line database of design decisions, documentation and descriptions of a program's design at various levels of detail;

(ii) by reasoning about these descriptions to detect Inconsistencies and predict the influence of incremental changes;

(iii) and by providing a library of standard forms lor use in program construction and analysis.

This paper focusses on the representation used in building the library of standard forms. Reasoning about plans will not be discussed in detail (see [34]1, other than to describe the formal system in which such reasoning lakes place; nor will the detailed contents of the library be discussed, other than to show some examples.

The utility of a library of standard forms in program development is motivated by the observation that . expert programmers (like experts in many other fields) are distinguished from novices by their use of a much richer vocabulary of

1. Support for the l1boralory's artificial intelligence research has been provided in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research contracts 11100014-75-C-0643 and NOOOI4-80-C-()505, and in pari by Nation1l Science Foundation grant MCS-7912179. The views and conclusions contained in I his paper ~re those of the author, and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Department of Defense, the Nalion1l Science Foundation, or the United Stales Government.

A FORMAL REPRESENTATION FOR PLANS IN THE PROGRAMMER·s APPRENTICE

Ch1rles Rich

The Artifici1l lnttlli&tnct l1bontory 1 Mnuchusetls Institute of Technolocy Clmbrid&e, Mnuchusetls 02139

intermediate level programming concepts. The novice programmer thinks of constructing a program out of assignments, tests, arrays, [)() loops, etc., whereas the expe.rl programmer worlt,s with larger, tess l1nguage-specilic concepts, such as searching, accumulation, hashing, etc. There are deep reasons for this having to do with managing the complexity of the design process [26]. To the extent that the programmer's apprentice can provide a library of such standard building blocks, the programmer benefits by a reduction in the amount he needs to say to construct a ptogram.

The idea of developing libraries of standard software components to gain the same benefits thai the use of standard components has provided in other area5 of engineering Is not new [32]. I believe that part of the reason efforts in this direction have not been more successful is because of deficiencies in the formalisms usP.d. The plan calculus i.s an attempt to remedy these deficiencies.

2. The Plan Calculus

To a first approximation, the plan calculus may be thought of as unifying in one formalism ideas from flowchart schemas [18], data flow schemas [8], program transformations (6,1,5] and 1bslracl dale types [17]. An example of a plan is shown in Fig. I. The details of the notation used in this figure can wail until later; lor now the reader may note thai a plan is basically a hierarchical structure made up · of different kinds of boxes and arrows. The inner rectangular boxes denote operations and tests, while the arrows between boxes denote data flow (solid arrows) and control flow (hatched arrows). The chief features of this representation, as compared with previous formalisms are es follow.

• (i) Language Independence. To echieve some measure of canonical form, the plan calculus suppresses features of a program which stem soley from the way an algorithm must be expressed in a particular programming language.
• (ii) Additivity. For a library to be easy to use, the rules lor combining forms must be straightforward and explicit. In the plan calculus, the result of combining two non-contradictory forms is always a form which satisfies the constraints of both of the original forms.

(iii) Verifiability. Simply having a library of standard forms addresses only the low productivity pari of the soltwtre crisis. The plan calculus also provides leverage on the software reliability problem by providing a methodology (in this case, an axiomatic semantics) lor verification of library components. Furthermore, this methodology provides a framework in which inconsistencies between uses of standard forms can be detected.

(lv) Multiple Points Of View. Multiple and overlapping points of view are represented in the plan calculus by overlays between plans. An example of an overlay is shown in Fig. 2 (to be discussed further in the next section). Overlays are used to express the relationship between levels of implementation, to describe overlapping module hierarchies, and to decompose dale and control structures in ways which make their relationship to the library more expl ictl .

An additional desideratum we set for representing the library of standard forms in the programmer's apprentice Is thai the formalism must be neutral between analysis, synthesis and verl(ication of progr.ms. This turns out to be of great practictl Importance for building ·an interactive programming aid, since in real program design situations all three of these activities are Intermingled. A neutral representation of standard forms is tlso theoretically more Interesting since It is more likely a priori to capture significant futures of human understtnding of these forms than a representation tailored speclflcaUy for analysis, synthesis or verification only. ·

Comparison with Other Formaliama

Past efforts to construct knowledge bases for automatic or partially automated programming have used one of the following formalisms : program schemes {11], program transformations (6,1,5 ], program ref inement rules [2], or formal grammars [30]. Although each of these representations has been found useful in certain applications, none combines all of the important features of the plan calculus listed above. This section will serve both to contrast the plan calculus with these other formalisms, tnd ts the preliminary to 1 more careful definition of the plan calculus to follow.

For example, program schemas (incomplete program texts with constraints on the unfilled parts) have been used by Wirth {42) to catalog programs based on recurrence relations, by, Basu tnd Misra [3] to represent typical loops for which the loop invariant is already known, and by Gerhart [11) and Misra {23) to represent and prove the properties of various other common forms. Unfortunately, the syntax of conventional programming languages Is not well suited lor the kind of generalization needed in this endeavor. For example, the idea of a search loop (· slandtrd programming form) expressed informally in English should be something like the following.

A search loop is a loop with two exits in which a given predicate (the same one each ljme) is applied to a succession of objects until either the predicate is satisfied, in which case thai object is made av.ailable for use outside the loop, or the objects to be searched are exhausted.

In Lisp, as in other languages, this kind of loop can be written

I

I

In lnnumer.ble forms, many of which are syntactically (and structurally) very different, such as :

(PRO& () LP (COND (exhausted (RETURN NIL))) ( COND ( (pr~icale current)( RUURN current)) I (60 lP)) or with only one RETURN instead of two, (PRO& () LP (COND (exhausted NIL) (T ... ( COND ( (pr~ie~te current) ( RUURN current Ill (60 LP)))) or even recursively, e.g. (DEFINE SEARCH() (COIID (exhaust~ NIL I (T ... (COND ((pr~icate current) current) (T ... (SEARCN))) I) I

The problem here is that conventional programming :anguages are oriented towards specifying computations in enough detail so that a simple local interpreter can carry them out. Unfortunately a lot of this detail is often ~rbi,lrary and concepluaHy unimportant. In the plan calculus, all three of the schemas above (and many other such variations) are expressed by the single plan shown in Fig. 1.

A new generation of programming languages descended from Simula [7], such as CLU [16] and Alphard [33], provide a syntax for specifying standard forms such as the search loop In a more canonical way. However, there are two more fundamental difficulties with using program schemas to represent stand.,d program forms, which Simula and its descendants do not solve. First, programs l1nd therefore program schem1s) are not in general easy to combine, nor are they additive. This means that when you combine two progr1m schemes, the resulting schema is not guaranteed to utisfy the constraints of both of the original schemes, due to such faCtors as destructive inler~ctions between variable assignments. Second, existing programming l1nguages do not allow multiple views of the ume progr1m or overl1pping module hierarchies. I believe the reason for this Is that 1 program

Flaure 2. Overlay Between Accumul·lion on the W1y Down va. Up.

I

Is still basically thought of, from the standpoint of these languages, as a set of instructions to be executed, rather than as a set of descriptions (e.g. blueprints) which toaether specify 1 computation.

Currently the most common way to represent relationships between standard forms (typically implementation/abstraction relationships) is via program transformations or program refinement rules [2). As compared to overleys, these formalisms have two serious problems which stem from their lack of neulralness between analysis and synthesis. (>.n overlay in tt]e plan calculus, as in Fig. 2, is made up of two plans and a set of correspondences between the parts of the two plans. Each plan represents a point of view; the correspondences express the relationship between the points of view. For example, in an Implementation overlay the plan on the right hand side is the abstract description and the plan on the left hand side is an implementation. It is important, however, that either plan can be used as the "pattern". In a typical program synthesis step using overlays the right hand plan is used as the pattern and lhe left hand plan is instantiated as a further implementation. Conversely, In a typical analysis step, the left hand plan serves as the patlern and the riaht hand plen is instantiated as 1 more abstract descrirlion. With both program refinement rules end knowledge­ based program lr anslormalions this sort of symmetric use is not possible since the right hand side of a transform.lion or refinement rule Is typically a sequence of substitutions or modifications to be performed, rather than 1 pattern.

A second problem stemming from the asymmetry of program transformations and refinement rules is their lack of verifiability. The correctness of an overlay in the plan calculus is verified by proving essentially that the the constraints of the plan on the left hand side, together with the correspondences (which ere formally a set of equalities between terms on the left and terms on the right) Imply the constraints of the plen on the right hand side. Neither Balzer's lrenslormation language nor Green and Barstow's refinement tree notation has been adequately formalized to permit

the question of correctness to be addressed. The recent work of Broy and Pepper [4] is an improvement in this direction, since their transformations have program forms on both the left and right hand sides, with associated proof rules. Unfortunately, they use program schemes as the representation of the standard forms which has the difficulties discussed above.

Another formalism some have· found atlr active lor codifying progf'amming knowledge is formal grammers. For example, Ruth (30] constructed a grammar (with global switches to control conditional expansions) which represented the class of programs expected to be handed as exercises in en introductory PL/1 programming class. This grammar was use·d in a combination of top-down, bottom-up and heuristic parsing techniques in order to recognize correct and near-correct programs. Miller and Goldstein [22] also used a grammar formalism (implemented as an augmented transition network) to rept'esent classes of programs in a domain of graphical programming with slick figures. The major shortcoming of these grammars from the point of view of the programmer's apprentice is their lack of a clear semantics upon which a verification methodology can bP b"sed.

3. A Situational Calculus

Before defining the plan calculus more formally, we first need to introduce the underlying logical foundations using a sitvelion111 calculus similar to the one developed by Green [13] and used by McCarthy and Hayes [20). A situational calculus is a variant of predicate calculus in which certain variables and constants are Interpreted as denoting situations. Situations can be thought of Informally as "instants in lime" or "stales of the world~.

1. As opposed to the folding-unfolding and similar transformations of Burstall and Dar1ington [5] which are intended to be a small set of very general tr anslormations which are formally adequate, but which must be composed appropriately to construct intuitively meaningful implementation steps.

Side Effects

One basic issue to be addressed in the logical foundations of the plan calculus is the description of mut11ble objects. In programming, as in the everyday world of physical objects, objects can change their behavior (or properties) over lime without changing their identity. The approach taken by Green to this problem was to add an extra situational variable to the various function and relation symbols which described the lime-dependent aspects of objects. So for example, lor a mutable set A he would write member(x,A,s) to assert that x is a member of A at lime s. At some other lime I ,s, it then might be the case . that ~member(x,A,t). We then say that A has been modified or that a side effect has occurred.

This situational notation becomes awkward, however, when one 'introduces defined relationships between objects. For example, suppose we wish to assert that between situations s and t some elements may have been removed from set A, but none have been added. The appropriate relation to use here is subset. In Green's approach we are forced to define subset as follows, adding two situational arguments :

subsei(A,B,s,t) = Vx [ member(x,A,s) => member(x,tJ,t) ]. We then would then assert subsei(A,A,I,s) to specify the indicated side effect.

This paper proposes an alternative situational calculus which allows us to preserve the standard algebra of set relations. Mutable objects are treated forma~y here as functions from situations to behJJviors. Behaviors are mathematical domains, such as sets, In which there are no side effects, i.e. in which an axiom of extensionality similar to the one for sets applies. 1 A mutable set, such as A, is then formally a function from situations to sets. So for example we could write

A(s)-{1,2,3) A(t)·{ I ,2) where s,.t. and A(t)~A(s) to specify the side effect discussed above.

This is the most straightforward example of specifying side effects. Additional complexity enters in when side effects are combined with hierarchical objects (objects with objects as parts) and multiple points of view. The representation of such side effects in the situational calculus in these more complex cases will be touched upon slightly in the upcoming sections on data plans and overlays. These topics are treated in detail in [28) Shrobe [34] also dis~usses some techniques lor reasoning about such complex side effects.

Control Flow

In addition to distinguishing the different behavior slates of mutable objects, situations can be used to represent control information. This is achieved formally by introducing a'primilive partial order on situations, called Precedes. Intuitively, this relation captures· the notion of sleles occuring before or elter other slates. This relation also makes it possible to talk ebout cyclic computations in which all objects return to the same slate as at some earlier lime.

Another basic feature of control flow we need to deal with in the situational calculus is conditionals. To do so formally, we introduce a distinguished constant ..1. into the domain of situations, such that Vs precedes(s,_L) .

Intuitively, ..1. represents a situation which is never reached. As we shall see in the following section, ..1. appears in the axioms for tests as a way of saying that the two branches of a test are mutually exclusive. ..1. also gives us. the power lo talk about the termination of a loop.

Coonputations

Given objects and situations, we cen by induction construct a domain of n-tuples (and n-tuples of n-tuples) in which the base components are objects and situations. We call each such n-luple a computation. So for example, the 3-luple <A,s,l> is a computation involving the object A and situations s and I. If the assertions given in the example above for A, s and I hold, then this computation involves a side effect to the mutable set A.

1. The axiom of extensionality for sets states that two sets ere equal if and only if they have exactly the same members.

As we shall see in the next section, a plan is formally a predicate on computations (with the syntactic variation of referring to the components of an n-tuple by selector funclions rather than by numerical index).

4. Plans

We are now in a position to give a formal definition of the plan calculus. In doing so, it is important to dist inguish three levels of definition :

(i) Plan Diagrams.

This is the diagr ammatic notation illustrated in Fig. 1 and Fig. 2. Historically this was the first level of the plan calculus to be developed and is still the notation which !s used most by the author for intuition and explanation. It is also the abstract "mental language" of the programmer's apprentice, i.e. the most natural language in which to describe its operat ions and strategies. (There of cour se also has to be a concrete implementation of this language In computer memory, as discussed below).

(ii) Formal Semantics.

A systematic method is given to translate each form of plan diagram into the axiomitization of a predicate in the situational calculus. This axiomat ization provides the rules of inference on plans, verifiability and additivity (combination of plans has the same formal properties as union of axiom systems). Note also that lor presentation purposes the actual formulae associated with some constraints in plans will often be omitted from plan diagrams, and the existence of a constraint just indicated by an arc between the constrained parts.

(Iii) Implementation.

Several different representations of the plan calculus as Lisp data structures have been implemented and used by the author, Shrobe and Waters. Two early versions of the implementation used a general purpose fully inverted assertional data base with pattern matching (similar to the one used in Conniver [21 ]) in which a separate assertion was stored to represent each feature (box, arrow, etc.) of a plan diagram. A subsequent re-implementalion by Waters optimized this data base by providing specific access paths tailored to the specific assertion types and pattern matching that was required by the current programmer's apprentice system. Most recently a third version was implemented using McAIIesler's truth maintenance system [ 19] in which the logical axioms are represented explicitly with a.dditional extra-logical annotation to encode the diagram level information. The implementation level will not be discussed further in this paper, other than to show the external lisp form in which plan definitions are entered in the most recent version.

The basic idea of a plan, as used in the programmer's apprentice, comes from an analogy between programming and other engineering activities [26]. "Plans" of various kinds are used by many different kinds of engineers. For example, an electrical engineer uses circuit diagrams and block diagrams at various levels of abstraction; a structural engineer uses large-scale and detailed blue prints which show balh the architectural framework of a building and also various subsystems such as heating, wiring and plumbing; a mechanical engineer uses overlapping hierarchical descriptions of the interconnections between mechanical parts and assemblies.

Programming is viewed here as a process involving the construction and manipulation of specificat ions at various levels of abstraction. In this view, there is no fundamental distinctio" between specifications and programs. A program (e.g. in Lisp) is merely a specification which is detailed enough to be carried out by some particular interpreter. This view is consistent with the current trend in computer science towards wide spectrum languages. The advantage of this approach is that various parts of a program design can be relined to different degrees without Intervening shifts of formalism.

The current plan calculus is based on a very simple model of computation (some limitations of this model and possible future extensions are discussed in the conclusions section). In this model all computations are composed out of three types of primitives : operations, tests, and primitive data objects. Corresponding to each of these primitive types, there is a primitive specification form in the plan calculus. Opera-lions are specified by input-output specifications (preconditions and postcondilions). Tests are specified by a condition on the inputs which determines whether the lest succeeds or fails. Primilive.dala objects are specified an appropriate mathematical theory, such as numbers, sets or functions.

Plans are composite specifications constructed by the uniform mechanism of defining parts (called roles) and constraints. Two kinds of plans are distinguished according to the types of the roles . Data plans specify data structures whose roles are primitive data objects or other data structures. Data plans thus embody a kind of data abstraction.

Temporal pltms specify computations whose paris . are operations, tests, data structures or other composite computations. The plan lor a search loop in Fig. I is an example of a temporal plan. In addition to arbitrary logical constraints between roles, temporal plans also include data flow and control flow constraints. Temporal plans thus embody a kind of control abstraction. Since temporal plans can have embedded data plans, and the same compositional mechanism is used lor both, control and data abslr action are unified in the plan calculus. The following sections describe the diagrams and formal semantics lor each kind of plan in detail.

Input-Output Specilie~tions

In plan diagrams an input-output specification is drawn as a solid rectangular box with solid arrows entering at the lop and leaving the bottom, as shown in Fig. 3. Each arrow entering al the top represents an input; each arrow leaving the bottom represents an output . Conslr ainls between inputs (preconditions) and between outputs and inputs (poslcondilions) are usually omitted in plan diagrams.

The definition of Set-add in the external formal of the current data base implementation is shown in Fig. 3 next to the diagram. Set-add has two inputs : Old (constrained to be a set) and Input (which may be an objecl of any type); and no other preconditions. The only output of Set-add is named New (a set). The postconditions of Set-add specify that the New set has exactly the same members as the Old set, with the sole addition of the Input. In terms .of its semantics, this input-output specification is translated Into a type predicate on computations, Set-add, dell11ed as shown below. 1

Set-add(a) = [ precedes(in(a),out(a)) " co-occur(in(a),out(a)) " set(old(aXin(a))) " set(new(aXout(a))) 1\ member(input ,new(aXout(a))) 1\ VK [ member(K,old(aXin(a))) :> member'(K,new(aXout(a))) ) , , VK [ member(K,new(aXout(a))) 1\ K~inpul :> member(K,old(aXin(a))) ) )

Note that each input and output name becomes a function symbol which is the selector function for a .component . of a computation. Such functions are called role funcltons. Thus mpul­ output specifications (and also tests), although introduced as primitive above, are in fact composite from the slandpomt of the formal semantics. Input and oulpul names are treated lhe same as role names in other composite plans.

Note two role functions in the definition above, In and Out, .vere implicit in the DEf IOSPEC form. These are situational roles which correspond inlulively to the situations immediately preceding and immediately following lhe e~eculion of the specified operation. The constraint between them is that the In situation precedes the Out situation, and that they co-occur . Co-occur is an equivalence on situations which is defined as follows.

Co-occur(s,tl = [ s·...L. +-+ I· ...l. )

This means that if the In si tuation i& reached, it follows that the Out situation is reached, i.e. the operation terminate's; and conversely, if the In situation does not occur (i.e. s·...L.), then the Out situation does not occur . This converse implication, together with the axiomilizalion of tests shown in the ne~l section, guarantees that none of the situations which follow in control flow from the failure side of a lest occur .

Finally note the lerms old(aXin(a)) and new(aXout(a)) in the definition' of Set-add. Input and output role functions return objects which must be applied to the appropriate silualional arguments to I alk about their behavior .. Thus Ofd and New are mutable sets; however this specification makes no commitment as to whether or not the Input object is added by side effect. (Note that we don't care about the ·behavior of the Input object here, only its identity.) Whether or nol a side effect is allowed depends on the larger plan in which a particular use of Set-add appears, specifically on whether the Old set is used again alter the operation. Formally, the specification of the side effect comes down to the question of equality between the Old and New objects. So for example, a specialized form (the specialization mechanism used here will be e~plained further below) of Set-add can be defined by adding one more simple ppslcondilion which stipulates that the addition be achieved by side effect.

(DEF IOSPEC IMPURE -SEf , ADD SPECIALIZATION SET-ADD (OlD INPUT) (NEW) () ((· OLD NEW)))

The me-aning of this definit ion is shown oelow. Note that Nhelher or not the role function is to be applied to a situational argument is encoded in the data base input notation by the presence or absence of parentheses around the role name in the constraint e~pression .

lmpure-sel-add(a) = [ set-add(a)" old(a)· new(a) )

Test Specifications

In plan diagrams a lest specification is drawn as a solid reel angular box with a divided boll om part, as shown in Fig. 4. The inputs and outputs of a test specification and their types are indicated in the same way as the inputs and outputs of an input­ output specif.ication. A lest also has preconditions and poslcondilions, just like an input-output specification. A lest specification differs from 1n input -output specification in that two distinct output situations, named Succeed and Fail, 1re implicitly specified. Which one occurs depends on whether or not a given relation (called the condition of the test) holds true between the Inputs. Control flow arcs originating from either the part of the test box marked S (lor succeed) or the part marked F (lor fa11l are then used to indicate which other parts of a plan are e~eculed depending on the les1. 1

The definition of the test specification Apply-predicate wrillen in the formal of the current data base implementation is also shown in Fig. 4. Note that this is the lest specification used in the Found role of the Search-loop plan of Fig. I . The two ex1l roles of Fig. 1 illuslr ale joins which ar.e the mirror. images of tests in the plan calculus. Joins are reqUired m cond1llonal plans to spec1fy what the output is in each case.

Apply-predicate has two inputs : Criterion (a _Predicate) and Input (any object to which the predicate is applicable); and no outputs. The lest succeeds when the Criterion is true of the Input; otherwise it fails. In terms of its semantics, this lest specification is translated into a type predicate on computations with three situational roles, In, Succeed and Fail, as shown below.

Apply-predicate(a) = [ precedes(in(a),succeed(a))" precedes(in(a),fail(a)) 1\ mutex(succeed(a),f~il(a)) 1\ predicale(criterion(a)) " member(inpul(a),domain(crilerion(aXin(a)))) " [ apply(crilerion(aXin(a)),inpul(a)) . :> co -occur(in(a),succeed(a)) ) 1\ [ ~apply.(crileriOfl(aXin(a)),inpul(a)) :> co-occur(in(a),fail(a)) ) )

IIAulex(s,l) = [ s·...L. v I·...L.)

From this way of defining tests it is possible to reason both backward and forward in lime. For eXImple, if lhe In situation is reached (i.e. in(a),l ...L.) and the Criterion Is true, then it follows that the Succeed situation is reached. Conversely, if we know thai the either the Succeed or Fail situation is reached, it follows that the In situation must have been reached.

Data Plans

Data plans are plans whose roles are primitive data objects or other data plans. In plan diagrams primitive data objects are drawn as solid ovals; data plans are drawn as dashed ovals. Data plans are used to represent standard data structure configurations which may be used in the implementation of more abstract data types. For example, the data plan lnde~ed-Sequence, shown in Fig. 5, represents the common cliche of a sequence (typically implemented more concretely as an array) with an associated index pointer . This configuration is typically. used to implement such things as buffers, queues, and slacks. (Implementation relationships are represented using overlays, which will be tfiscussed further in an uocoming section.)

The plan Indexed-sequence has two roles : Base (I sequence)

F'laure 4. Test Specification for Applyin1 1 Pradiuta.

(DEFTEST APPLY-PREDICATE ((CRITERION PREDICATE) INPUT) () ((MEHlER INPUT (DOMAIN (CRITERION)))) () (APPLY (CRITERION) INPUT)) ; Inputs ;outputs ;precondlt Ions ;pos tcondlt Ions ;ttst condition

1. More complicated tests with more than two cases can be represented by composing binary tests. Alternatively, lhe lest notation may be generalized to more than two case·

and Index (an Integer); and the constraint that the Index is between zero and the length of the sequence. The definition of Indexed-sequence in the external format of the data base is also shown in Fig. 5.

Data plans as a mechanism for data abstraction are similar in certain ways to to algebraic axioms [14,12) ·and abstract data types (17). The constraints between roles of a data plan are similar to what Is called the invariant in either formalisms. From this point of view, the semantic translation of a data plan can be thought of as a data type predicate. For example, Indexed­ sequence, Is defined as shown below.

lndexed-sequence(B) =

Vs [ sequence(base(3Xs)) 1\ lnleger(index(BXs)) " gl(index(3Xs)10) " le(index(BXsl,lenglh(base(BXs))) )

Algebraic uioms and abstract data types, however, do not allow one to specify side effects on data structures -- all operations are purely functional. In the plan calculus, we single out the primitive selector operations of the data abstraction, which become the role functions. Side effects are then specified in terms of changes to the roles of a data structure. Note that Indexed­ sequence is defined as a predicate on behaviors not objects, i.e. I above is meant to denote a 2-tuple with components named Base and Index. A mutable indexed sequence is an object 0 such that, for eKample, O(s)·5. Aspects ·of this formalization of mutable data structures ate similar to the approaches taken by Earley [9), by Reynolds [24) for reasoning about arrays, and by Gullag and Horning [15).

The plan calculus also represents sharing (i.e. aliasing) In composite data objects, which is not the case with algebraic axioms or abstract data types. Space does not allow a full treatment of this topic here (see [28]); the basic. Idea is that the parts of a composite data object can themselves be data objects, e.g. base(O(s)) above is a mutable sequence. In this formalization 1 side effect to base(O(s)) logically propagates to O(s).

Temporal Plans

Temporal plans are the most general form of plan, in which both data and control abstraction can be expressed. The roles of a temporal plan may be either primitive data objects, data plans, Input-output specifications or test specifications. The most typical constraints between input-output and test specification roles are data flow and control flow constrainis. An example of the diagram for a temporal plan is shown in Fig. 6 (note that Fig. I earlier also Illustrates a temporal plan).

The Bump+update plan in Fig. 6 has four roles: Bump, a subtract one operation; Update, an operation to change one term In a sequence; and Old and New, which are indexed sequence data structures. This plan captures the cliched pattern of operations on an indeKed sequence in which the index is decremented and a new term is stored. (Among other things, this is the implementation of 1 Push operation if the Old and New indexed sequences are viewed IS slacks -- see section on overlays).

Solid arrows in a temporal plan diagram, such as between the

Ftaure 5. Data Plan for an Indexed Sequenca.

Output of the Bump step and the Index input of the Update· step, denote data flow, i.e. the Output of Bump becomes the Index input of Update. This notion of data flow is intuitively one of the main sources of additivity in the plan calculus. An arbitrary amount of other computation may be added between Bump and Update as long as the stipulated data flow is not disturbed. As we shall see below, data flow constraints are formalized loglc~lly as equalities between terms .. which denote the respective input and output ports. The additional solid lines in Fig. 6 denote equality constraints between parts other than the input and output ports of Input-output specifications. For example, the Base of the Old lndeKed sequence becomes the Old sequence input to the Update step; the Base of the New indexed sequence is the New sequence output <?f the Update step.

A second feature of temporal plan diagrams inlro.duced in Fig. 6 is control flow (cross-hatched) arrows. The control flow arrow between Bump and Update means that the termination of the Bump step precedes (and implies) the initiation of the Update step. The eKternal plan definition form for Bump+Update given in Fig. 6 summarizes all of these features. Also shown below are the input­ output specifications of the Subtract -one and Newterm, which are straightforward.

(DEfiQSP£C SUBTRACT-ONE ((INPUT INTEGER)) ( (OUTPUT I NTEG£R)) () ((· (OUTPUT)(- (INPUT) 1)))) (DEFIOSPEC NEWTERM ( (OLD SEQUENCE)( INDEX INTEGER) INPUT) ( (NEW SEQUENCE)) ((&T (INOElC) O)(LE (INDEx)(LENGTH (OLD)))) ((· (LENGTH (NEW))(UNGTH (OLD))) (· (TERM (NEW)(INDEX)) INPUT) (fORALL I (IMPliES (NOT (· I (INDEX))) (· (TERM (OLD) I)(T£RM (NEW) I))))))

There are two further features of the Bump+updale plan to note before looking at the semantic translation. First, like Set-add

Flaure 6. Temporal Plan for Updalin& an Indexed Sequence.

this plan makes no commitment to whether or not a side effect is Involved. A specialized version of Bump·update can be specified In which the Update step is specialized to an impure Newterm specification and in which the Old and New Indexed sequences ue constrained to be identical. Also note that the Input to Newlerm (the value of the new term) Is not constrained in this plan. Temporal plans are typically combined by providing data flow from and to such ports.

Shown below is the semantics of the temporal plan Bump· update which is defined, similar to input-output and test specifications, as a predicate on computations.

Bump·update(a) =

[subtract -one( bump( a)) " newterm(update(a))

" cflow(out(bump(a)),in(update(a)))

" output(bump(a)Xout(bvmp(a))) ·index(update(a)Xin(updale(a)))

1\ ]s [ indexed-sequence(old(aXs))

" index(old(aXslXsl·input(bump(a)Xin(bump(a)))

• " base(old(aXslXs)·old(update(a)Xin(update(ci))) ]

1\ ]f [ indexed-sequence(new(aXt))

• " index(new(aXflXfl· output(bump(a)Xout(bump(a)))

1\ base(new(aXtlXtl · output(update(a)Xout(update(a)))]]

Cllow(s,t) = [ precedes(s,t) " co-occur(s,l) ]

The interpret at ion of this formal definition is left largely to the reader . The major complexity in translating temporal plans into their logical equivalent is in providing the appropriate situational arguments. In particular, for roles which are data plans, such as Old and New above, we posit the existence of some situation (e:g. s and t above) in which the constraints of the data plan hold, and then assert constraints between the behavior of the parts in that situation and the input and output .ports to . which they are connected in the plan diagram. The default situational arguments for Input and output ports here are assigned the same way as in the corresponding input -output specifications, namely In for input objects and Out for output objects.

The Bump·update plan does not illustrat~ an additional important feature of temporal plans, namely the use of recursion to represent loops. Recent work on Lisp interpreters [35] and compilers [36] suggests that the distinction between loops and singly recursive programs in which the recursive call is the last step of the program (so called "tail recursions") should be considered only a superficial syntactic variation. The plan calculus takes this point of view. Recursion in plan diagrams (data plans may also be recursively defined) is indicated by a spiral line as shown in Fig. 1, the plan for a search loop, introduced earlier.

Pro&rammin& lan&uages

The plan calculus makes it possible to build a progremmer's apprentice which is concerned with the sy~tactic details of different programming languages only at its most superficial Interface. In order to translate back and forth between a given programming language and the plan calculus, the primitives of the programming language are divided into two categories :

(I) The primitive actions and tests of the language, such as CAR, CDR, CONS, NUll and EQ in Lisp, are represented as input-output specifications and lest specifications.

(ii) The primitive connectives, s4ch as PROG, COND, SETQ, GO and RETURN in lisp, are represented as patterns of control and data flow constraints between operations and tests.

The translation from standard program text to an equivalent plan representation has been implemented for reasonable subsets of lisp [25], Fortran [39) and Cobol [10]. The tr~nslation from suitably restricted plans to Lisp code has also been implemented by Waters [ 40].

5. Relations Between Plans

Fig. 7 is a small excerpt from the current plan library which illustrates the the taxonomic structure of the libr~ry . A· first observation to make about the nodes of the library shown ih this example Is that they are a mixture of both data abstractions (e.g.

set, predicate, directed graph) and control abstractions (Find and Thread-find are input -output specifications, and in gener at there are temporal plans also).

The four types of relations which relate nodes of the library are named in the upper right hand comer of the figure next to an example of the type of line or arrow used to represent each relation In the body of the figure. The first relation, component, simply indexes which plans are used in the definition of other plans, as for example Indexed-sequence was used in the definition of Bump·update above. The next two relations are simple inheritance relationships by which a plan inherits the roles and constraints of another plan and then adds its own additional roles or conslr·ainls or both. Specialization is the relation in which only constraints are added; extension involves adding roles (and usually, constraints between the new roles and the inherited ones).

Overlays are the most important type of relation between plans In the library bec~use overlays represent significant additional knowledge, such as the details of how .. me abstraction may be Implemented in terms of another . The diagram notation and semantics for- overlays are explained in the following section.

Starling with Set in Fig. 7, a typical question we might want to ask in the course of program analysis or synthesis is: what plans (e.g. Input-output specifications) are there in the library which use sets? This type of question is answered in general by looking up the composition relation; in this example from Set. to Find. Find is an input-output specification with three roles : an Input set, a Criterion predicate and an Output object; its precondition is !hal there exist an element of the Input set which satisfies the Criterion; its postcondition is that the Output is such an element.

Overlays pointing to a node answer questions of the form: what implementations are available for Find operations? In this example, one answer is that Find may be implemented as Thread­ find, where the Input set is implemented as a thread. (Note that Thread is a specialization of Directed-graph in which each node has at most one predecessor or successor and there are no cycles.) The input-output specifications of Thread-find are shown below. II has three roles similar to Find : an Input thread, a Criterion predicate and an Output object; its precondition is that there exist a node of the Input thread which satisfies the Criterion; its postcondition is thai the ·Output is such a node.

(DEFIOSPEC THREAD-FIND ((INPUT THREAD)(CRITERION PREDICATE)) ( OUT.PUT) ((EXISTS X (AND (NODE (INPUT) X) (APPLY (CRITERIOII) X)))) ((NODE (INPUT) OUTPUT) (APPL:Y (CRITERION) OUTPUT)))

Fln·lly, extension Is 1 relallo~ between plans which can be used to access useful variations of a plan. For example, in the fiaure an extension of Thread-find is Internal-thread-find. The Input-output specifications of lnler'1al-thread-find are shown below.

( OEF JOSPEC INTERNAL · THREAD· f JND EXTENS JON THREAD · f JND (INPUT CRITERION) (OUTPUT PREVIOUS) ((NOT (APPLY (CRITERJON)(ROOT (INPUT))))) ( (SUCCESSOR (INPUT) PREVIOUS OUTPUT)))

Note that an additional output role, Previous, has been added with the constr aint that it be the predecessor of the Output node In the Jnput thread. This is a very common kind of operation on directed graphs when spl icing of, nodes in and out is being performed. In order to be used properly, Internal-thread-find must also have the addit ional precondition (from which its name is suggested) that the Criterion is false for the root node of the Input thread.

Overlay·

Overlays provide a mechanism in the plan calculus for representing the relationship between two different points of view, each of which is represented by a plan. Overlays are similar to Sussman's "slices" [37], which he uses to represent equivalences in electronic circuit analysis and synthesis. Formally, an overlay is a mapping from instances of one plan to instances of another . Such mappings are a very gener al mechanism; the Intuitive import of var ious overlays depends on what kind of plans are involved, whether the mapping is many-to-one or one-to-one, and how the mapping is def ined.

An example of an overlay between a temporal plan and an input-output specification is shown in Fig. 8. Intuitively, this overlay expresses how . a Push operation can be implemented by the Bump+updale plan discussed above, given that the slack is implemented as an indexed sequence. Note that the diagram for an overlay is made up of a plan on the left hand side (which is the domain of the mapping), a plan on the right hand side (which is lhe range of the mapping), and a set of hooked lines showing a set of correspondences between roles of the two plans (which defines the mapping). In the external formal of the current data base, an overlay is defined as follows.

(DEFOVERLAY BUHP+UPOATE>PUSH (BUHP+UPDATE PUSH)

(· (OLD PUSH) (JNDEXED·SEQUENCE>STACK (OLD BUHP+UPDATE))) (· (NEW PUSH) ( JNOEXEO· SEQUENCE>STACK (NEW BUHP+UPDATE))) (· (INPUT PUSH) (INPUT (UPDATE BUHP+UPDATE))) (· (IN PUSH) (IN (BUMP BUHP+UPDATE))) (· (OUT PUSH) (OUT (UPDATE BUHP+UPOATE))))

Notice that each overlay has a name, e.g. Bump+updale>push, 1 which will become a funct ion symbol in the formal semantics. Correspondences between roles are either simple equalities, as in

• (· (INPUT PUSH) (INPUT (UPDATE BUHP+UPOATE))) ,

which says that the Input to Push (the object which becomes the head of the new slack) corresponds to the Input of the Update step in the Bump+updale plah; or correspondences which def ined In terms of other overlays, as in

(· (OLD PUSH) ( JNDEXEO ·SEQUENCE>STACK (OLD BUHP+UPDATE)))

The overlay lndexed-sequence>slack is an example of a many ­ to-one overlay between data plans. The basic idea of this overlay Is that an indexed sequence may be viewed as the implementation of a slack In which the head is the term of the sequence indexed by the current index, and the tail js, recursively, the sequence with index one greater. The formal definition of this overlay will not be shown here, as it is very similar to what is called an abstraction function in abstract data types. The formal semantics of the Bump+updale>push overlay is the following function definition.

,!I·Bump+updale >push(a) =

[ old(IJ)-indexed-sequence>slack(old(a))

• " new(IJHndexed-sequence>stack(new(a))
• " inpui(IJ)-inpul(updale(a))
• " ln(IJ)-in(bump(a))
• " oui(IJ)-oul(update(a)) J

1. This symbol is intended to be read "Bump and Update as Push".

Implementation overlays such as Bump+updale>push and lndexed- sequence >slack are typically many-to-one. There are also one-to-one overlays in lhe library, which are naturally thought of as providing alternative points of view .or transformations of data or control structure. For example, a L1sp list can be viewed alternatively as a slack (i.e. a recursively defined data structure), as a labelled directed graph (in particular

a thread) wherein the nodes are Cons cells connected by the Cdr relation and labelled by the Car relation, or as a sequence wherein the i-th term is the Car of (i - l)lh Cdr .' Each of these data plans provides its own vocabulary for specifying properties of a data structure and a standard set of manipulations on it . There are one-to-one overlays in the library between them so !hal the appropriate point of view can be used dependin& on the properties and manipulations of interest. There are also one-to· one overlays in the library between temporal plans, such lhe overlay introduced earlier in Fig. 2 which captures the relationship in general between singly recursive prO&rams which accumulate "on the way down" (e.g. reverse copying a list) and those that accumulate "on the way up" (e.g. copyin& a list).

Other overlays of particular interest are those which map from temporal plans to data plans, in parlicular from recursive temporal plans to lists. These latter are called stream overlays and embody a kind of abslr action in which the objects filling a &iven role at all levels in a recursive plan are viewed as a sin&le data structure. For example, there is a stream overlay in the library by means of which the succession of Input's to the Found lest in the Search­ loop plan are viewed as a list ; and if that overlay is composed with the overlay to view a list as the implementation of a set, then Search-ioop can be viewed as the implementation of the Find specification discussed above. This method of abstraction provides a very powerful means of decomposing loops and recursions in a way which makes their behavior much clearer than the standard invariant assertion method. For a further discussion of this idea see Waters [39].

A final point to note regarding the use of overlays is that they are not only part of the taxonomic slruclure of the plan library, they are also used to construct the refinement tree of a particular program. This tree encodes the design history of a program at many levels of detail. A way in which overlays differ from other refinement tree notations is thai ovt:rlays permit overlapping implementations [29], where components that are distinct at one level of abstraction share parts at lower levels. This is a real feature of good engineering design and is an important way in which overlays are an improvement over previous notations.

6. Final Remarks

The emphasis in this paper on representation rather lhan reasoning has allowed no mention of an important dimension of lhe plan calculus. In the programmer 's apprentice, reasoning about plans lakes place within a system [1"9] which maintains explicit dependencies between each assertion in the data base. These dependencies are crucial lor support ing evolut ionary design and debugging of programs. Each overlay in the library has a pre­ compiled network of dependencies between the specifications on the left and right hand sides (called its teleological structure) which is instantiated along with lbe parts, constraints and correspondences when it is used.

There are several areas in which we have found the current plan calculus deficient and hope to extend it ·further in the fuklre . Important among these are the following :

• (i) Performance Considerations. A way of formalizing lime and space lrade-olfs is needed, both for the library and lor reasoning about particular programs.
• (ii) Error Handling. The non-local flow of control typically Involved in error handling code is not well represented in the current plan calculus.
• (iii) Glob11l Shared Data. Programs which communicate primarily by inserting and retrieving information in a global shared data base are not well decomposed by the data flow ideas in the current calculus . .

Finally, we intend to investigate the usefulness of the plan calculus in other planning contexts . In particular, I believe there is potential for a fruitful flow of ideas back and forth between program understanding (analysis, synthesis and verification) and robot planning (e.g. Abslrips [31 ]). Many of the insights underlying the plan calculus originate from work in robot planning;

I also believe some of the techniques developed in the plan calculus for representing and· reasoning about overlapping data structures and side effects have bearing on aspects of the classical "frame problem" [20] in robot planning.

Blblio&raphy

• (I I R. BAlZER, "TRANSFORMATIONAllt.lPlEMENTATION AN EXAMPlE", /fCC TRIWS. ON SOFTWAI?C CNG., VOL 7, NO. I , JANUARV, 1981.
• DR ·BARSTOW, "A.UTOMATIC CONSTRUCTION OF AlGORITHMS AND DATA STRUCTURES USING A KNOWLEDGE BASE OF PROGI!AMMING RULES" STANFORD AIM-308, NOV. I 977. '
• 131 S BASU AND J MISRA, "SO.ME ClASSES Of NATURALL V PROVABLE PROGRAMS", 2HD INT. CONF. ON.SOFTWARC CNG., SAN FRANCISCO CAL OCT , 1976 ' '
• M. BROV AND P PEPPER. "PROGRAM DEVELOPMENT AS A FORMAL ACTIVITY", /CCC TRANS. ON SOFTWARC CNG., VOL. 7, NO. I , JANUARY, I 980.
• [5) R M. BURST ALL AND J l DARLINGTON, "A TRANSFORMATION SVSTEM FOR DEVELOPING RECURSIVE PROGRAMS", J. OF THE ACM, VOL. 24, NO. I JANUARY, 1977. '
• TE. CHEATHAM, "PROGRAM REFINEMENT BV TRANS~ORMATION" 5TH INT CONF. ON SOFTWAR[ CNG., SAN DIEGO, CAL, MARCH, 1981 ' .
• [7) OJ. DAHL AND K. NVGAARO "SIMULA - AN ALGOL-BASED SIMULATION lANGUAGE", COMM. OF THC ACM, VOL 9, NO. 9, SEPTEMBER I 966, PP. 671 -678.
• [I) JB DENNIS, "FIRST VERSION Of A DATA FLOW PROCEDURE LANGUAGE", PROC. OF SYMPOSIUM ON PROGRAMMING, INSTITUT DE PROGRAMMATION, U OF PARIS, APRIL 1974, PP. 241-271.
• J EARLEV, "TOWARD AN UNDERSTANDING Of DATA STRUCTURES", COMM. OF THC ACM, VOL 14, NO 10, OCTOBER 1971 , PP. 617-627.
• I 10) G FAUST, "SEMIAUTOMATIC TRANSLATION Of COBOL INTO HIBOL", (M.S THESIS), MIT{lCS{TR-256, MARCH, 1981
• I II I Sl GERHART, "KNOWLEDGE ABOUT PROGRAMS A MODEL AND CASE STUDV", IN PROC. OF INT. CONF. ON RCLIABL f SOFTWARe, JUNE 1975 PP. ~~ '
• I 12) J A. GOGUEN, JW. THATCHER, AND E.G WAGNER, "AN INITIAL ALGEBRA APPROACH TO THE SPECifiCATION, CORRECTNESS, AND IMPLEMENTATION Of ABSTRACT DATA TVPES," CURRCNT TRCNOS IN PROGRAMMING MCTHODOLOGY, VOL. IV, <ED RAVMONO VEHl, PRENTICE-HAll, 1978.
• I 13) C. GREEN, "THEOREM PROVING BV RESOLUTION AS A BASIS FOR QUESTION-ANSWERING SYSTEMS, MACHIN£ INTCLLIGCNCC ~. D. MICHIE AND B. MELTZER, EOS , EDINBURGH UNIVERSITY PRESS, EDINBURGH, SCOTLAND ~~~ '
• [ 14) J GUTTAG, "ABSTRACT DATA TVPES AND THE DEVELOPMENT OF DATA STRUCTURES", COMM. OF THE ACM, VOL 20, NO 6, JUN£ I 977, PP 396-404
• I 151 J GUTTAG AND J J HORNING, "FORMAl SPECIFICATION·AS A DESIGN TOOL", 7TH ANNUAL ACM SYMPOSIUM ON PRINCIPLCS OF PI?OGRAMMING LANGUAGES, LAS VEGAS, JANUARV, 1980, PP 251 -261
• [ 16) B liSKOV CT. AI., "ABSTRACTION MECHANISMS IN CLU", COMM. OF THC ACM, VOL 20, NO 8, AUGUST 1977, PP 564-576
• I 17) B H LISKOV AND S N ZlllES, "AN INTRODUCTION TO FORMAL SPECifiCATIONS OF DATA ABSTRACTIONS," CURRCNT TRENDS IN PROGRAI.II.IING I.ICTHOOOLOGY, VOL. I, <ED RAVMONO VEHI, PRENTICE-HAll, 1977.
• I II) l MANNA, MATHCMATIC THCORY OF COMPUTATION, MCGRAW-HILL, 1974 (19) D.A MCALLESTER, "AN OUTLOOK ON TRUTH MAINTENANCE", MIT/AIM-551 , AUGUST, I 980
• J MCCARTHY AND P HAVES, "SOME PHILOSOPHICAL PROBLEMS fROM THE STANDPOINT Of ~RTIFIC IAL INTELLIGENCE", MACHINE INTWIGENCC ~. 0 MICHIE AND B IAH TZER, EOS , EDINBURGH UNIVERSITY PRESS. EDINBURGH, SCOTLAND, I 969
• [21) 0 MCDERMOTT AND G J SUSSMAN, "THE CONNIVER REFERENCE MANUAL", MIT /AIIA-25911, 1973
• [22) M l . MILLER AND I GOLDSTEIN, "PROBLEM SOLVING GRAMMARS AS FORMAL TOOLS FOR INTELLIGENT CAl", PROC. or THC ASSOC. FOI? COMPUTING MACHINCRY, I 977
• J MISRA, "AN APPROACH TO FORMAL DEfiNITIONS AND PROOFS OF PROGRAIAMING PRINCIPLES", ICfE TRANS. ON SOFTWARC CNG., VOL SE-4, NO. 5, SEPTEMBER 1978, PP 410-413
• J C REYNOLDS. "REASONING ABOUT ARRI\VS", COMM. OF THC ACM, VOl 22, NO. 5, MAV 1979, PP 290-298
• 12!11 C. RICH AND HE SHROBE, "INITIAL REPORT ON A LISP PROGRAMMER'S APPRENTICE ", <1.4 S THESIS I, MIT /AI/TR-354, DECEMBER I 976
• C. RICH, HE SHROBE, RC. WATERS, G J SUSSMAN, AND C E HEWITT, "PROGRAIAIAING VIEWED AS AN ENGINEERING ACTIVITY", (NSF PROPOSAL), MIT/AIIA-459, JANUARV, 1978
• C RICH, HE. SHROBE, AND RC WATERS, "AN OVERVIEW OF THE PROGRAMIAER'S APPRENTICE", PROC. OF 6TH INT. XJINT CONF. ON ARTIFICIAL INTCLLIGENCC, TOKVO, JAPAN, AUGUST, 1979
• C. RICH, "INSPECTION METHODS IN PROGRAMMING", MIT{AI{TR-604, (PHD ·THESIS), DECEIABER, 1980
• C. RICH, "MULTIPLE POINTS Of VIEW IN MODELING PROGRAMS", PROC. or WORKSHOP ON DATA ABSTRACTION, DATA BASCS AND CONCCPTUAL MODCLING, ACM SIGPLAN NOTICCS, VOL 16, NO. I, JANUARV, 19&1, PP. 177-179
• G RUTH, "ANAL VSIS OF ALGORITHM IMPLEMENTATIONS", MJl PROJECT lilAC TECHNICAL REPORT I 30, (PH 0 THESIS I, 1973
• 131 I ED SACEROOTI, "PlANNING IN A HIERARCHY Of ABSTRACTION SPACES", ARTIFICIAL INTELLIGCNCC, VOL 5, NO 2, 1974, PP 115- 135
• J.T. SCHWARTZ, "ON PROGRAMIAING", AN INTERIM REPORT ON THE SEll PROJECT, COURANT INSTITUTE OF MATHEMATICAL SCIENCES NEW VORK UNIVERSITY, JUNE 1975. '
• [33) M SHAW, WA WUlf , AND R L lONDON, "ABSTRACTION AND VERifiCATION IN AlPHARD DEFINING AND SPECifYING ITERATION AND GENERATORS", COMM. OF THC ACM, VOL 20, NO. 8, AUGUST 1977, PP 553-563.
• HE. SHROBE, "DEPENDENCY DIRECTED REASONING FOR COMPLEX PROGRAM UNOERSTANOING", .(PHO THESIS), MIT{AI{TR-503, APRIL 1979
• Gl: STEELE AND G J SUSSMAN, ·THE ART Of THE INTERPRETER, OR, THE MODULARITY COMPLEX <PARTS ZERO, ONE, AND TWOI, MIT{AIM-453 MAV 1978 '
• Gl. STEElE, "RABBIT A COMPILER FOR SCHEME (A STUOV IN COMPILER OPTIMIZATION)", IAIT{AI{TR-474, MAV, 1978
• 1371 G.J. SUSSIAAN, "SLICES AT THE BOUNOARV BETWEEN ANALYSIS AND SYNTHESIS", ARTIFICIAL INTCLLIGCNCC AND PATTERN RCCOGNITION IN COMPUTCR AIDCD DESIGN, LATOMBE, EO , NORTH-HOLLAND, 1978
• I31J R.C. WATERS, "AUTOMATIC ANALYSIS Of THE LOGICAL STRUCTURE Of PROGRAMS", MIT{AI/TR-492, <PHD THESIS!, DECEMBER, 1978.
• RC. WATERS, "A METHOD FOR ANALYZING LOOP PROGRAMS", ICCf TRANS. ON SOFTWARe CNG., VOl SE-5, NO. 3, MAV 1979, PP. 237-247
• R.C. WATERS, "A KNOWLEDGE BASED PROGRAM EDiTOR", PROC. or 7TH INT. JOINT CONF. ON ARTIFICIAL INTCLLIGCNCC, VANCOUVER, CANADA, AUGUST 1911 '
• T. WINOGRAD, "BREAk THE COMPlEXITY BARRIER (AGAIN)", PROc. OF THE SIGIR-SIGPUW INTCRFACC MCCTING, NOVEMBER, 1973
• N. WIRTH, SYSTCMATIC PROGRAMMING, AN INTROOUCTION PRENTICE-HAll 1973. ' ·