A Method for Automatically Analyzing Programs

1. Introduction

This paper presents a method (described fully in [21)) for an11lyzing programs. This analysis of a progarm results in a "plan" for the program which represents the underlying logical structure of the program. ·The analysis method is based on the observation that programs are buill up in a small number of stereotyped ways referred to as plan building methods (PBMs).

An impor tant appl ication of PBMs is that they can be used to an~lyze a loop in a way which makes it easier to understand what the loop does and why. Sect ion 2 shows why this is a more useful analysi s than one based on basic structured progr amming constructs. Section 3 describes the PBMs in detail. Section 4 discusses how an analysis of a loop in terms of the PElMs c11n be used to guide a proof of correctness for the loop. It 11lso ~how~ why the resulting proof is more useful than a proof b a~ed on a single loop invariant.

An experiment is discussed in Section 5 which shows that the PBMs can be used to analyze a large class of programs. The experiment also shows that the pieces which result from the analysi~ are largely simple and easy to understand. A system (dt?scribed in Section 6) has been implemented which performs PBM analysis automatically. Section 7 discusses the relationship between the PBMs and current programming language cons tructs.

2. Desiderata For an Analysis Method

An analysis method views a program as built up out of parts, and makes it possible to understand the relationship between the oper ation of the program as a whole and the operation of its parts. From the point of view of gaining an understanding of a program, the parts are subproblems. Once the parts have been

This report describes research done at the Artificial Intelligence Labor atory of the Massachusetts Institute of Technology. Support for the laboratory's artificial intell igence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research

contract N00014-75-C-0643.

understood, their understandings can be combined in order to obtain an understanding of the whole.

There are several criteria which can be used to evaluate the usefulness of an analysis method. First, given a program, it should be straightforward to identify the parts. Second, the parts should be easier to understand than the whole. Third, the process of developing an understanding of the whole based on understandings of its parts should be as easy as possible.

The development which is most similar to PBMs has been the dt?velopment of structured programming constructs. Consider the loop progrclm in Figure 1. A naive approach to looking at how this program is logic~lly built up is b~sed on the idea that it is constructed on ~ line by line basis. Given this approach, it is easy to an~lyzc the prORram in order to break it up into its component p~rts (the six lines of the program). Further, the pMts are indeed much easier to underst~nd than the program as a whole. However, the problem with this approach is that it is not at all easy to discover what the program does once the parts are understood, because the interactions of the lines with e~ch other are complex.

I · 1:

z · 0:

LOOP: IF NOTIAIIl>0l THEN GOTO SKIP:

Z · Z-tAIIl;

SKIP: I a I + 1 : IF lsN THEN GOTO LOOP:

Figure I : An example program.

The b~sic structured programming constructs (composition, if - then-else, and do-while) suggest a much better analysis method. They indicate that the program should be viewed log1cally as being buill up hierarchically using these structured progr ~rnming constructs. Ficure 2 depicts the program in Figure I ~nalyzed in terms of these three basic structured programming constructs. The program is analyzed as being a composi tion of ·z~e· with an extended form of do-while which consists of counting from I to N in I and a body which is an if - then-else consisting of a predicate "A(I)>0" and a then clause

"Zr. Z+A(I)".

When it is possible without transforming a program, this is an easy analysis to perform. This is true whether or not the program is written in a syntactically structured way. II is po~.sible to write a program which cannot be analyzed in terms of the b<~sic structured programming constructs, unless it is first transformed to change the topology of its control flow. (An example of this is a program which contains a loop with 111ore than one entry point). However, a large number of programs can be directly analyzed in this way. In any case, the parts are easy to understand once they are isolated.

Let us now look at the structured programming oriented Clpproach in the light of how easy it is to develop an understanding of the result based on understandings of its pilrls. First consider if-then-else. If the parts are understood, then it is easy to get an understanding of the whole. Namely, in a given situation an if-then-else either acts like the then clause, or like the else clause, depending on the value of the predicate. In Figure 2 the if-then-else adds A()) to Z if A())>0. Composition is also an easy operation to understand. In general, these two structured programming constructs, whith describe non-looping programs, meet the criteria set forth above very well.

In contrast, consider the construct do-while in the light of f'.ow e<~sy it is to develop an understanding of the resulting program based on underslilndings of its parts. The body of the loop in Figure 2 can be understood as a conditional which adds A(l) to Z if A(l)>0. Unfortunately, it is not easy to go from this to an understanding !hill the loop Cldds the sum of the positive members of the first N elements of A to the initial value of Z. II is e<lsy to conclude this if an appropriate loop invariant can be found. However, in general, it is not easy to find such an invariant.

Another problem with the analysis in the figure is that the close relationship between the statements ·z~0· and "Z·Z+A(I)" is not made clear. In order to Clnalyze a program in such a way that things which <~re intimately related are closely linked together, these two statements should be put together in a single locality distinct from the rest of the loop. Having the statements spread through the loop makes it harder to understand that the program as a whole computes the sum of the positive members of the first N elements of A.

The diffiCulties with do-while stem from the way it looks at a loop. The body of the loop is first analyzed like any other straight-line program. This understanding of the body is then bootstr11pped up to an understanding of the loop as a whole. The problem is that this bootstrapping process is far from automatic. The PBMs for loops lake a different approach. They arP ba~rd on the idea that the body of a loop should not be Clni!lyzed in the same way as a straight-line program. Instead, they bre<~k the loop up in order to analyze it as built up out of stereot>·ped loop frilgmenls. (The lines "Z·0" and "Z·Z+A(I)" are an example of such a fragment.)

The PBMs for loops break the loop in Figure 2 up into four frC~gmenls CIS shown in Figure 3. The first fragment (A) counts up by one from one. It enumerates the sequence of integers ( 1,2, ... }. The second fragment (8) tests the sequence of integers produced by A and slops the loop when an integer greilter than N is found. This has the effect of truncating the sequence of integers to the sequence ( 1 ,2, ... N}. The third fr<~gment (C) oper<~tes on the trunc;~ted sequence of integers. It restricts the sequence by selecting only those integers which correspond to positive elements of the vector A. The last fragment (D) computes the sum of the elements of A corresponding to the integers in the restricted sequence produced by C. In the loop as a whole, the four. fragments are cascaded together so that the loop computes the sum of the positive members of the first N elements of A.

The key feature of the analysis above is that it breaks the loop apart Cllong a different dimension from the one used by an ;~nalysis in terms of do-while. There are two principle ;~dvantages to loohing at a loop in this new way. First, the loop is broken up into pieces which correspond to easily understood stereotyped fragments of looping behavior. Second, the way the pieces arc combined is logically equivalent to composit ion, which makes it eilsy to understand.

In order to make the idea that the fragments of Ike loop are composed together precise, the notion of a temporal sequence of values has been developed jointly by Howard Shrobe [ 19) and the author [21 ]. Given a program, such as a loop, which is repetitively executed, it can be useful to talk about the sequence of slates in which some part of the program is executed, and about the sequences of values available in those stiltes. For example, consider the statement "Z·Z+A(I)" in the loop in Figure 2. This statement is executed in a sequence of stC~tes. There are sequences of values of I, and Z which are C!Vailable in tho~e states. These sequences are referred to IJS temporal sequences of v;~lues. The insight is the realization that logici!lly, a temporal !.equence of values can be treated in the same way as any <~r,gregale data objet!. The concept of lazy ev;~luation [5, 8] uses the same insight going in the other direction. If an aggregate data object (such as a sequence of numbers) is desired, then it can be created temporally, rather thiln all at once, so that each piece of it is not actually created

until it is needed.

Looking back ;~t Figure 3, fragment A produces a temporal sequence of values of I. The elements of this sequence are tested by fragment C. Logic;~lly, the key relationship is that A creates data used by C. A is composed with C by passing lhis data from A to C. Viewed <~bstr;~ctly, it m;~kes no difference whether this datil is put into a vector which is passed all at once to C, or, as in the example, A and C are intermingled so that C can use each individual value created by A as soon as it is produced. Intermingling A and C is just an efficient way of implementing the data flow from A to C.

The key properly of composition which makes it an easy process to underslal)d is that the only interaction between two !hines which are composed together is that one passes data to the other. They have no other effect on each other. The loop fragments above have this key property. Fragment A will

produce a sequence of values of I counting up from ·me no matler what is happening in the rest of the loop. Fragment 8 tests the values of I it !.ees no matter what else is going on in the loop. As a result, each of the fragments can be understood completely in isolalron from whatever loop they are being used in. (Fragment 8 presents a problem because it controls the number of limes the other fragments are executed. In order to maintain the independence of the fragments in the face of this inle rt~clion, the descriptions of the fragments are prohibited from making any slt~temen!s about the· absolute number of elements in any temporal sequence of values. As a result, from thf' point of view of the descriptions, the fragments do not intert~cl because their interaction cannot affect anything in the descr ipt ions.)

3. !b~ Plan !;_3uilding Methods

Th1s section describes the len PBMs which have been developed. Figure 4 shows how the POMs are related. They are divided into two main groups. One group can be used to analyze str aight-line (non-looping) programs while the other group is used to analyze recursive programs and loops.

There are three basic straight-line PBMs: predicate, composition, and conditional. In addition, two special cases of composition are recognized: conjunction and expression. Figure 5 shows examples of segments of code which would be analyzed in terms of straight-line POMs.

predicate IF X<Y THEN GOTO Ll; ELSE IF Z<Y THEN GOTO L2; ELSE GOTO L3;

conditional IF X<0 THEN X·-X;

conjunction Z·COSIXI; W-SINIXI;

composition Z·FIRSTISORTIAII;

expression Z·SI N I COS lXII;

Figure 5: Examples of straight -line PBMs.

The PBM predicate is used to build up complex tests out of simpler ones. In the example, two two-way branching tests are combined into a three-way branching lest. The PBM conditional combines a lest with some act ions in order to construct a conditional expression. II is exactly analogous to the structured programming construct if-then-else.

The PBM composition is used to construct arbitrary non-branching sections of straight -line code. Two special cases of (Omposilion are recognized because they have part icularly useful logical properties. The PBM conjunction combines segments in such a way that there is no data flow between the segments. This means that the pieces are totally independent and can be understood completely in isolation from each other. II is particularly easy to understand what a conjunction does, bee a use the specific a lions for the conjunct ion as a whole are simply the conjunction of the specifications for the segments wh1ch have been combined.

With the PBM expre~sion, as with composit ion in general, there is data flow carrying the outputs of segments to the inputs of other segments. The PBM expression is more restricted than general composition in that the segments combined are requi red to have "substitutable" specifications. A specification is said to be substitutable if each output is described by a sinp,le assert ion of the form "oulpul=expression-involving-the-inputs". For exMnple the segment "COS" is described by the assert ion "output ~cos(inpul)". II is easy to understand what an expression docs, bee e~use substitution can be used in order to develop simple specifications for the expression as a whole.

In contrast to an expression, a general composition can combine segments with non-substitutable specifications. This me~kes it cumbersome to develop a description of what the result does. For example, in the composition in Figure 5, SORT might welt be descr ibed as producing an output which contains the same elements as the input, and in which the elements appear in i ncre<t ~.i ng order. This being the case, simple subst itut ion wilt not suffice to conclude that the composition as a whole computes the minimum element in the input. Some actual deduct ion is required.

It is very easy to analyze a straight-l ine segment of a program in terms of the straight-l ine PBMs because it is not possible to confuse an instance of one with an instance of another. This is due to the fact lhat there are only three be~sic PBMs (predicate, composit ion, and conditional) and the fact that they are completely different from each other. II should be noted that it is possible to write " straight-line progr e~m which is unstructured in that it cannot be analyzed in terms of these PBMs, or in terms of structured programming constructs, without first transforming the code.

The four PBMs which build up recursive structures embody the idea that recursive structures are buill up by composing together stereotyped fragments of recursive behavior in a way which is exactly analogous to the way non-branching straight-line segments of code are built up by composing simple segments together. For simplicity, the discussion below dP.scrihes the recursive PBMs solely in terms of loops. The .discussion in [21) shows how they apply to arbitrary singly r.elf-rccursive programs. Three of the recursive PBMs (augmente~tion, filler, and termination) construct loop fragments. The fourth one (temporal composition) combines fragments together.

The PBM augmentation combines an initial izat ion which is executed once with a body which is executed repet itively in order to create a loop fragment. The resulting fragment lakes in temporal sequences of values and produces temporal sequences of values. The name "augmentation" is derived from the fact that an augmentat ion can be added into a loop in order to ;~ugmenl its activities without affecting anything else the loop does.

n1a><

Z=very-small:

IF ~>Z THEN Zc~:

in it:

IJocly:

Fir,ure 6: E~ample augmentations.

Fi[~UrC' 6 ~how!. four different augmentations. Consider the !·CCOnd one "Z ~0; Z·Z+X;" which computes a sum. The variable X is underlined in order -to indicate that it stands for the place where the fragment receives a temporal sequence of values. II crC'<~Ies " corre!.ponding sequence of parti;~l sums in the variable Z. The behavior of an augrnenlalion can be s·traightforwardly described in terms of a recurrence relation derived from the inili;~liz;~lion and the body. For the summation fragment this recurrence relation is "ZJ =0 11 Zi+l KZi+Xi"· In situations where the recurrence relation has a simple solution, better !.pecificalions can be derived (such as "Zi'"lj=l,i-1 X( for the summation augmentation). A luge number of the augmentations seen in proer ams correspond to simple actions such as counting, summing, or calculating a m;~ximum. The count augmentation is interesting in !hat it does not ta~.e any temporal sequence of values as an input but rather simply generates a sequence of values. The feedback free augmentation is particularly easy to understand because is recurrence relation ("Zi~2tXj") does not refer to prior values of Z and therefore is trivially solvable.

Figure 7: An e~ample filter.

The PBM filter constructs a loop fragment from a test which is repeatedly e~ecuted. ' The fragment takes in a temporal !.equcnce of values and restricts the sequence by filtering out some of the values. In a loop, this action is realized by creating a restricted execution environment which is only executed on some of the iterations of the loop. The filler in the example I akes in a sequence of values of X and creates two outputs: I he sequence of negative values of X and the sequence of non-negative values of X.

IF l>N THEN GOTO EXIT:

Figure 8: An example termination.

Like a filler, a termination creates a fragment out of a lest which is repetitively executed. Also like a filler, it takes in a temporal sequence of of values and outputs a restricted sequence of values. The restricted sequence corresponds to the initial portion of the input up to the first value which satisfies the test. However, unlike a filter, a termination has the far reaching effect thai il causes the loop as whole to terminate.

The PBM temporal composition builds complex loops by combining loop fragments together. The process of combining the fragments is logically equivalent to composition. This makes il easy to understand what the resulting loop does. Figure 9 shows an example of this. The four fragments in the figure are composed together in order to yield the loop shown (which is the same as the one in Figure I). Logically this is just a composition of [)(C(B(A()))) and therefore it is clear that the

feedback free

the loop which results from the temporal composition I = 1: z .. 0: LOOP: IF NOTIA1lb01 THEN Z · Z+Aill: I .. I +1: IF I~N THEN GOTO LOOP:

Fieure 9: An example temporal composition.

result computes the sum of the positive members of the first N elements of the array A since the augmentation A counts up by I from I, the termination 8 truncates this sequence at N, the filler C selects the elements of the sequence which correspond to positive members of A, and the augmentat ion 0 computes a sum of these elements.

The process by which the fragments are actually combined in order to produce the resulting loop is somewhat complicated. Th1s process is designed so thai the validity of the simple logical analysis in terms of composition will be preserved. The fragments are la~.en apart, and their pieces are reassembled into the resulting loop. The inilializalions of the fragments are placed before the resulting loop. The bodies are placed inside the loop. Their arrangement in the loop is dictated by the data flow communicatine temporal sequences of values between the fr<'gments. The key idea is that if the body of one fragment uses a temporal sequence created by the body of another fraGment, then the first body should be placed alter the second one in the resulting loop. The action of a filler is produced by placinG the bodies which receive its outputs within the scope of a conditional predicated on the filter's test.

II turns out to be straightforward to analyze a loop in order to brea~. it apart into fragments combined by temporal composition. The analysis process is based on locating sections of the loop which do not affect any other parts of I he loop. One section affects another if it either has data flow to il, or if it controls when il will be executed. Once such a section is located, it is removed as a fragment and the analysis continues. This process is sufficient to locale augmentations and filters. Consider the re~.ulting loop in FiGure 9. If il were being analyzed, the first frasmenl to be located would be D. This would be done by noticing thai the line "ZaZ+A(l)" does not have data flow to any other part of the loop. Once this line is removed the filler C is no longer controlling the execution of anything, so it too can be isolated and removed.

Terminations are somewhat more complex because they perforce affect everythine else in the loop since they determine when the loop will terminate. To allow them to be located and removed, the delinition of not affect is weakened in order to allow I his particular kind of effect . In order to main! ain I he logical structure based on composition, the descriptions of the fraemenls have to be prohibited from mentioning anything which a termination can affect (namely the absolute number of limes anything will be executed).

4. Using PBM Analysis to Guide Verification

The most fundamental impact of the PBMs on verification is that they break up a program into a useful hierarchy of segments wi thin segments. This structure can be used as the underlying structure of a proof of correctness, by determining spec if ications for each segment and then verifying these specif ic at ions. With each subproof, the method which is used to r,enerate a proof can benefit from the fact that it only has to work on the single subproof which has been singled out by the PBMs, rather than on the program as a whole.

The impact of the PBMs on the strutlure of a correctness proof is greatest with regard to loops. They lead to a proof which is fundamentally different in form from the standard approach of u~ing a single loop invariant. Consider the program in Figure 10 ;md how it would be verified by using a single loop invariant as originally introduced by Floyd [ 4] and Hoare [9]. Assertions are passed over the body of the loop in order to develop a statement of what the body does. Then an appropriate loop invariant is developed. Finally, the statement of what the body does is used to prove the invariance of the loop invariant, and the loop invariant is used to verify the specifications of the loop.

X a 0; Y a 0; L 11; DO K=1,10; IF CIKI>0 THEN 00; X X+A IKI; Y · Y+A IKhA ILl; END; L · L+l; END; the program is claimed to compute X·l:llsisl0 I Clii>0JAiil " Y·l:llsi sl0 1 Clii>0JAiii*Aii+l01 assertion summarizing the actions of the body ICIK'I>0 ... IX~X'+IIIK'I "Y=Y'+A(K'I*AIL'lll" L· L ' +l" ICIK'ls0 ... IX=X' "Y·Y'll "K·K'+l a loop invariant 0sKsll "X·Itlsisl0 1 Clii>01Aiil " L·K+l0" vpLflsisl0 1 Clii>0JAiii*Aii+l0l

One of the most difficult steps in a proof of this form is the determination of an appropriate loop invariant. Considerable research has been done on ways to automatically develop invar iants. Mpch of this work centers around heuristic methods whi ch can be used to guide a search for an invariant [6, 12, 22]. Some of it is or iented toward directly deriving invariants for specific dasses of loops [2, 3, 14). The work of Basu and Misra is part icularly interesting. They analyze the mathematical proper ties of a loop in order to directly derive an appropriate loop invar iant for certain classes of loops.

Figure 11 shows how the program .in Figure 10 would be analyzed by PBMs, and how this leads to a proof of correctness. The program is divided into six parts: an augmentation which enumerates integers in K, a termination which truncates this to the sequence of integers from I to 10 in K, an augmentation which enumerates the integers from II to 20 in L, a filter which restricts these temporal sequences of values by selecting only those elements which correspond to positive values of C(K), an augn1entation which computes the sum of the indicated elements of A, and an augmentation which computes the sum of the products of the indicated elements of A. This decomposition leads to a style of proof based on composition which is very different from the proof in Figure 10. First several lemmas are proved. Each lemma summar izes the actions of one of the parts of the program. Second, the lemmas are combined by composition in order to yield the desired result.

loop fragment K c l; K a K+1; IF K>10 THEN GOTO EXIT: L · 11: L = L+l; IF CIKI>B THEN X · 0: X= X+AIKI; values it produces lsi Kip i 1sis10 K i E i 1sis10 Li·i+l0 restricts 1sisl0 Xi·Lflsjsi Ki and Li C I j 1>01 A ( jl v 0; l s i sl0 Y · Y+AIKJ*AILI; yi.L!lsjsi 1 Clji>0JA!ji*Aij+101

The problem of finding the loop invariant is dealt with by breaking it up into pieces. No invariant is needed in order to ver ify the program as a whole. Rather , each of the proofs of the lemmas requires an invariant. However, each of these proofs is so simple that it is easy to determine what the invariant should be by the methods of Basu and Misra, if not by simpiP recognition. It should be noted that not all programs can be decomposed by PBMs as nicely as the one in the example. There is no limit to the complexity of the pieces which result. Therefore, it may be very diff icult to determine the invariant needed to prove one of the lemmas needed. Even in this situation, the PAM analysis is useful because it determines the parts of the invanant as a whole which are easy and separates them from the parts which are difficult. PBM analysis is ('lOt a uniform procedure which will determine the invariant for any loop; rather, it simplifies the problems involved with finding most of the invariant for most loops.

The fund;~mental difference between the form of the proof en~endcred by PBM analysis and the form of the proof resulting from the single inv;~riant method becomes apparent when the proof is used for something other than giving a yes/no answer to the question of whether or not the program is correct. For ex ;~mple , suppose that the program were incorrect and that therefore the proof failed. The PBM proof is broken up into a sequence of steps which are directly linked to parts of the program. If the failure of the proof can be localized to one of the steps of the proof, then the bug in the program can be localized to the corresponding part of the program. The failure of a proof based on a single loop invariant does not lend itself to this kind of analysis.

5. An Experiment

The straight -line PBMs are similar to bas1c structured programming constructs, and can be used to analyze any straight-line program that does not have spaghetti-like control flow. The loop PBMs are more novel, and it is not immediately clear how wide their rllnge of applicability is. An experiment was performed in order to estimate what percentage of the loops which programmers actually write can be analyzed in terms of the PBMs without anything more than trivial transformations being done. 20% of the 220 programs in the IBM FORTRAN Scientific Subroutine Package (SSP) [10) were chosen at random and analyzed in terms of the PBMs by hand. The SSP was chosen as an object of study because it is a large group of clearly written programs which is an actual commercial product.

The 1111 programs chosen contained 1611 loops. It was possible to analyze all of the loops with the PBMs. They were analyzed as being built up by means of the PBM temporal composition out of 11112 augmentations, 6 fillers, and 186 terminations. Conf igurations which cannot be analyzed (such as a loop with more than one entry point) did not occur in these loops. The sole diffic.ully was that one loop had multiple level error exits which branched outside of the loop from inside an inner loop. In order to analyze tlie error exits in terms of the PBMs, they had to be looked at as being explicit exits from the inner loop and the outer loop. This may or may not be a good way to look at them.

Nearly 90% of the lime, the pieces which resulted from PBM analysis were very simple. Of the 11112 augmentations, 374 (85'4) were either easy to understand because they did not have feedback to themselves, or easy to recognize as 1 product, a sum, a max, a min, or a count. Only 31 (7%) were really difficult to understand. The remainder were of intermediate complexity. All 6 fillers were simple comparisons with zero and therefore easily understood.

Of the 186 terminations, 165 (89'4) were very simple to understand because they were simple comparisons with a fixed number, and the input which they tested was a simple sequence of numbers, most often {1,2,3, ... }. Due to the fact that their tests and inputs were so simple, it was trivial to determine the exact number of states associated with their inputs, and hence ex·actly when the loops they were in would terminate. lv1ost of the 2 I terminations. that were more complex, were additional terminalions in loops which had at least one simple termination. As a result of this, 162 (99%) of the 164 loops contained at least one simple termination, and therefore can be trivially shown to terminate.

6. An Automatic Analysis System

The author has implemented a system (described fully in [21)) which l!ulomatically 11nalyzes programs in terms of PBMs. The system operates in two phases. A translation phase reads in a pror,ram and converts it to a language independent internal form railed a "surf ace plan". An analysis phase then analyzes the program by looki11g at its surface plan.

A surface plan makes the control flow and. data flow explicit independent of the syntactic constructs of any particular l11nguagc. It is essentially a graph with two kinds of arcs. The nodes of the graph correspond to primitive operations such as: plus, times, and less than. One type of arc specifies the flow of a data object from one node to another. The other type of arc specifies the flow of control from one node to another. Co11structs which languages use to implement data flow (such as: variables, assignment, parameters, and nesting of expressions) are not present in a plan. All information about data flow is contained in the data flow arcs. Similarly, constructs which l<mguages use to implement control flow (such as GOTOs and sequenti11l placement of statements) are eliminated in favor of the control flow arcs.

A translator has been written which converts FORTRAN progr11ms, like those in the IBM SSP, into surface plans. Char les Rich [17] has written a translator which converts LISP programs into surf ace plans. After this conversion, the analysis phase of the system works on LISP programs just as easily as on FORTRAN programs.

The translator works by running over the program like an ev11luator, creating control flow arcs, data flow arcs, and no,des which comprise a surface plan as it goes. The tr11nslator .has detailed knowledge of the constructs which implement data flow and control flow. It does not have any knowledge of what the primitive functions do except how many inputs and outputs tliey have.

Once a program has been tr anslaled into a surf ace plan, it is then analyzed in terms of PBMs. This is done in two main steps. The first step looks primarily at the control flow arcs and analyzes the slrai~:ht-line sections of the program while merely identifying the loops in it. This is essentially an analysis in terms of basic structured programming constructs as discussed in Section 2. The analysis is done bottom up by locating minimal configurations which can be grouped together in accordance with a PBM. Whenever such a configuration is located, it is grouped together into a single node, and the analysis cont inues. This process terminates when the entire program is grouped into a single node.

The first step of analysis can be compared with the system of B. Baker [I). Her system uses graph theoretic methods in order to analyze FORTRAN programs based on their control flow in terms of basic structured programming constructs. Her system then outputs the program in a structured form. GOTOs are used in situations where an analysis in terms of the structured programming constructs is not possible.

The second analysis step analyzes the loops discovered by the earlier steps according to the four PBMs temporal composition, augmentation, filter, and termination. This analysis is based primarily on data flow connectivity and proceeds as described in Section 3. For example, augmentations are located by finding minimal subsets of the body of a loop which do not have data flow to any olhP.r pe~rl of the loop. Once 11n augmentation is discovered, it is removed from the loop and the remaining loop is 11nalyzed further.

7. PBMs and Programming Language Constructs

The PBMs which are used in the first step of analysis correspond to basic structured programming constructs. If the analysis system operated on programs written in a language which required the use of these basic structured programming constructs, the first step of analysis would not be necessary. On the other hand, the loop PBMs do not correspond to eny existing structured programming constructs.

However, the loop PBMs do embody natural ideas, end many programming constructs have features in common with them. For example, there are a variety of constructs which have the fe<~ture that they separate out an augmentation and a termination, which tonether enumerate a sequence of values, from the rest of the loop which does something with them. The most common example of this is the DO statement. It makes a cle~r syntactic distinction between the enumeration of a ~.equence of integers and their use. However, in most languages, the DO statement does not correspond semantically to an <~u&menlalion and a termination because the programmer is not prohibited from <~ssigning to the DO variable in the body of the loop.

The MAPC funct ion in LISP is similar to the 00 statement except that it enumerates the clements of a list instead of a sequence of integers. GENERATORS in ALPHARD [18] and ITERATORS in CLU [13], extend thi~ concept to the enumeration of elements of Mbilrilry data types. The MAPCAR function in LISP is Interesting becau~e as well as enumerating the elements in a list, it conlilins a standard augmentation "(SETQ X NIL) (SETQ X (APPEND X result))" which forms a list of the results.

The language APL [15] has several operators which operate directly on vectors in a fashion very similar to the way PBMs operate on temporal sequences of values created by loops. For example, the reduction operator is · similar to augmentation in thai it applies an operator such as plus or limes to the elements of a vector in order to compute the sum or product of all the elements in the vector.

The Language developed by .Kahn and MacQueen [II) makes it possible to construct coroutine processes operating on sequences of values which interact in the same way as aunmenl at ions <~nd filters. The processes can be combined together into expressions which can be evaluated either ~.equentially, or in parallel.

With either APL or the language of Kahn and MacQueen, in Older to gel the significant savings in lime and space which result from implementing augmentations and filters by loops operating on temporal sequences of values the language would have to h<~ve a smart compiler . The compiler would have to know how to combine the pieces together into loops. The work which has been done on developing a compiler for APL (see for example, (7]) indic ales that this is not an unreasonable goal.

8. Conclusion

The basic idea behind the analysis method presented here is "'"' a typical loop can be looked at as a composition of stereotyped fragments of looping behavior. This point of view reflects the way many programmers analyze, understand, and reason about loops. The PBMs, and the idea of temporal sequences of. values are important because they make if possible for <1n ilulomalic system to analyze, understand, and re<~son about loops in this same straightforward way.

The PBMs were developed as part of a larger research project. The goal of this project is to develop a system (called the ""Programmer's Apprentice"·) which can assist a person who is writing" program. Research on this system [16, 17, 19, 20, 21) is being carried out by a group consisting of Charles Rich, Howard Shrobe, and the author. The intent is that the <~pprenlice system will cooperate with a programmer throughout all philses of work on a program and be able to communicate with him about it. The programmer will do the hard parts of design and implementatipn while the apprentice will act as a junior p<~rlncr <~nd critic, keeping track of details and assisting the programmer whenever possible. PBMs play an important role in the processes by which the ilpprentice develops an understanding of and reasons about a program.

ACKNOWLEDGMENTS

The author would like to thank Charles Rich, Gerald Roylance, Howard Shrobe, and Gerald Sussman for their assistance.