A Heuristic Approach to Program Verification

I. Introduction

The desirability of proving that a given program is correct has been noted repeatedly in the computer literature. Floyd [1967] has provided a proof method for showing partial correctness of iterative (flow­ chart) programs, that is, it shows that if the program terminates, a given input-output relation is satisfied. The method involves cutting each loop of the program, attaching to each cutpoint an "inductive assertion" (which is a predicate in first-order predicate calcul­ us), and constructing verification conditions for each path from one assertion to another (or back to itself). The program is partially correct if all the verifica­ tion conditions are valid. Elements of these tech­ niques have been shown amenable to mechanization. King [1969], for example, has actually written a 'veri­ fier' program which, given the proper inductive asser­ tions for programs written in a simplified Algol-like language, can prove partial correctness. Thus, it is fairly clear that the parts of this method which in­ volve generating verification conditions from inductive assertions and then proving or disproving their vali­ dity is a difficult but programmable problem. However, as King puts it, finding a set of assertions to 'cut' each loop of the program "depends on our deep under­ standing of the program's performance and requires some sophisticated intellectual endeavor".

In this paper we show some general heuristic tech­ niques for automatically finding a set of inductive assertions which will allow proving partial correct­ ness of a given program. More precisely, we are given a flowchart program with input variables x (which are not changed during execution), program variables y (used as temporary storage during the execution of the

A HEURISTIC APPROACH TO PROGRAM VERIFICATION

Shmuel M. Katz and Zohar Manna

Department of Applied Mathematics The Weizmann Institute of Science Rehovot, Israel

program), and output variables z (which are assigned values only at the end of the execution). In addition, we are given "input predicate" <P (x), which puts re­ strictions on the input variables, and "o·utput predi­ cate" 1jl(x,z), which indicates the desired relation be­ tween the input and output variables. Given a set of cutpoints which cut all the loops, our task is to at­ tach an appropriate inductive assertion Qi to each cutpoint i.

We distinguish between two general approaches:

• (a) top-down approach in which we obtain the induct­ ive assertion inside a loop by analyzing the predicates which are known to be true at the entrances and exits of the loop, and
• (b) bottom-up approach in which we generate the in­ ductive assertion of a loop directly from the state­ ments of the loop.

For "toy" examples, having only a single loop, it is generally clear that the top-down approach is the natural method to use. However, this is definitely not the case for real (non-trivial) programs with more com­ plex loop structure. In this case some bottom-up tech­ niques were found indispensible. Most commonly we have found it necessary to combine the two techniques, with the bottom-up methods dominant.

Preliminary attempts to attack the problem of find­ ing assertions have been made by Floyd [private commun­ ication], and Cooper [1971]. Heuristic rules basically similar to some of our top-down rules have been discov­ ered independently by Wegbreit [1973]. Elspas, et al. [1972], used "difference equations" derived from the program's statements which is, in essence, a bottom-up approach.

We handle programs with arrays separately, since generating assertions involving quantification over the indices of arrays requires special treatment. Thus in Section II we discuss heuristic techniques for flow­ chart programs without arrays, while in Section III we extend the treatment to programs with arrays. In Sec­ tion IV (conclusion) we discuss open problems and pos­ sible implications of our techniques. Related problems where these approaches seem applicable include proving termination of programs, and discovering the input and output assertions of a program.

Our emphasis in this paper is on the exposition of the rules themselves and we are purposely somewhat vague on other problems, such as correctly locating the cutpoints or ordering the application of the rules. Though we do not enter into details, we assume that whenever possible we conduct immediate tests on the consistency (with known information) of a new component for an assertion as soon as it is gene­ rated, and that algebraic simplifications and manipu­ lations are done whenever necessary.

II. Heuristics for Programs without Arrays A. Top-down approach.

We begin by listing the top-down rules, which may be divided into two classes: entry rules and exit rules.

1. Entry rules. These rules are intuitively ob­ vious, but provide valuable information in a surpris­ ing number of cases.

rule Enl. Any conjunct* in the input predicate ~(x) may be added to any Q. It need not be proven since the input variables are not changed inside the program. rule En2. Any predicate known to be true upon first reaching a cutpoint i should be tried in Qi.

1. Exit rules. For simplicity in the statement of these rules, we assume that a cutpoint is attached to the arc immediately before an exit test of the loop. Thus we may consider an exit from a loop to be of the form

where ti is the exit test, pi is some conjunct of a predicate known to be true when the exit test first holds, i is the cutpoint on the arc leading into the exit test, ·and Qi is the assertion which we wish to discover. We attempt to extract information from pi and ti in order to find an assertion for the cutpoint i. The exit rules will lead to a predicate R which is guaranteed only to satisfy

* If a predicate is expressed as a conjunction A1AA 2 A ··. AAn' then each Ai is a conjunct of the predicate.

we then must show that the R obtained is indeed a va­ lid assertion.

rule Exl, If pi is not identical to ti' let R be pi itself. rule Ex2. (transitivity) Although this rule could be applicable to a wider class of operators and rela­ tions, we restrict the treatment to inequalities. Suppose pi has_ the form a 1 Aa 2 and ti has the form b 1 Bb 2 where aj and bj are any terms and A,B are equality or inequality relations. If one of the a.'s J is identical to one of the bj's, try to find an appropriate inequality or equality relation R so that ti A R :::> pi becomes true. For example, if ti is x < y 2 and pi is x < (y 1 +1) 2 , then we let R be y 2 l> (y 1 +1) 2 since x <. y 2 A y 2 ~ (y 1 +1) 2 ::>x < (y 1 +1)2 is true.

We may extend rule Ex2 and use in our search for R any conjunct attached to cutpoint i which has some­ how been previously verified (i.e., it is true upon entry to the loop, and is invariant going around the loop, but does not yet imply the exit predicate pi). For example, if the conjunct y 2 = y 3 · x 2 has been previously verified at cutpoint i, and ti is the test y 3 1, while pi is y 1 < x 2 , then we may try R being y 1 < y 2 , since y 2 = y 3 ·x 2 A y 3 = 1 A y 1 < y 2 :::> y 1 <x2'

Another possible extension of rule Ex2 is to search for additional information on the variables in the exit test. We seek information which along with ti would imply stronger restrictions on the exit values of those variables. For example, suppose ti is y 1 >- .x , we know that y 1 < x upon first reaching i (i.e,, the loop is executed at least once), and y 1 is incremented by 1 at each pass through the loop. Then * we let t be y 1 = x since y 1 >- x A y 1 -l < x :::> y 1 ~ x in the integers. Thus, rather than looking for R satisfying y 1 >­ satisfying y 1 x A R :::>pi' it suffices to find an R X A R :::> pi.

rule Ex3. If rule Exl fails, a natural "weaker" attempt could be to let R be ti :::>pi' This rule is sometimes of practical use; however, it says very little about the computation taking place in the loop. Our strategy would give this rule a low priority, try­ ing other rules with stronger resultant claims first.

It is possible to continue ~o design rules for obtaining R for specific forms of pi , but since our a im i s to explain the general tone of these technique~ we will not go into further details in this direction. B. Bottom-up Approach.

All of the rules given above have in common that they expect to- be provided with some information on either what conditions were true upon entering the loop or what conditions were expected to hold upon completing the loop (or both). However., it is possible t o produce conjuncts of the assertion Q without con­ sidering predicates already established elsewhere in the program. In order to accomplish this goal we shall look for a predicate which is an invariant of the loop L, i.e., it remains true upon repeated exe­ cutions of the loop.

Clearly, any conjunct in the inductive assertion of a loop must be an invariant of the loop. However, in the top-down rules this is usually the last fact which is established about a prospective assertion. In the pure bottom-up approach, assertions which arise "naturally" from the computations in the loop are di­ rectly generated -- and only afterward checked for relevance to the overall proof.

Most invariants may be traced back to the fact that at any stage of the computation, those assignment statements which are on the same paths through the loop have been executed an identical number of times, and this is a 'constant' which may be used to relate

the variables iterated.

For an assignment statement yi + f(x,y) we let yin) denote the value of yi after n executions of the statement, while yiO) indicates the "initial" value of yi upon first reaching a given cutpoint of the loop.

Our technique for finding invariants involves constructing an "operator table" in which we record useful information for each operator. Among the entries for an operator are its definition (using "weaker" ope­ rators), a description of a general computation after n itera tions, and other common identities which faci­ litate simplifications. For example, for +our table will include the fact that for an assignment gtatement of the form y + y +k, in general y(n)=y(O)+ L k(j-l) (j 1) i i i i i-1 where k - is the value of k before the j-th iteration of the assignment statement. Important identities are also noted n L c=c ·n, and that i=l including that for a constant c , n n(n+l) L i= --- 2 --- · Rules for producing i=l invariants linking variables which receive assignments on different paths through the loop are presently being developed. Here we present rules only for the simple case of variables changed only on the same paths through the loop.

rule Il. (invariant) To construct an invariant, given a group of assignments*

we consider those variables yj' 1 ~ j ~ 1 , which are not changed elsewhere in the loop. Using the operator table we express the value of each yj after n iterations, i.e. y~n). W th tt t t fi d f J e en a emp o n a actor common to two expressions in order to obtain a usable relationship between yin) and y~n). The relation ob­ tained after substituting the initial values of yi and yk at cutpoint A for yi 0 )and y~O), respectively, and removing the superscript (n) is an invariant of the loop. It also holds for the initial values of the variables at A and thus may be added to QA.

For example, if y 1 and y 2 are changed only in the assignments (y 1 ,y 2 ) + (y 1 +x·y 3 , y 2 +5·y 3 ) inside a loop, then y(n) = y(O} + x·I y(i-l) and y(n) 1 1 i=l 3 2

that the initial values of y 1 ing the cutpoint are y(O) = 1 1 the invariant 5(y 1 -l) = x·y~. (yl,y2)+(2·yl,y2/2) then yln) and y upon first reach­ and y~O) = 0 we obtain 2 · If the assignments were = y(O). ~ 2 and 1 i=l

x(x ~ 0) we rule I2. only (O) yi get that y 1 ·y 2 = x is an invariant. (n) Whenever yi may be expressed in terms of (n) ro) and n, i.e., y 1 ~ f(y{ ,n) , and the value of y~O) at the cutpoint A is known to be m, then rel. placing yiO) by its value and removing superscript (n), we may obtain the invariant 3n[n ~ 0 A yi = f(m,n)]. Variables iterated simultaneously may be quantified by the same n. For example, in the second example of Il, 3n[n ~ 0 A y 1 = 2n A y 2 = x/2n] is an invariant of the loop.

* The above notation implies that the value of fi(x,y) is assigned to yi for all i's simultaneous­ ly.

Our heuristic rules are all relevant to programs having an arbitrary number of loops, and an arbitrary complex 'topology', although, of course, they will yield valid inductive assertions more often and more immediately in a simple program.

One of the problems in applying the rules is deci­ ding what order is preferable. In particular, it has been found that many terms of the assertion may be ob­ tained both by the bottom-up rules and by repeated use of the top-down rules. However, usually one method will yield the result immediately, while considerable effort is expended if the other method is applied first. Experience shows that there is a need for in­ teraction between the top-down and bottom-up ap-. proaches. For example, we may use established invar­ iants to deduce the relation R in the top-down rule Ex2, and on the other hand, we may direct the search for particular invariants based on variables or opera­ tors which appear in pi ·

C. Examples. We demonstrate the rules listed so far on a few examples.

Example 1: Integer square root. The program in Figure 1 computes z = l~J for every natural number x. That is, the final value of z is the largest integer k such that k ~ ~. We show partial correctness for ~ (x) x ~ 0 and $(x,z) : z 2 ~ x A x < (z+l) 2 · Clearly yi ~ x A x < (y 1 +1) 2 is required to be true after exit from the loop. We first try the top-down approach. By rule Exl we attempt adding the conjunct Yt ~ x to Q

The verification condition x >- 0 ~ yi ~ x is, in fact, true for the initial value of y 1 at the cutpoint, i.e., y 1 = 0. For the moment we do not attempt to verify that it is an invariant of the loop. Considering the second conjunct of the predicate, x < (y 1 +1) 2 , an attempt to apply Exl fails because this relation is not true for the values of the variables when the cutpoint is first reached. Since the exit test y 2 > x and the predicate x < (y 1 +1) 2 both contain x, we apply rule Ex2. We find that y 2 ~ (y 1 +1) 2 is the desired relation since y 2 > x A y 2 ~ (y 1 +1) 2 ~ x < (y 1 +1) 2 is a valid statement. y 2 ~ (y 1 +1) 2 is satisfied for the initial values of the variables. However, an attempt to prove the validity of Q : yi ~ x A y 2 ~ (y 1 +1) 2 does not yet succeed.

At this point we try to use the bottom-up approach, i.e., try to find invariants. We note that the assign­ ments along one pass of the loop may be combined into the single group of assignments (y 1 ,y 2 ,y 3 ) +

(yl+l,y2+y3+2 ,y3+2) obtain the equations From the operator table we

We may use equation (3) to substitute for y~i-l) in equation (2}, and simplify to

In the simplification above known facts about the sum­ mation operator (obtained from the operator table) are used.

for every n, i.e., y 3 = 1+2y 1 A y 2 = (l+y 1 ) 2 are in­ variants of the loop and should be added to the trial Q. Q becomes Yf ~ x A y 3 = 2y 1 +1 A y 2 = (y 1 +1) 2 ,

which will prove the partial correctness of the program.

Example 2: Division within tolerance, The program of Figure 2 divides x 1 by x 2 first to find invariants. within tolerance x 3 · We try Considering the assignments obtain the equations y~n) Therefore

the cutpoint, we obtain 2y~n) = x 2 ·y~n). Thus 2y 2 = x 2 ·y 3 is the first conjunct in the trial Q. Next we consider the assignments (y 1 ,y 4 ) + (y 1 +y 2 ,y 4 +y 3 /2). In order to be able to find a common factor in the equa­ tions for y}n) and y~n) we first eliminate y 2 by using the already established invariant y 2 = x 2 ·y 3 /2, obtain­ ing (y 1 ,y 4 ) + (y 1 +x 2 ·y 3 /2,y 4 +y 3 /2). Now we get

(i-1) n y3 Eliminating the common term L --- 2 --- , the result is i=l

paths to initially reach the cutpoint, the pair

( (0) (0)) yl ,y4 x2 1 may be either (0,0) or (:2, 2), In (n) either case, the simplified expression becomes y 4 (n) y 1 /x 2 · Therefore y 4 = y 1 /x 2 is added as a conjunct to the trial Q.

Since no further information ca~ be gained from the invariant rules, we turn to the top-down rules. We have y 4 ~ x 1 /x 2 A x 1 /x 2 - x 3 < y 4 true upon exit from the loop. Trying Exl on y 4 ~ x 1 /x 2 , the conjunct can be seen to hold initially at the cutpoint by cases, since if x 1 < x 2 / 2 then y 4 is initially 0 at the cutpoint and by cp we have 0:; x 1 /x 2 , while H x 1 <1 x 2 /2, then 1/2 ~ x 1 /x 2 and y 4 is 1/2 at the cutpoint. Thus by Exl we may add y 4 ~ x 1 /x 2 to Q. The second conjunct, x 1 /x 2 - x 3 < y 4 , on the other hand, does not nold ini­ tially so we try Ex2. The necessary 'transitive' relation is found to be x 1 /x 2 - y 3 ~ y 4 since y 3 < x 3 A xl/x2 - y3 ~ Y4 => xl /x2 - x3 < Y4 We note that xl/x2 - y3 ~ y 4 holds for the initial values at the cutpoint so we add it to Q. Q is now y 2 = x 2 ·y 3 /2 A y 4 = y 1 /x 2 A y 4 ~ x 1 /x 2 A x 1 /x 2 - y 3 ~ y 4 which will prove the program partially correct.

ExamEle 3: Hardware (integer) division. The program of Figure 3 is a simulation of how integer division might be carried out by a computer. The 'division by 2' represents a 'shift-right', and the 'multiplication by 2' a 'shift-left'. Although the second loop of this example is similar to the program of Example 2, we bri ng it in order to illustrate how programs with more than one loop may be handled, and how compli­ cations which could arise from integer division may be solved with the aid ot the inv~~i~nt ~le, Our stra­ tegy is to obtain a maximum amount of information from the first loop, which will be true upon entrance t o the second loop. Then top-down rules can be used conven­ iently for the second loop.

In the first loop we attempt to link y 2 and y 3 , obtaining y~n) x ·2n and y;n) = 1·2n which leads to the 2 invariant y 2 X2'Y3 by rule Il. By rule I2 we also have the conjunct 3n[n ~ 0 A y 2 = x 2 ·2n A y 3 = 2n]. We now consider top-down rules, Since y 1 ~ 0 A y 2 > 0 holds initially, it is added by rule En2 to Q 1 , which thus becomes the valid invariant y2 = X2·y3 A 3n[n ~ 0 n = 2n] ~ 0 A o. A y 2 = x 2 ·2 A y 3 A yl y2 > All this information, as well as y l ~ y2 is a predicate p 1 true upon first reaching the second loop. Recall that for the entrance rules we consider the predica tes true upon first reaching the cutpoint i. Thus the in­ formation in p 1 must be 'moved' along the paths to cut­ point 2. y 2 > 0 A y 2 x 2 ·y 3 A 3n[n ~ 0 A y 2 = x 2 ·2n A y 3 = 2n] are unchanged by either path to 2, while y 1 might be changed but y 1 ~ 0 can be seen to remain true by inspection. If the right path is taken, y 1 ~ y 2 is strengthened to y 1 < y 2 , while the left path may be used only if y 2 · In this case y 1 is set to zero, and since y 2 > 0 is known, in either case y 1 < y 2 at cutpoint 2. At this point, all the necessary assertions for hand­ ling the second loop are already given explicitly in the entry and exit predicates. Using rule En2 we ob­ tain Q 2 : y 2 = x 2 ·y 3 A 3n(n ~ 0 A y 2 = x 2 ·2n A y 3 = 2n] A y 1 ~ 0 A y 2 > 0 A y 1 < y 2 , while from Exl we add x 1 = y 4 ·x 2 +y 1 to Q 2 · This Q 2 will be a good inductive assertion.

The rule involving n, obtained by I2, is necessary here in order to guarantee that the conjunct y 2 = x 2 ·y 3 is valid, because of the 'shift-right' division. We clearly could have obtained some of the conjuncts in Q by other rules. For example, y 1 < y 2 could have been obtained by rule Ex2 (because p 2 contains y 1 < x 2 , y 2 = x 2 ·y 3 is an invariant, and y 3 = 1 is the exit test), or x 1 = y 4 ·x 2 +y 1 by rule Il.

III. Heuristics for Arrays

The problem of finding assertions involving arrays is quite different from that of finding assertions for simple variables because an array assertion generally will be an entire family of claims. This is the rea­ son most assertions about arrays will involve quanti­ fiers. All rules in Section II continue, of course, to be applicable for those variables not in arrays. In addition, rules Enl, En2, Exl and Ex3 may be used for assertions with arrays.

Underlying the heuristics which follow is the assumption that arrays in a program are used "properly', i.e., to treat a large number of variables in a uni­ form manner, and not just as a collection of unrelated variables fulfilling different roles in the program. The further assumption is usually made that an asser­ tion about an array will be of the form

Vj[<j-index> ~ <j-array>] or 3j[<j-index> A <j-array>], where <j-index> is a claim on the indices of the array and <j-array> is the claim which is made about the array elements themselves. We often separate the two problems of finding the <j-index> and of fi~ding the <j-array>.

As in Section II, we distinguish between the top­ down and bottom-up approaches.

In order to apply some of the array rules it is convenient to first determine t)le "one-pass" assertion, i.e., the claim which can be made about the effect on the arrays of one circuit through the loop. This claim is often not difficult to establish, in particular for loops which do not contain other loops since then the circuit through the loop is a simple sequence of state­ ments. The assertion can be most easily established by the known technique of "backward substitution", moving backwards around the loop past each assignment statement.

A. Top-down rules.

As noted above, all previous top-down rules, except for the transitivity rule Ex2 (which invo1ves inequali­ ties), are directly applicable for arrays. In the rules listed below, p denotes an assertion with quanti­ fication concerning an array which is true after exit from the loop, while p' is an assertion like p, but true upon entrance to the loop. Q denotes the desired loop assertion. Rules Al, A2, and A4 attempt to either transform or create assertions p and p' having a form which will facilitate generating Q by rule A3. rule Al. Let p be a claim about a specific element of an array, say S[c] (and thus not necessarily including quantifiers). We rewrite it as 3j [c ~ j ~ c A <j-array>], where <j-array> is p with j in place of c. Similarly, if a p' as above is true upon entrance to the loop, we rewrite it as Vj[c ~ j ~ c ~ <j -array>] ·

The underlying principle here is that a claim whose <j-index> is made smaller by the loop probably has an existential quantifier (we are "looking for something''), while if the <j-index> is extended to cover more ele­ ments by the loop, the claim probably has a universal quantifier (we want something to be true for a larger part of the array). Thus we may check the feasibility of the resulting assertion by determining whether the <j-array> is in fact expanded or contracted in the lao~ This principle is also used in the bottom-up rules. rule A2. Given a p, we examine the definitions of the operators and relations in p and whatever information is known about the array upon first reaching the loop. Using this information we produce the <j-index> for a p' which must be true upon entrance to the loop, and has a <j-array> identical to p. For example, if p is 3j[l ~ j ~ 3 A A[j] = ~(A[l], ··· ,A[n]) ], and we know only that A is defined upon entrance to the loop, by the rule we require a <j-index> such that A[j] = ~(A[l], ··· ,A(n]) must be true. By the definition of max we can determine that the maximum element must belong to the array. Thus 3j[l ~ j ~ n A A[j] = ~(A[l], ··· ,A[n])] is the parallel assertion upon entrance to the loop.

In some cases of a predicate p with universal quantifiers, the corresponding initial claim may require a <j-index> which is empty (so that the overall claim is vacuously true). For example, if pis Vj[l ~ j < n ~ A[j] ~ A[j+l]], and we have not sorted A before the loop, p' might be Vj(l ~ j < 1 ~ A[j] ~ A(j+l]] ·

Rule A2 is the only example in this paper of a rule which enables us to project "backwards" to find the minimal conditions which must hold upon entrance to a given loop. Such rules should be useful not only to aid in discovering the correct assertion for the loop in question, but also to carry information backwards for loops earlier in the program. Thus further inves­ tigation of this general technique is warranted. rule A3. . If p contains a term r as a boundary of the indices, and we have determined that for some term s, s = r upon exit from the loop (by any of the rules in Section II), we let Q be the predicate obtained by substituting s for some appearances of r in p.

Similarly, if p' contains a term r, and s r upon entrance to the loop, let Q be the predicate obtained by substituting s for some appearances of r in p'.

For example, if p is Vi[l ~ i ~ m ~ A[i] ~ A[m)), and i = m is the exit test of the loop, we could try letting Q be either Vi[l ~ i ~ i ~ A(i] ~ A[m]], Vi[l ~ i ~ m ~ A[i] ~ A[i]] or Vi[l ~ i ~ i ~ A[i) ~ A(i]].

Obviously, if information is known about both p and p' , the application of A3 can often be directed by matching the results of various substitutions until the entrance and exit claims are identical. Thus, if there are several possibilities for substitution, we may decide for which appearances of terms in p or p' to substitute.

We would like to be able to also use the transiti­ vity rule Ex2 for an array assertion with quantifi­ cation (specifically, a p with an inequality as its <j-array>). This requires establishing that for each pair of terms compared, we may find a third term such that there will be two new inequalities, true upon exit from the loop, which will imply the original in­ equality (as in Ex2).

rule A4. Given a p with universal quantifier and an inequality including arrays as its <j-array>, we use the "one-pass" assertion to find a term which contains the two needed inequalities for a particular value of j (i.e., for a single pair of values from p). Then let each new in'equality be the <j-array> for a claim having the <j-index> of p. The other top-down rules may then be used separately on each of the new in­ equality claims to obtain the loop assertion.

For example, given p : Vi[l ~ i ~ m ~ A[i] ~ B(i]], we might discover a C[k] such that A(k] ~ C[k] A C[k] ~ B[k] for some k, and assume Vi(l ~ i ~ m ~ A(i] ~ C(i)] A Vi(l ~ i ~ m ~ C(i] ~ B(i)] is true upon exit from the loop. Then, if, for example, i = m and j = 1 upon exit from the loop, A3 used along with other information could result in Vi[l ~ i ~ i ~ A[i] ~ C[i)] A Vi(j ~ i ~ m ~ C[i] ~ B(i)] as the loop assertion.

B. Bottom-up approach.

In order to identify which heuristics to use, we must differentiate between two methods of computation: a) If the exit test has the variable i compared with a term which is not changed inside L, and i is incremented monotonically inside L, then it is assumed to be a counter controlling the loop in an "iterative going up" computation.

b) If the variable i is compared with a term which does not change in the loop, and is decremented monotoni­ cally inside L, then i is a counter controlling the loop in an "iterative going down" computation.

In the rules below we assume all loops have the index i, and let i 0 denote the value of i when it first reaches the cutpoint of the loop, while i 1 denotes the value of i upon exit from the loop. As in Section II, we assume that the cutpoint is located immediately before the exit test.

We first list the rules for finding the <j-index>. rule Xl. If i is a counter (incremented by 1) in a "going-up" iteration and is also the variable which appears in the index of array elements receiving assignments, then try assertions of the forms Vj[i 0 ~ j < i ~ <j-array>) or 3j[i < j ~ i 1 A <j-array~ in the inductive assertion. These will also be the form of the predicate p which is true after exit from the loop.

If i 0 is known, say i 0 = c upon entrance to the loo~ then the c should be substituted for i 0 in Q and p. Similarly, if i 1 = d upon exit from the loop, d should be substituted for i 1 ·

rule X2. If i is a counter (decremented by 1) in a "going-down" iteration and is also the variable which appears in the index of array elements receiving assignments, try assertions of the forms Vj [i < j ~ i 0 ~ <j-array>] or 3j [i 1 ::; j < i A <j-array>). As in rule Xl, p will also have the above form and i 0 or i 1 should be eliminated if possible.

rule X3. Discover whether Xl and X2 fail only because i is assigned a function f (i) rather than merely incremented or decremented by 1 in the loop. If so, try to find the set of elements which i assumes during the loop (using rule I2). The assertion will have the same form as in Xl or X2, except that the <j -index> will include the I2 invariant. For example, if i + i+7 in the loop, and i is initially zero, then the assertion is Vj{O ~ j < i A 3n[n >- 0 A j = 7·n] ~ <j -array>} ·

The following two conditions are used to decide which of the bottom-up <j -array> rules to apply assu­ ming that the <j -index> has already been determined.

(a) All assignments in the loop are to array ele­ ments with indices not specified by the <j -index> before executing the loop. That is, once we have in­ cluded an element of the array in the assertion after some circuit, we will make no more assignments to that element in subsequent circuits around the loop.

For example, the program segment above could be part of a "bubble-sort" program. The "one-pass" assertion is clearly S[i-1] ~ S[i] , but if the form of the assertion before executing the loop is Q : Vj[2 ~ j < i ~ <j-array>] the loop violates condi­ tion (a) because S[i-1] may receive an assignment and i-1 is already in the domain of the <j-index> .

(b) The "one-pass" assertion can be written as a single conjunct . Furthermore this conjunct is valid for all array elements whose indices are added to the domain of the <j-index> by one circuit through the loop. Thus if the "one-pass" assertion is S[i] = S[i+l] A S[i+l] ~ S[i+2] and i and i+l are added to the <j -index> by the loop, the condition (b) is not fulfilled because it cannot be expressed by an appro­ priate single conjunct.

rule Rl. If both (a) and (b) are true the "one-pass" assertion itself is taken as the <j - array>. Of course, the quantified variable of the <j-index> must be sub­ stituted for the actual array ind~x which appears in the loop. For example, if we have found the assertion to be Vj[l ~ j < i ~ <j -array>] and in the loop we have only A[i] + 0 and then i + i+l, the "one-pass" asser­ tion is A[i) 0 , and (a) and (b) hold. Thus we obtain Vj[l ~ j < i ~ A[j) = O] as the loop assertion .

The following rule is based on the fact that we have already established the desired form of the <j-index> part of the assertion. We want to be able to write one conjunct, say Vj[l ~ j < i ~ <j-array>], where the <j -array> will be a statement about (only) the array elements with indices 1 ~ j < i and not contain any additional restrictions on the indices.

rule R2. (generalization) If (a) is true, but (b) is not, check whether (b) fails only because the assertion is not a single conjunct. If so, the <j - array> parts of all the conjuncts in' the assertion are searched to find the strongest single conjunct which is true for all array elements specified by the known <j -index>. This conjunct becomes the <j-array> . For example, given a one-pass assertion

Vj[l ~ j < n ~ A[j-1] < A[j]] A A[n-1] ~ A[n] and a required Q of the form Vj[l ~ j < n+l ~ <j-array>], the correct <j - array> by this rule is A[j-1] ~ A[j].

rule R3. If (b) is true, but (a) is not, take the "one-pass" assertion as the <j-array> and consider the effect of an additional pass through the loop on this predicate. Then apply the generalization rule R2 to the result. For example, for the segment of the bubble-sort program introduced above, the one-pass assertion yields Vj[2 ~ j < i ~ S[j -1] ~ S[j]) · One circuit will change this to:

Generalizing this predicate by R2 is a relatively difficult step, not yet completely investigated. The generalization procedure would be expected to recog­ nize that no predicate comparing each element with its neighbor is possible, since no information is available about the relation between S[i-2] and S[i-1]. Then the transitivity of the inequality would yield that Vj [1 ~ j < i ~ S[j] ~ S[i]] is the strongest claim which can be made about the entire segment.

C. Examples.

Example 4. Minimum of an Array. The program in Figure 4 will find the minimum of an array A using an

I

array S in an unusual way. (The upper half of the array is set to A, and the computation takes place in the lower half, using only comparisons.) For the first loop, top-down rules give no information, so we use bottom-up rules. By Xl, we will try the assertion 'v'j[l ~ j < k :::> <j-array>] (because k 0 = 1, and we have a "going-up" iteration). The "one-pass" asser­ tion is clearly S[n+k] = A(k], and conditions (a) and (b) are fulfilled. Thus by rule Rl we obtain Q 1 : 'v'j[l ~ j < k :::> S[n+j] = A[j]]. Since upon exit from the loop k = n+2, we have

p : 'v'j[l ~ j ~ n+l :::> S[n+j] = A[j]]. By rule En2, p is added to Q 2 · We try rule Exl on w', but S[l] is undefined on entrance to the loop, so the rule fails.

Using array top-down rules, we first rewrite w' as 3j[l ~ j ~ 1 A S[j] = min(A[l], ··· ,A[n])] by rule Al. Using A2, we would like to retain the <j -array> part in an assertion true on entrance to the loop. By the definition of min we know that one of the elements is the minimum, and the p we have at the entrance to the loop states that A has been copied to the upper half of S. Thus we obtain 3j[n+l ~ j ~ 2n+l A S[j] = ·min(A[l], ··· ,A[n])] as the initial assertion which must be true. Since the assignment before the loop implies that i = n upon entrance to the loop, a possible substitution by A3 is q : 3j(i+l ~ j ~ 2i+l A S(j] = min(A(l], ··· ,A(n])]. Since i = 0 upon exit from the loop, this q becomes identical tow'. (Any of the other possible substi­ tutions of i for n will fail to match w' .) Thus we let Q 2 be q A p. The second conjunct is not needed to prove w' , but can be retained to provide the addi­ tional information that the upper half of S is un­ changed by the second loop, and contains A.

Example 5. Partition Program. The program of Figure 5, due to Hoare, will find a partition of the elements of a real array s. We would like to show that it is partially correct with respect to~ · : n::: 0 and ljJ : 'v'aVb{O ~a< i A j < b ~ n ~ S[a] ~ S[b]} A j < i, We use the bottom-up approach, seeking a Q 1 for the large outer loop. Thus we consider one pass through the loop. (It should be noted that the in­ variants we will find at cutpoints 2 and 3 during the "linear" pass are not necessarily the desired Q 2 or Q 3 for the overall execution of the program.) The first inner loop yields immediately by rules Xl and Rl, the invariant p 1 : 'v'k[i 0 ~ k < i ~ S[k] < r]. Thus upon exit from the first inner loop p 1 A S[i] ::: r is true. Similarly, after the second inner loop, we ob­ tain p 2 : 'v'~[j 0 ::: ~ > j ~ S[~] > r] A S[j] ~ r by X2 and Rl. There is no possibility that the second loop could disturb the claim of p 1 , because there are no assignment statements to the array in the loop. Moving p 1 A p 2 A S[i] ::: r A S[j] ~ r through the two possibilities for the test i ~ j, if we reach point A, the assertion is unchanged while at point B we have ' 'v'k[i 0 k < i-1 ~ pl ~ S[k] < r] A S[i-1] ~ r and ' p2 'v' ~ [jo ~ ~ > j+l ~ S[~] > r] A S[j+l] ::: r Rules Xl and X2 indicate that we require

*

p 1 'v'k[i 0 ~ k < i ~ <k-array>] and * P 2 'v'~[j 0 ::: ~ > j ~<~-array>], Thus by R2 we seek weaker array assertions about the entire range of k and ~ which will fulfill these forms. The weakest assertion made about an element in p or p 1 is that * 1 S[i-1] ~ r. Thus we let p 1 be * 'v'k[i 0 ~ k < i ~ S[k] ~ r]. Similarly p 2 is 'v' ~ [j 0 ::: ~ > j ~ S[~] ::: r] · Since i 0 is initially 0, while j 0 is initially n, we assume a Q 1 assertion of the form 'v'k[O ~ k < i ~ S[k] ~ r] A 'v'~[n >- ~ > j ~ S[~] ::: r], By rule En2, Q 2 and Q 3 will be given the assertion of Q 1 , and verifying these assertions will show the program partially correct. We clearly could have used the transitivity rule here, but for this example, the amount of work required is about the same.

IV. Conclusion

Clearly, the rules and examples given in this paper are far from being a general system for finding induc­ tive assertions. More and better rules are needed, particularly for array assertions, which tend to be complex and unwieldy.

In addition, before the rules can be incorporated into a practical framework, we must order their appli­ cation. That is, at each step we must provide more exact criteria for deciding which rule to apply and on which cutpoint of the program. The order in which the rules are presented in each subclass does implicitly provide a partial specification. Thus we presently would try to apply Exl, and only if it failed try Ex2, etc. Moreover, we generally would try to gather in­ formation on simple variables using the rules of Sec­ tion II before attempting to treat array assertions.

The more basic (and open) questions are (a} whether to attempt top-down or bottom-up techniques first for a given loop, and (b) which loop of a program should be treated first. Although we experimented with various orderings in the examples in this paper, we have tentatively formulated a more fixed approach. Our present inclination is to first use top-down rules from the (physical) beginning of the program. (Since in general there is more th.an one outer loop, usually only entrance rules are applicable.} Then we use bottom-up rules for the same loop, to create a p true after exit from the first loop containing as much in­ formation as possible. We continue with the next outer loop in a similar manner. If, however, we are stymied and unable to find a loop assertion, we start with top-down rules from the end of the program, and try to work backwards towards the beginning.

A more sophisticated approach would require a weighted evaluation function capable of making a very cursory scan of the program. This function would identify loops which seemed 'promising', i.e. likely to yield valuable information rapidly, and apply sele~ ted rules first to these loops.

Since some of the rules could continue searching for a possibly non-existent form of assertion ·almost indefinitely (the transitivity rule, for example), such rules would have a "weak" version and a "strong" version. The "weak" version would be used in the initial attempt to find an assertion, and would "give­ up" rapidly if it did not provide an almost iiiiiilediate solution. Then other, possibly more appropriate, rules may be tried on the cutpoint. Only if all rules failed to add relevant information, would the "strong" version be applied. This division is parallel to the human attempt to first find what is "obviously" true in the loop, and only afterwards bring out the fine points.

The overall strategy we have adopted in this paper has been to find assertions strong enough to prove the partial correctness in as few steps as possible. Thus, in general, we attempt to directly produce a near-exact description of the operation of a loop, without going through numerous intermediate stages where we are unable to shm· either validity or unsatisfiability. If our heuristic is wrong, this fact will be revealed relatively rapidly by generating an unsatisfiable veri­ fication condition. We then may try a weaker alter­ native claim. We feel that this is the approach which should be taken in order to construct a practical system which co~ld be added to a program verifier.

We believe that the bottom-up approach may also be used to solve other problems. For example, in the partition program (Example 5), the inductive assertion was actually found without using the w given by the programmer. In one single step w may be generated from Q 1 , and thus we have 'discovered' what the program does without the use of additional information. This feature of the bottom-up approach can probably be most useful for strengthening a too-weak assertion, i.e., revealing that the program does more than is claimed in w ·

Another apparent application is for proving termi­ nation using well-founded sets. For termination, predicates Qi and functions ui are required, where ui (a mapping to the well-founded set) has its domain bounded by Qi and descends each time the loop is exe­ cuted. Here again the bottom-up approach is useful since no w is provided. We have already begun inves­ tigating bottom-up methods for generating both the Qi 's and the ui 's which will ensure termination.

The ultimate goal of automatic assertion generation is almost certainly unattainable; thus the optimal system would involve man-machine interaction. Whenever i t was unable to generate the proper assertion, the machine would supply detailed questions on problematic relations among variables and possible failure points (incorrect loops) of the program. Clearly, a partial specification of the assertions, provided by the programmer, could shorten this entire process.