Automatic Program Annotation

AUTOMATIC PROGRAM ANNOTATION

Nachum Dershowitz Stanford Artificial Intelligence Laboratory Stanford, California 94305

ABSTRACT

Techniques were developed by which an Algol-like program, given together with its specif ications, may be documented automatically. This documentation expresses invariant relationships that hold between program variables at intermediate points in the program, and explains the actual workings of the program regardless of whether the program is correct. These techniques, formulated as deduction rules for both guaranteed invariants and candidate invariants, represent a unification of existing approaches, and sometimes improve upon them.

INTRODUCTION

Program annotation is the task of discovering a set of invariant assertion· and documenting a program with them. These invariants describe the workings of the program, independent of its correctness or incorrectness, by detailing relationships between the different variables at specific points. Not only are invariants necessary for the verification of a program by the invariant-assertion technique, but they may also be used .to prove termination or incorrectness of a program, to analyze the efficiency of the program, aid in the optimizat ion of the program, and guide program debugging and modification.

This research is aimed at unifying previous approaches to annotation (e.g., Wegbreit [1974] and Katz and Manna [1976]) and extending some of the earlier techniques. The methods developed have been implemented in QLISP and a catalog of annotation rules has been compiled.

THE RULES

The annotation techniques are expressed as rules, each rule consisting of a set of antecedents and a consequent: There are two basic types of rules: algorithmic and heuristic. ·

• Algorithmic rule· derive invariant relations between variables directly from the program statements. These rules may be further subdivided into two categories:
• assignment rulea, which yield global invariants that hold at all labels in the program, based only upon the assignment statements of the program;
• control rulea, which yield local invariants associated with specific points in the program, based upon the control structure of the program.
• Heuristic rulea have candidate invariants as their consequents. These candidates, though promising, are not guaranteed to be invariants and must be checked by a verifier. Initially all programmer supplied assertions are candidates.

The assignment rules relate to particular operators occurring in the assignment statements of the program. For example, there are three rules for multiplication: a multiplication rule, which gives the range of variables which are updated by multiplication by a constant expression; a aet multiplication rule for the case where a variable is multiplied by other variables whose ranges are already known; and a multiplication relation riLle which relates variables that are always multiplied by similar expressions. Corresponding rules are formulated for other operators.

Consider the multiplication rule, P: u := uO I u·ul I u·u21 . ..

P: { u ' uO·ulN·u2N·... }

The antecedent states that the only assignments to the variable u in the program P are u := uO , u := u·u1 , u := u·u2 , etc., where the expressions uO , u 1 , u2 , . . . are of constant value within P. When this condition holds, the global invariant u £ uO·ulN·u2N· . . . holds throughout execution of P. That is, once u has been assigned a value in P, it belongs to the set uO·ulN·u2N· . . . , where N is the set of natural numbers and for any expression a, a(Sl,S2, ... ,Sm) denotes the set of elements a(sl,s2, . .. ,sm) such that s1 ' 51 , s2 £ 52 , . . · , sm ' Sm . From such an invariant, specific properties, such as a bound on u , may be derived. Note that no restrictions are placed on the order in which the assignments to u are executed.

An assignment u := a(s) , where it is known that s £ S, may be viewed as the nondeterministic assignmenf u :£ a(S) of an arbitrary element of a(S) to u . Thus the above rule might be considered as a special case of a more general 1et muliiplicction rule,

where TIS denotes the closure of S under multiplication, i.e., the set of products of elements of S. If S contains the single element s , then TIS = sN .

The following multiplication relction rulo relates different variables appearing in the program:

where a , P , .. . , are arbitrary (not necessarily constant) expressions. The simultaneous assignments in the antecedent of the rule may represent individual assignments executed along the same program path, such that whenever, for example, u := u·aU1 is executed, so is v := v·av1 for the aame value of the expression a .

While the previous rules completely ignored the control structure of the program, the control riLles derive important local invariants by taking the program's structure into consideration. For example, the rule

derives ·a loop invariant from the known invariants preceding the loop and following the loop body. It states that when control is at the head L of the loop- body, either the loop has just been entered, in which case the invariant A holds, or the loop-body has just been executed and B holds.

In contrast to the above rules, which are algorithmic in the sense that they derive relations that are guaranteed to be invariants, the other class of rules, heuristic rules, can only suggest candidate invariants. An example is the following generalization laeuriatic, which is valuable for programs with universally quantified output specifications. Given a loop invariant B(l<) at label L , where I< (a variable or expression) counts the number of loop iterations, we have as a candidate for a loop invariant that B holds for previous values of k as well. That is,

{ k = 0 } ; loop L: { B(l<) } ; S ; { I< = I<'+ 1 } repeat

L: {T B(O:I<] T} where I<' is the value of I< when last at L and B[O:k] is short for " B holds for all values between 0 and k ". The "{?" and "?}" indicate that the consequent is only a candidate which must be verified. Another example is the top-down heuriltic

loop 51 ; L: { A } ; until B ; 52 repeal ; {? C ?}

L: {T A " B ;) C ?}

which may be used to push candidates backwards into a loop.