Heuristic Methods for Mechanically Deriving Inductive Assertions

Introduction

Mechanical verification of program correctness is desirable and possible.l Given a program, a first-order axiomatization of its semantics, and predicates on the input, output, and ~ach l?op, verifi7ation of the output pred~cate ~s a mechan~cal process. (c. f. (2) and [3) for recent surveys).

Input and output predicates are necessary and natural for a programmer to supply. However, completely specifying the predicates on loops is tedious, error-prone, and· redundant. It is tedious due to the large amount of · stereotyped detail required. It is error-prone* partly because of the tedium and partly because the notation is less natural than that for procedural steps. It is redundant since the predicates repeat information which is manifest in the program. The purpose of this paper is to show that loop predicates can be derived mechanically** and that partially specified loop predicates can be completed mechanically.

*An example may lend some weight of experience. In his thesis4, King presents nine programs submitted to the verifier; the most complex of these {Example 9) has an incorrect loop predi­ cate, i.e. the inductive assertion is too weak to be consistent or to imply the desired output predicate. {Since the theorem prover rejected the loop predicate due to an inability to handle multiple quantification, the predicate error was overlooked.)

**In one sense, this is trivial. All well­ formed predicate expressions for each loop can be enumerated and proofs of correctness dovetailed until one succeeds. If every valid theorem of the subject domain is provable, this will eventually verify the program; otherwise, mechanical verification is not possible in general. Such a procedure is, however, computationally intractible.

tAlso at Harvard University, Cambridge, Mass.

HEURISTIC METHODS FOR

MECHANICALLY DERIVING INDUCTIVE ASSERTIONS

Ben Wegbreitt

Bolt Beranek and Newman Inc. Cambridge, Massachusetts

. Elspas, Green, Levitt, and Waldinger 5 have ~ndependently worked on this problem using difference equationg as an aid to specifying assertions. Cooper has previously studied the problem and observed that an inductive ~ssertion . can be obtained by hand by construct­ ~n~ the f~rst few terms in the loop expansion, wh~ch generally shows what the infinite union must be. ·

Our method uses a different approach. To generate loop predicates where none are supplied, the output predicate is dragged backward through the program and modified when passing through program units, to produce trial loop predicates. Trial loop predicates which are ·loop inconsistent are modified according to various heuristics, to generate better trial predicates. Hence, it is also possible to accept a programmer-supplied inductive assertion which gives the "essential" idea of some loop and mechanically fill in the deta~ls to arrive at a complete, correct loop pred~cate. Many of the heuristics are domain specific, this paper uses integers and integer arrays as the subject domain.

The paper is divided into five sections. Section 2 illustrates our approach with two simple examples. Section 3 discusses the general method, domain-independent heuristics, and heuristics specific to the integers. ·section 4 treats a number of complex examples to show how the heuristics are used and exhibit their coupling. Section 5 discusses implementation and application of this method.

Notation. Throughout, a simple flowchart language is used. The input predicate is denoted by ~; the output predicate by ~. Unprimed {primed) variables and predicates denote values and predicates on these values before {after) control flows through a set of flowchart boxes. The transformation due to a flowchart path Ail Ai2···Ain is denoted by

o (i 1 ,i 2 , ·· · in).

Simple Examples

The flowchart of Figure 1 {taken from [1]) computes the quotient Q and remainder R of integer X divided by integer Y. ~={X~0 A Y>~}, ~={X=QY+R A 0~R A R<Y}. ~ at the entrance implies that at arc A 0 the predicate P 9 ={X~0 A Y>0 A Q=0 A R=X} holds. To verify the flowchart, it suffices to find a loop

predicate P1 at arc A1 such that

• {El) p 0 -+ pl
• {E2) P 1 A o{l,2,3,ll p , 1
• {E3) Pl A 0{1,4) -+ v

The standard means for generating a loop predicate is to use E3 and start with trial choice of P 1 ={o(l,4) -+ ~'}. Here, this gives Pl={R<Y -+ {X=QY+R A 0~R A R<Y) }. Converting to disjunctive form and simplifying, P 1 ={R~Y v (X=QY+R A 0~R) }· To verify the flowchart, it suffices to prove that with this choice of P 1 , E1 and E2 are each valid. E1 is {X~0 A Y>0 A Q=0 A R=X} ~ {R~Y v (X=QY+R A 0~R) }

which is valid. However, E2 is

{R~Y V (X=QY+R A 0~R)} A R~Y A R'=R-Y A Q'=Q+1 ~ {R'~y V (X=Q'Y+R' A 0~R') }

which, while satisfiable, is not valid. Since E2 is satisfiable, this suggests that the trial choice for P 1 be replaced by a stronger one. Dropping a d~sjunct is a possible strengthening transformation; plausibility arguments suggest that the disjunct to drop is the one arising from o(1,4). Hence consider the next trial choice P 1 ·{X·QY+R A -~R}. E1 remains valid; E2 becomes

{X=QY+R A 0~R} A R~Y A R'=R-Y A Q'=Q+1 ~ {X=Q'Y+R' A 0~R'}

which is also valid. Hence, this choice of P1 is said to validate E1 and E2, and the flow­

chart is verified.

The flowchart of Figure 2 (taken from [4]) computes AB by a binary decomposition of B. ~={X=A A Y=B A Y~0}, ~={Z=AtB}. From ~ it follows that P0={X=A A Y=B A Y~0 A Z=1} holds at arc AQ. Using the exit condition E3, the first tr~al choice for P 1 is {Y=0 ~ Z=AtB}. This validates the entrance condition E1. The loop condition E2 generates an implication for each loop path. The one on A 1 A2AsA 6 A7A1 is valid. The one on A1A2A3A4A6A7A1 requires

{Y;S v Z·AtB} A Y;S A Y MOD 2·1 A Z'=Z·X A Y'=Y.+2 A X'=X·X ~ {Y';0 V Z'=AtB}

which is not valid but is, however, satisfiable.

The occurrence of an invalid but satisfiable E2 implication indicates that the first trial loop predicate is too weak. Hence, heuristics are used to generate a stronger P 1 from the approximation {Y=0 ~ Z=AtB}. The appearance of antecedent Y=0 with a consequent equality suggests three likely candidates for a stronger P1: {Z=AtB+K~Y}, {Z=(AtB) · (KtY) }, and {Z·(KtY)=AtB}, where K is unknown. E1 and E2 are used to decide which, if any, of the three are consistent loop predicates and to solve forK in the consistent cases. Using the third choice for Pl in E1 gives {X=A A Y=B A Y~0 A Z=1} ~ {Z·(KtY)=AtB} which is valid if K=A or K=X. Using the choice K·X in P1, E2 gives

{Z·(XtY)=AtB} A Y;0 A Y MOD 2;1 A Y'=Y+2 A X'=X·X ~ {Z·(X'tY')=AtB} and

{Z·(XtY)=AtB} A Y;0 A Y MOD 2=1 A Z'=Z·X A Y'=H2 A X'=X·X ~ {Z· (X'tY')=AtB}

both of which are valid. Hence, P1= {Z·(XtY)=AtB} verifies the flowchart.

General Considerations for Single-Loop Flowcharts

Consider a flowchart belonging to the schema of Figure 3. The initialization, loop-body, and terminal-computat~on are arbitrary loop-free computations. From ~ and the initialization, the strongest predicate P 0 on arc A0 can be derived mechanically. To verify the flowchart, it suffices to find a loop predicate P 1 at arc A1 such that

• (E1) P 0 ~ P 1 '
• (E2) P 1 A 0(1,2,3,1) ~ p , 1
• (E3) P1 A 0(1,4,5) ~ v

In view of E3, the weakest possible choice for PJ is P1={o(l,4,5) ~ ~'}. ~hould E1 be invali with this choice of P 1 , the flowchart is not verifiable. E2 generates an implication for each path between A 2 and A3 : if all are valid, the flowchart is verified; if any are unsatisfiable, the flowchart is not verifiable; if all are satisfiable but some are invalid, then P1 must be replaced by a stronger inductive assertion.

There are two domain-independent heuristics for obtaining a stronger loop predicate from a previous approximation.

(Gl) Convert to disjunctive form and drop some of the disjuncts which come from the exit predicate D. Typically, drop those disjuncts which cannot be used in any of the domain­ specific heuristics described in the next

section.

(G2) If {P1 A o,: ~ P1' I i=k1, ··. kn} are the

invalid but sat~sfiable E2 implications, then replace P! by P1 A (Okl ~ P1') A ··· A (okn ~ P1 ) }. If appl~ed blindly and repeatedly, this can lead to an infinite sequence of trial P1's; hence, this must be used to limited depth, in concert with heuristics for "simplifying" the expressions. (e.g. Il through I4 below)

Whenever a new choice for P1 is obtained by some heuristic from a previous approximation, it is tested in E1, E2, and E3. 'El not valid indicates that the choice is too strong. This is generally a good filter giving a quick reject to incorrect predicates; since the set of trial predicates should be pruned whenever possible, this is useful. E3 not valid indicates that the choice is too weak. An unsatisfiable implication due to E2 indicates that the choice is too strong. An invalid but satisfiable E2 implication indicates only that the choice is wrong.

There are three other useful domain­ independent heuristics:

(G3) To verify a predicate, convert to con­ junctive form and verify each conjunct separately. This may be a losing strategy if two or more conjuncts are coupled and can only be proved in concert, but when this works, it reduces the size of the formulas to be manipulated and hence cuts the computation for a proof and the search space for other heuristics. This independent processing of conjuncts applies both to ~ and to the results of G2. In the latter case, the new trial loop predicate is the conjunction of the previous one and a set of new clauses, so this is a natural situation in which to try separation.

• (G4) If the application of G3 results in verifying some but not all of the conjuncts, record those which do veri~y as consis~~~~ loop predicates at that arc. When subsequently searching for the proof of an inductive assertion at some arc Ak, the list of predicates previously verified at Ak may be a useful source of lemmas. Suppose, for example, that a trial predicate at Ak is {ckl A ck2} and that ckl is loop consistent while Ck2 is not. If {ckl A ck2} is not verifiable, and a new trial predicate is formed, verification of the new predicate may be aided by knowing that ckl holds at Ak.
• (G5) Each predicate which is found to hold at some arc Ak is propagated to all successors Aj under the transformation o(k,j). This includes both the input predicate ~ and the results of G4.

Because of G5, the first step of flowchart verification is to extend ~ so far as possible, forming the assertion P 0 at one input to the first loop junction (c.f. Figures 1 and 2). Whenever, because of G4 or G5, it is known that some predicate P1 holds at A1, P1 is cojoined as a clause on the left nand side of E2 and E3.

Integer-Specific Heuristics

Turning to domain-specific methods, the heuristics are richer and more powerful. The following heuristics apply to the integers (and to the reals, except as noted otherwise). They each replace a predicate by a weaker one; when used inside a negation (as is commonly the case) their application results in a stronger inductive assertion.

• (I1) In a conjunction of inequalities, form transitive closures and drop the conjuncts used. For example, replace*
• (I2) In a conjunction of an equality and an expression & equal to zero, a term in & may be added to one side of the equality, e.g. replace

where K is unknown. Less common, but possible is: multiply one side of the equality by K&, e.g. replace

{ (KtX) ·A=B·C}.

(A similar case is the conjunction of an equality and an expression & equal to 1: either side of the equality may be multipled by &. In practice, this turns out to be useful less frequently than the zero case.)

• *In the case of reals, the last of these is changed to: replace

(I3) In a conjunction of an inequality and an existentially quantified conjunction, use transitivity to extend the range of the quantified variable, and drop the inequality conjunct. For example, replace

(I4) In a conjunction of an inequality and a universally quantified disjunction, use transitivity to extend the range of the quantified variable and drop the inequality conjunct. For example,

{I~N A VK[K~N V Q(K)1 II ··· }

may be replaced by the weaker form

Multiple Loops

The next level of loop complexity beyond the single loop schema is the class of simpl~-nested loop programs, in which the loop- ody of Figure 3 contains inner loops. Consider, for example, the schema of Figure 4 where the inner-bod~ and outer-body are loop free. To ver1fy th1s, it suffices to find an inductive assertion P4 such that:

• (E4) P 0 11 6(~,1,2,3,4) -+ P4~
• (E5) P4 11 6(4,5,6,4) -+ P 4 ~
• (E6) P 4 A o(4,7,8,1,2,3,4) -+ p ~ 4
• (E7) P4 A 0(4,7,8,1,9,1~) -+ v

!he weakest possible ch~ice for P4 is P4={~(4,7,8,1,9,1~) -+ ~ }.

This class of flowcharts is of interest for two reasons. (1) It and its generaliza­ tions to depth n occur frequently, (2) Obtain­ ing a solution for P4 requires no new techniques, since E5 and E6 each have the same form as E2 - the set of implications they generate cover the set of poesible paths from arc A4 to itself - and the nesting is otherwise irrelevant. These considerations extend to simply-nested flowcharts of arbitrary depth.

In general, the situation is less clean. Consider, for example, the schema of Figure 5. Here, there is no single innermost arc: A3 and A7 are each innermost. The verification conditions are

Finding P 3 and P7 is complicated by the coupling due to E10 and E12. Loops such as these can sometimes be decoupled by the following heuristic.

(G6) Approximate the first loop by a finite expansion to some depth i -- one disjunct per time around the loop. Use this to find a valid inductive assertion on the second loop. Then use that assertion to obtain the assertion for the first loop. For example, the loop <3,4,5,3> may be approximated to depth i=l by

P7 must validate

• (E2a'l p7 A 6(7,8,9,7) -+ p7 ,
• (E1 ') Po A ~D 1 A !J.. -+ p7 , '!.
• (E2b') p7 A o(7,8,10,1,2,3l A !J.. -+ p7 , '!.

which is in standard form. With P 7 obtained, P3 is determined by E8, E9, E10, and E12.

More Complex Examples

The flowchart of Figure 6 (taken from (4]) sets the flag variable J to 0 or 1 as A is or is not prime. P 0 =. {A~2 A I=2}, w={[J=0-+ VK(2~K<A-+ A MOD K¢0)] A [J=1 -+ A MOD I=01 }. Using E3, the weakest possible inductive assertion at arc A1 is P1={((I~ A J'=0) V (I<A A A MOD I=0 A J'=1)] ... w'}.

Simplifying this, and converting to disjunctive form

P1={I<A v VK(2~K<A -+ A MOD K¢0) }.

(The disjunct J'¢0 has been dropped, sin2e it involves primed va~iables.) Since P 0 = ~1' E1 is validated. P1 A 6(1,2,3,4,1) -+ P1 is invalid but satisfiable. To obtain a stronger inductive assertion, I3 is used to replace ~{I~ A 3K(2~K<A A A MOD K=0} by the stronger predicate ~{3K(2~K<I A A MOD K=0}. That is,

the next trial P 1 is

This validates E1 and E2, so the flowchart is verified.

The flowchart of Figure 7 (taken from [2]) computes* the fractional quotient P/Q to within tolerance E. $={0~P<Q A 0<E} so that P 0 ={0~P<Q A 0<E A A=0 A B=Q/2 A D=1 A Y=0}; w={P/Q-E<Y~P/Q}. Using E3, the weakest possible loop predicate at A 6 is

This validates implication E1, since P 0 A o(~,1,2,3,5,6) -+ P6: and P 0 A o(0,1,4,5,6) -+ P6'· E2 generates two implications

With P 6 , neither of the~e is valid but both are satisfiable, hence P 6 must be replaced by a stronger predicate.

In determining the correct P6, it is helpful to use heuristic G3: break w into two conjuncts and verify each separately. consider first

·In th~s example, the doma~n ~s the reals, rather than the integers. The techniques carry over with only minor changes in the treatment of transitivity.

With this choice of P6 , both 7.1 and 7.2 are , invalid but satisfiable. In replacing p61 by a stronger predicate, heuristic I1 is used to get ~{P/Q-D>Y}, i.e. {P~QY+QD}. With this choice of P 6 , E1 and 7.1 are each validated, while 7.2 is invalid but satisfiable. Since 7.2 is {P~QY+QD A D~E A P<A+B -+ P~QY+QD/2}, heuristic G2 suggests the next trial choice for P6 is

{[P~QY+QD] A [D~E A P<A+B -+ P~QY+QD/2]},

while heuristic G3 suggests verifying the two conjuncts separately. When G2 and G3 are applied together, it suffices to verify the new conjuncts (here, second conjunct) · With PG={D<E V P~A+B v P~QY+QD/2}, E1 is validated while 7.1 and 7.2 are each invalid but satisfiable. This suggests using a heuristic to get a stronger predicate; I1 and G1 applied to ~{D~E A P<A+B A P>QY+QD/2} give ~{A+B>QY+QD/2}.

Using this for P6 , E1 is validated while 7.1 and 7.2 are each invalid but satisfiable. Using G2, I1, and then G3, 7.1 and 7.2 respectively give rise to the new conjuncts {B~QD/2} and {B~QD/2}.

Combining these into the single conjunct {B=QD/2} and using this for P6 , E1, 7.1 and 7.2 are each validated. Hence the output conjunct wl={P/Q-E<Y} is verified with the loop predicate p6 1m{P~QY+QD A A+B~QY+QD/2 A B·QD/2}.

The second output conjunct w2={Y~P/Q} is simpler. Successive conjuncts generated for P62 are {Y~P/Q}, then {A+B~QY+QD/2}, and finally {B=QD/2}. As in the case of P 6 1, the primary choice at each step is between using G2 to add another conjunct and some other heuristic to simp~ify by strengthening a conjunct. Since w'~- is verified by P 6 i for i=1,2, the flowchart is verified. Combining p 6 1 and p 6 2 gives P 6 ={P/Q-D~Y~P/Q A B=QD/2 A A=QY}.

Figure 8 (taken from (4]) gives a simple exchange sort.

Po=~; w={VM 2~~N-+ A[M-l]~[M] }. As A3 is the unique overlap arc of the two loops, the inductive assertion is formed there (c.f. Section 3.3). From E3,

P3={I>N A J=0 ... w'} = ~{I>N A J=0 A 3M(2~M~N A A [M-1] >A [M]) } ·

This validates E1, trivially. E2 generates three implications:

• (8.1) P3 A o(3,10,11,1,2,3) -+ P 3 '

• ( 8. 3) P3 A 0(3,4,7,8,9,3) p , 3

With P 3 , these are invalid but satisfiable. Hence, it is necessary to replace P 3 with a stronger assertion.

Using heuristic I3,

This choice of P 3 validates E1 and the three implications of E2. The most difficult proof is for 8.3:

{J¢0 v VM(2~M<I -+ A[M-1]~A[M))}

A I~N A A(I-l]~(I) A I'=I+1 -+

{J¢0 V VM(2~M<I' -+ A[M-1]~A[M)) }.

which requires a case analysis on the quanti­ fied variable M.

Conclusion

Having shown that it is possible in some number of cases to derive the inductive assertions by heuristics, we turn to the application of this in a mechanical verifica­ tion system.

Implementation

We have not yet implemented this technique and the above examples are the result of hand simulations. It appears that programming this is reasonable, although by no means trivial.

Modifying the trial loop predicates and searching the space of possible modifications is the heart of this method. A problem-solving language (e.g. [7), [8) or (9]) with facilities for pattern-matching, backtracking, and multiple environments is the preferred implementation tool. The need for pattern­ matching to invoke heuristics, and backtracking to make retractible trials should be clear. Experience with hand simulation suggests that additionally a breadth-first search capability (i.e. multiple environments) is required, since an incorrect choice of heuristic often leads not to a recognizable failure but rather to a nOii='convergent series of loop predicates ~ each inconsistent.

. The theorem-proving required is within the range of contemporary domain-specific theorem provers (e.g. [10)). This can also be programmed in the problem-solving language.

The interface between heuristic predicate generation and theorem proving can be organized in two ways. A disjoint organization would separate the two and use the theorem prover as an oracle returning one of four replies for any formula submitted to it: valid, unsatisfiable, invalid-but-satisfiable, or can't-tell (escape clause for undecidable domains) · A better organization is based on the observation that the heuristics used in trial predicate generation and in theorem proving are often the same and that this can be exploited by combining the two more closely. Further, in seeking to validate an E2 implication with some trial predicate, the theorem prover may generate a number of clauses which are invalid but satisfiable; it is often useful to take these as new goals and try them as additional conjuncts in the next trial predicate (i.e. a variation on G2).

Application

We do not believe that the proposed techniques will be capable of generating all inductive assertions on a large, complex program in a reasonable time scale. Rather, we assume that a program submitted to a verifier will have its loops tagged with assertions of varying degrees of completeness: some complete, some partial, and some untagged. In general, interaction will be required in developing correct assertions and proving very difficult lemmas. It is desirable, however, to do mechanically as much as practical. The proposed technique allows completing certain loop predicates and generating certain inner predicates from outer ones. This should suffice to fill in a significant portion of the inductive assertions mechanically and, therefore, should expedite the task of proving programs correct.

ACKNOWLEDGEMENTS

The author would like to thank L. Peter Deutsch, Carl Hewitt, Ralph London and Jay Spitzen for discussions concerning various aspects of mechanical program verification. Ralph London is the source for the observation of predicate incompleteness in the example discussed in Section 1.

This research was supported by the Advanced Research Projects Agency of the Department of Defense under Contract No. DAHC-71-c-0088.