The Conceptual Calculus For Automatic Program Understanding

1. INTRODUCTION

CAN is an implemented program understanding system. It is fully automatic and detects semantic properties :

• -unused portions of code, or undefined function epplicet ions
• classes of data for which a program execution never ter11inates
• programs whlch are underused in a given task

this diagnosis nor11al activity actlvlty is superimposed to CAN's assigning a meaning to a program.

CAN's undarlylng formal theory, the conceptual calculus, is basad on clausal form of predicate logic. It admits new types of variables (segment variables, typed element variables, index notations) and constructors (sequences, bags, sets) within terms, with associated equation solvers. It uses an induction rule whose task is to 1nduce properties of date from recursive equations [61, rather than to prove them. The application criteria of this lnductlon rule is a v1c1ous c1rc1e detector.

As opposed to program verification, which lies on veri flcatlon cond i tlons generation (VCG> [3,81 and theorem proving, program understanding lies on ·ta-eva1uat1on [17,41 and

• equat1on so1v1ng [5,7,15,161.

Mete-evaluation as daf lned in [5] is 11 generalisation of aymbollc evaluation [9,181.

2. FROM VERIFICATION CONDITION GENERATION TO MET A-EVALUA Tl ON

Statements subsume implicit structures which they access and modify (tables of identifiers, l/0 buffers, stacks, arrays). Symbolic evaluation pays a closer attention to these implicit structures than verificafion condition generation. Instead of being h ldden in log leal express lone, they are individualized as data abstractions. As an example, where assignment is reduced, within VCG, to a mere operation of substitution on a logical expression [81, symbolic evaluation uses an abstract data structure which models a table of identl flers. It permits to easily take in account different assignment modes, as they exist in programming languages.

But symbolic evaluation, as it is defined in most works, leaves some problems unsolved. A call to a LISP-defined symbolic evaluator of LISP expressions (as copied on existing ones [181), would appear as 1

<EVAL-SYMB express1on 1dent1f1ers-tab1e>

1dent1f1ers-tab1e would be a list of tuples :

<1dent1f1er . va1ue-of-1d>

Actual symbolic evaluators only allow va1ue.-of-1d to be mate-described. Meta-evaluation requires both 1dent1f1er and express1on to be eventually mete-described too (for instance, the SET function will introduce meta-described 1dent1f1ers in the 1dent1f1ers-tab1e. EVAL and the possibility to make programs build and use other programs, will both introduce meta-described expressions),

THE CONCEPTUAL CALCULUS FOR AUTOMATIC PROGRAM UNDERSTANDING

D. GOOSSENS Dept. d'lnformatique Universite PARIS 8 2, Rue de la Liberte 93526 St-DENIS Cedex 02

The eMtension from symbolic evaluation to aeta-evaluation is not simply a theoretical Improvement, but a practical need.

On another hand, the combined uses of EVAL and FEXPRs ello~ the programmer to define his o~n control structures; ne~ conditionals, iterations, repetitions and miscellaneous.

~e have adopted a formalism for representing program aeanings ~hich allo~s :

• any level of abstraction in the description of the environment of an aMpression to be meta-evaluated (including the eMpression itself).
• lncrementality : CAN's meta-evaluator is a set of conceptual representations of the basic LISP functions, statements, and control structures. It increases itself as it understands ne~ user definitions. The meta-evaluator transforms each ne~ LISP definition in a conceptual representation. This representation eMtends the understanding po~er of the meta-evaluator.

Our formalism is based on the clausal form of predicate logic [101; I.Je have adopted a ne~o~ syntaM. Clauses are replaced by concepts and functional terms by conceptual representations 117,51. One concept generally corresponds to several clauses, ~hich share ldentical subter~s. This ne~ syntaM is especially adapted to the induction rule of the conceptual calculus.

~e have also eMtended the classical reso1ut1on rule [141 to en equ111brat1on rule, ~here unification [141 is BMtended to equation solving. This aMtension has been first suggested by [131. Our equation solving systea includes unification under aMioms of :

• -associativity and commutativity [16,71
• -associativity [12,151

-associativity, commutativity, idempotence [111

• indeM notations [6,51

lndeM notations are obtained from the induction rule.

Meta-evaluation is a strategy ~hich eMciusively uses the equilibration rule. Equilibration perfor~s in a unified ~ay the various tasks of :

• 1- choosing ~hich concept applies on the current syntactic unit, in the eMpression to be aeta-evaluated. This confrontation process is en equation solving process, rather than a test, eince the syntactic unit may be meta-described.
• 2- evaluating the relevant parts of the current syntectic unit, as stated by the chosen concept.
• 3- conetrelning the returned values and modified environments, as asked by the chosen concept (this le still done by equation solving, and may cause ceee analysis),
• 4- constructing the resulting abstract environaent and value returned by the syntactic unit.

CAN is not simply a meta-evaluator. It uses perform, ~ith the help of induction, a analysis task. one to program

3. THE CONCEPTUAL CALCULUS

SYNTAX :

The basic syntactic units of the conceptual calculus era the concepts. A concept is a couple :

aJNCEPT = <LOGIc I CCNTRCL>

~here CONTROL is either

tara + tera

or tara + (BP tara . cant)

lhe <BP tare cant) form is a breakpo1nt. tare is e procedure call and cant is a set of subconcepts. Subconcepts are concepts. The distinction ~ill ho~ever be helpful for the eMposition of the equilibration rule.

The LOGIC component is a conjunction of literals. teres are simple pointers to the LOGIC component.

If the LOGIC component ~ere not syntactically distinguished from the control component, the LISP function ~ ~ould be conceptually defined as :

<MEMBER e1 e2) 1 <BP e1

M 1 <BP e2

(a1 ··· an)/ai-w 1 NIL

(e1 ... an w · y>lai-w 1 (w , y)))

This definition includes the evaluation of the arguments e1 and e2, and the purely applicative part of MEMBER. I.Jith the LOGIC-CONTROL distinction, it looks like (ti are eleaent variables) :

<{t1·<MEMBER t2 t3>

t2·e1

t3·e2} , t11<BP t2

<true , t41<BP t3

<<t5-(a1 ... an)

ei-t4

t6·NIL} , t51t6>

<{ t5· <a1 ... en · t7)

t7-<t4 · t8>

ei-t4} , t51t7>>>>>

SEMANTICS

~e have defined a semantics for concepts, ~hich associates a set of HORN clauses [101 to a concept. The results ~hich hold for clausal form of predicate

logic hold for the conceptual calculus.

In particular, the follo~ing equilibration rule corresponds to the resolution rule [141. The induction rule and the vicious-circle detector, ho~ever, have no kno~n equivalent.

RULES OF INFERENCE

Rule of equilibration

The equilibration rule ~ay be interpreted as a procedure invocation mechanism, based on equation solving. It states that the CONCEPT, or SUBCONCEPT

aey be replaced, ~ith the help of the CONCEPT <l1 1 t1+01>

(~hich ~ay be m itself), by the set of concepts

conto(<L1 1 t1+01>o<L2, t2+t3>)

Distribution of composition (Ci ere concepts) 1

Composition :

Clo<l , tl~<BP t2 · cant)> · <l , tl~<BP t2 {Cl}ocont)>

Base case of composition :

tl·t3r- means that a is a solution of equation tl·t3. ElCallple :

B~ s~stematic application of equilibration, and using the conceptual definitions of APPEND, CONS, MEMBER, end identifier evaluation, the LISP expression : <MEMBER X <APPEND l <CONS X M>>> W is conceptualized in 2 concepts, which correspond to the cases whether X is in l or not. The meta-evaluation of 00 is detailed in [5].

Aula of induction

If the equation t1·t2 gives corresponds to e vicious tell-recursive concept : a solution a which circle, then the

where tru. is the empt~ conjunction of literals, be replaced b~ 1 may

Non tail-recursive case : If tl-t2 gives a, end corresponds to a vicious circle, ·

ee~ be replaced b~ the set of concepts (we do distinguish between LOGIC end CONTROL in definition of lnductx for ease of exposition) not the

n {<L1M I t1+(BP t2 v+(BP ( inductx v n) (lnductx v O)+v1 ll'llUCElC1l, INOUCE[Ckl} where INDUCE is defined as : -»>1 INOUCE[ti+Dil · (inductx ti nb+1)+1N01Dil IND!teral · (BP (lnductx tare nb) w+w) !NO [(BP tare t1'+01' t~;+Oa')l · (BP tare t1'+1NDlD1'l te'+INO[O.'l))

Remark 1 ~corresponds to a set of HORN clauses. If induction were to be defined within actual s~ntax of c leuses 11 OJ , l t would need a preprocess for gathering separate clauses. This process is not n~~ded with the s~ntex of concepts.

Example :

MEMBER ma~ be defined without using index notations, using the recursive concept :

<MEMBER x (~ · z))/x-~ is t1 and <MEMBER x z) is t2. Equation t1=t2 solves in :

which corresponds to a vicious circle. So,

Thus, application of the rule of induction on ~ gives

(MEMBER x (yl ··· yn z))/x-yi ~ <BP <MEMBER x z) v ~ v)

Equilibration of this concept with the two stop conditions of a recursive definition of MEMBER gives the conceptually-defined and non-recursive definition of MEMBER.

Vicious circle :

A substitution list a is a vicious circle iff every of its associations is of the form variable=f(variable'), where f(v) is a term containing v, end where variable has been renamed in variable' during equation solving. In that case,

n

n

e includes the association variabla·f (variable').

n ~ays of building f from and obtaining index notations and technics for solving equatlons which include index notations are devetoppad in 151.

STRATEGIES

Evaluation end seta-evaluation are strategies which systematically use the equilibration rule. These strategies may not stop when applied to recursive concepts. CAN uses a program ana1ys1s strategy which controls the application of equilibration rule, and uses induction to simplify the control component of recursive concepts. To control the application of equilibration and induction on a set of concepts, CAN builds the dependency graph of the set of concepts, which corresponds to the connection graph 1101 built from HORN clauses. This control, and the situations it is sensitive to, are developped in [51. The strategy of program analysis used by CAN is as follows : The dependency graph of a set of concepts is dave topped by equ ilibret ion until all loops (self-referent concepts) are vicious circles. Then, induction is selectively applied 151 end the whole process is restarted.

4. AUTOMATIC DIAGNOSIS OF SEMANTIC PROPERTIES

During the process of meta-evaluation, several semantic properties are detected by CAN, ~hich correspond to simple properties of the solutions of the equations encountered. All the fo llo~ ing ewamples have been treated successfully by CAN.

lNJSED PORT IONS OF CODE AND LHIEF IN I T IONS.

An undefinition is diagnosed from the composition of t~o concepts :

~hen equation tl-t2' has no solution. In that case, 01 is an unused cant inuat ion. If concept t1 -+ 01 .is part of the definition of a conditional, for instance the else part of IF :

w/x-nil -+ <PROGN · expressions)

then <PROGN expressions) is an unused portion of code.

Ewemple

In the follo~ing unfinished pattern matcher, the lndicated portion of code ~ill never be evaluated :

<DE MATCH <P 0 SUBSTITUTION> <CONO <<EQUAL P 0)

SUBSTITUTION>

«ATOM P>

NIL> <<MEMBER P VARIABLES>

<LET - (VAL <ASSQl P SUBSTITUTION>>

<IF VAL

(IF <E~UAL <COR VAL> D>

SU STITUTION

... ))

!ill,l (CONS <CONS P D> SUBSTITUTION>>>>

The detection of this unused portion of code ~auld be easy if ASSQl ~as conceptually defined. But CAN is only provided its LISP definition :

<DE ASSQl <V S> <COND <<NULL S> NIL> ( <EQ V <CAAR S> > (CAR S> > <T (ASSQl V <CDR S>>>>>

CAN must conceptualize this recursive definition in order to find that <ASSQl P SUBSTITUTION> ~ill al~ays return the value NIL. CAN uses the induct ion rule to conceptus l ize ASSQl, in the ATOMS-LISTS model of LISP, ~here EQ is defined as :

<EQ atom atom> .. T <EQ x y)/x-y -+ NIL

Note that CAN is not looking for unused portions of code. In the present example, CAN really discovers lt. This is an understand1ng activity.

I.NJERUSE tF A FLN:T I ON.

If, from the composition

the equation tl·t2' solves in one solution, and if this solution contains an equation of the form v = constant ~here v is a segment variable, then t1 ; Dl ~s underused ~hen applied to t2 .. t2'. (a vartable ts a segment variable ~hen it is the argument of an associative function).

simple examples :

Let e be an expression in the else part of

<IF <CDR L) then-part · else-part)

• e being <REVERSE L> leeds to the equation {al ... an)·L ~hich solves in nzl or nzO.
• e being (LAST L>

leads to the equation {?1 Y)·L ~hich solves in (?1):() (?1 is a segment variable).

So, REVERSE and LAST are underused in this context.

No~, CAR is not underused if e ~auld be <CARL>. The related equation (a . b)·L solves in b=(), but b is not a segment variable.

NDN-T~INATION.

CAN determines the class of data for ~hich a program never terminates from its dependency graph by the follo~ing method:

- Within the set of concepts ~hich result from the analysis of the program, consider any recursive concept :

~here equation t1=t2 corresponds to a vicious c ire le. If, for any other concept t3 + 03 the equation t2=t3 has no solution, then the concept :

t1 + t2: infinite computation

replaces m.

Example :

Here is an erroneous definition of the LISP function MEMBER :

CAN conceptualizes the applicative part of MEM as

<MEM <MEM NIL (al ..· an)) .. NIL ! (al ... an)la1-!> .. <MEM! ()>:infinite-computation <MEM x (al an ~ . y)/a1-x> .. (x . y)

Remark NIL may not be substituted to underlined variables.

If ~e describe the class of never terminates, by the contain X, ~e miss the case this case, MEM stops ~ith special case corresponds to <CAR HIL>·HIL. data for ~hich MEM cases ~here L does not ~here X is NIL. In a correct ans~er. This the LISP special case

INTERESTING FEATURE.

The following PO~ERSET program builds the list of subsets of a set represented as a list of its elements :

<DE POWERSET <E> (IF <NULL E> <CONS NIL NIL> <LET <X <POWERSET <CORE>>> <APPEND X (OCONS <CAR E> X>>>>>

<DE OCONS <A U

<IF <NULL L> NIL

<CONS <CONS A <CARL>>

(OCONS A <COR L>>>>>

Though PO~ERSET ~ay not be conceptualized, or siMplified, more than as a recursive program, quite ldenticel to its LISP form, we may use CAN ln a particular Model, a simplified space of properties of LISP objects 121, where LISP lists are abstracted to the number of their elements. In this model, CAN conceptualizes PO~ERSET in:

whlch says that lf PO~ERSET is applied to a list of length n, its result has length 2 power n, which is the number of subsets of a set.

LNEASTI'INJING httFIT A PROGRfl'l DOES.

As · student-examination simulation, let us write a program which tests whether two lists have the same length or not, without using the LISP function LENGTH :

~e now try a s11ell subtlety: instead of testing whether M is empty, we swap L and M at the recursive call, with only one of them reduced. Thus, we obtain :

~e can verify if this program fits our intentions by asking CAN to understand it. CAN's conceptualization of SAMELENGTH shows that the value is T (true) when L and M have equal lengths, but the conceptualization exhibits an undesired case 1 SAMELENGTH's value is T also when L has exactly one single element more than M. In the other cases, the value is correctly NIL (false>.

5. CONCEPTUAL REPRESENTATIONS

Conceptual representations are an attempt to :

• -maximally simplify the CONTROL component of a program, for the benefit of the LOGIC component.
• -make the most of the literals in the LOGIC component be of the form variabla~term or variabla,ter·. That is, properties of terms and relations among terms are maximally represented in the form of substitution lists, which detail their structure.
• A conceptual calculus program (concept) is a couple <LOGIC 1 CONTROL>. The maximum simplification of the CONTROL component is as a rule : term ~ term. The simplification process consists in getting rid of breakpoints in the CONTROL component. Breakpo ints can be suppressed by :
• Equilibration. The LOGIC component is augmented with the solutions of the solved equations.
• Induction. The LOGIC component is augmented with indefinite sequences of associations, represented with index notations.

In other words, the structure of terms, which is implicit in the CONTROL component, is explicited in the LOGIC component. The latter may then be of invaluable help in further equation solving situations.

However, the only notations (variables and constructors) which may be allowed in the LOGIC component are those for which equation solvers have been designed. For instance, equation solvers which deal with associative constructors and segment variables (prefixed here with a "?") allow to replace the classical recursive definition of APPEND

<LOGIC and readability) model of LISP CONTROL are intermixed for more by the one CAN uses in the ATOMS-LISTS

CAN automatically obtains~ from ID· By developping conceptual representations, we have been able to maximally simplify the CONTROL component of the conceptual definitions of many basic LISP functions :

• -Typed element variables for functions CAR, COR, CONS, NULL, ATOM, NUMBP, EQUAL.
• Segment variables and associative constructors for functions APPEND, LAST.
• Index notations for MEMBER, NTH, ASSOC, REVERSE, LENGTH.
• -Associative-commutative constructors for arithmetic functions.
• Associative-commutative-idempotent constructors for internal functions such as the binding and unbinding of an identifier CSETQ, SET, and ldentifier evaluation).

6. EQUATION SOLVERS

The equation solving methodology is an improvement on the classical procedural specification technics : Ho~ is an automatic program understanding system going to find a redundancy in :

<PROGN <SETQ X <>>

<LENGTH X>)

A typical AI solutlon, based on procedural specifications, ~auld be to make LENGTH decide itself, during meta-evaluation, ~hether or not its abstract argument is too much restricted or not. This solution ~auld need every LISP function, user defined or not, to do so. Our solution is to commit this decision to a general equation solving system ~hich is independent from LISP functions (user defined or not).

In the present case, the decision is taken from the comparison of the t~o abstract sequences :

(a1 . :. an)=()

~here a1 ... an and n are variables, ~hich gives the constraint n=O.

The equation solving methodology consists in grouping the procedural capacities ~hich are redundantly scattered into independent reasoning systems. The implemented equation solvers that CAN uses, including the index notation cases, are developped in [51.

7. CONCLUSION

We have presented the CAN system for automatic understanding of LISP programs. CAN is programmed in the conceptual calculus frame~ork and sho~s capabilities ~idely beyond the scope of other existing program understanding systems. The reasons behind these achievements ~ill not be found in a special effort to devise ad-hoc solutions, but in the directions ~e focussed our attention to, ~hich indivisibly concern the representation and deductive po~er of the conceptual calculus.

While traditional logical expressions and theorem proving ~ere adapted to program ve~ifying, ne~ variables, constructors and equation solving have raised the program understanding task to previously unreached summits.

We have recently studied a promising ne~ direction: the automatic choice of a level of representation. This possibility ~auld alto~ CAN to conceptualize, using for instance set notations, programs ~hich are not built from set operations, but ~hose operation may advantageously be abstracted to a set operation.

In front of the multiplicity of ne~ directions, and ~ith regard to the pro·ising achievements ~e expect from them, ~e can consider the program understanding problem as highly deserving entirely devoted ~arks.

CAN and the conceptual calculus are implemented on e POP KL-10 in the VLISP language Ill.