A System which Synthesizes Array-Manipulating Programs from Specifications

A SYSTEM WHICH SYNTHESIZES ARRAY-MANIPULATING PRO�~~S FROM SPECIFICATIONS

M. BIDOIT, C. GRESSE, G. GUIHO Laboratoire de Recherche en Informatique Batiment n° 490 Universite de Paris-Sud

91405 ORSAY (France)

A system is presented for constructing array-manipulating programs from given specifications. The system accepts high level specifications and produces recursive programs in an Algol-like language.

Restriction to a specific domain and use of powerful techniques such as first-order matching or generalization make our system very efficient. It has been implemented in LISP on a small computer and has been tested for a large number of examples.

The general techniques we use, are briefly discussed and the synthesis of one program produced is presented.

Key-words Array-manipulating programs - High-level specifications - First order matching - Generalization- Program synthesis.

I · INTRODUCTION

Although program synthesis is a recent develop­ ment, there are already a·great number of ap­ proaches (1-7).

Our approach is similar to that of Manna and Waldinger [5) but we restrict ourselves to the synthesis of array-manipulating programs. We think that this restriction will limit back­ tracking.

The principle of this kind of synthesis is : We provide the specifications of the problem to be solved in a high-level language (not compi­ lable in a conventional way). The system works as a transformation program in order to obtain a final rrogram written in a compilable langua­ ge. For this purpose, the system uses heuris­ tics and rewriting rules to eliminate non-comp~ lable terms which occur in the specification language. The synthesis is then achieved by use of matching and generalization. This system has been implemented on a small computer (MITRA 125) in LISP and has been tested for a large number of examples.

2. LANGUAGES

2.1 The specification language

The language level should be high enough to represent the abstract types close to the concepts used by the programmer in his descrip­ tion of the problem. In our restriction to the array type, the constructors and selectors are simple and few. Here are some constructions we use as specification language.

Note that for all the examples the system knows that T is an input array with bounds A and B and that I is a subscript. So input specifica­ tions like in the DEDALUS system of Manna and Waldinger are not necessary.

1. Find I between A and B such that 5> (I, input variables)

Examples :

• Find I between A and B such that T(IJ=Z
• Find I between A and B such that T(I)~ll T[A:lt
• Test if~ (input variables)

Examples :

• Test if Z<All T~A.Bl
• Test if for aZZ I between A and B-1 T(I) ~ T(J+l)
• Construct TAB[BI ·. B2) such that TAB·consauxor (I, input variables and §J (I, input variables) from T[A ·· B]

Example :

• INSERT (T,A,B,Z). We want to insert an integer Z in a sorted array
• construct TAB[Bl .· B2] such that TAB=CONC(T [A ·· I), Z, T [I+l ·· B]) and AZZT [A ·· I):s: Z and AZZ T[J+l . · B)>Z from T[A .· B]

1. Co~ute the number of elements T[I)such that~ (!,input variables)
2. Example : -the number of elements T[I) such that T[I)~Z. e. Two of the upper constructions can be combi­ ned to make a more complex one Example :
3. Find I between A and B such that (the number of elements T[J] such that T[J]~T[I])=K.

Although we use few constructions, the possibi­ lity of combining them makes our program more flexible in the sense that we can use different specifications for solving the same problem. Example : Finding the maximum element of an array can be specified both by :

• Find I between A and B such that T(I] ~All T[A · · B)
• Find I between A and B such that (the number of T[J) suah that T[J)>T[I)J=O.

These different specifications lead to diffe­ rent pt·ograms

f. etc ·..

2.2 The output language

The output language is an Algol-like language and we extensively use recursion and basic ope­ rators relevant to array structure. For the INSERT example, the output will be of

• the form :

INSERT (T,A,B,Z~INSERT�EN (T,A,B,Z,A) INSERTGEN (T,A,B,Z,C~if C>B: TAB+CONC(T(A .. B) .~ ifnotifi(T(C)5.Z) : TAB+CONC.(T(A .. C-1] ,Z,T(C .. B)) else INSERTGEN (T,A,B,Z,C+1) endif

3. REWRITING RULES AND HEURISTICS

The are two kirtds of heuristics. Some of then are related to abstract types which are used and some others are related to general program­ ming principles.

1. The first class of heuristics deals with the constructors and selectors of abstract types [12). Informally, the heuristics use selectors to achieve a decomposition of the problem and then constructors to solve the original problem. In our implementation, the only type we use is the array type so this family of heuristics is restricted. It corresponds to the case forma­ tion rule (see Manna [5) or Weigbreit [8))
2. If the array is empty, then no operation is necessary
3. If not, we try to deal with one particular element of the array (generally the first one) and then look at the rest of the array.
4. The second class of heuristics deals with general knowledge on programming. The basic principles are similar to those used in Weigbreit [8) ·
5. -Formation of recursive calls.

During the synthesis, the first class of heuris­ tics defines subgoals of the initial problem. If by matching, we notice that a subgoal is an ins­ tance of a previous one or an instance of the initial goal, we infer a recursive call. It is then necessary to verify a well-founded set condition.

• Generalization : (Insane heuristic) (Wegbreit [8) , Kodratoff [4)). In the previous process, when matching fails ; it is possible in most cases to generalize the goal used. With this generalization, matching becomes effective and a recursive call can be generated.
• Subsidiary programs : (Manna and Waldinger [5D In the case formation rule, the inferred condi­ tions can be non-elementary (i.e. it contains some specification language terms). Then a sub­ problem has to be introduced at this point.

4. TECHNICALS TOOLS

4.1 First order matching

This matching is mainly used for the detection of recursive calls. The· algorithm implemented here is from Huet [9) . Note that recursive calls are always terminal.

4.2 Second order matching

A second order matching in necessary, in princi­ ple, in order to select the transformation rules to be applied. In fact, in our present implemen­ tation we don't nead a '~ophisticated' algorithm and we use a simple key-word detection algorithm similar to pattern-directed invocation.

1. Theorem prover

To solve the subgoals induced by the case forma­ tion rule it is often necessary to use a theorem prover.

It is surprising that the necessary prdofs are often very simple. So we have implemented a very "naive" theorem prover which has been suf­ ficient for all our examples.

1. ONE EXAMPLE OF SYNTHESIS : INSERT The input array T[A .. B) is sorted and we want to insert an integer Z in T such that the output array TAB[B1 .. B2) remains sorted.
2. We provide the following input to our system
3. -INSERT (T,A,B,Z)
4. -CONSTRUCT TAB[B1 .. B2) such that TAB·CONC (T(A ·· I) ,Z,T(I+1 .. B)) and All(T[A .. I)s;Z and All T(I+1 .. B) >Z from T(A ·· B) -For All I between A and B-1 T(I) 5. T(I+1)
5. The first rule, when applied, transforms the problem into a first goal :
6. (I) (Find I between A and B such that All T(A .. I)5.Z and All T(I+l .. B]>Z then (construct TAB[B1 .· B~ such that TAB = CONC (T(A .. I) ,Z,T(I+1 .. B))
7. At first the system considers only the first part of the goal and transforms in into (Find I between A and B such that

All T[A .. I) sz) then (verify

All T[I+I .. B) >Z) then (construct ... ) The system now applies the decomposition rule to the first sub-goal and generates a segment of the desired final program and three new subgoals. if A>B then (2)

i fnot i fi[T(A) SZ) then (3) else (4) where (2),(3),(4) are the following subgoals.

1. I+B then .... unchanged ....
2. I+A-1 then .... unchanged · . · .
3. (Find I between A+l and B such that AllT(A+l.. I) !:Z) then (Verify AllT(I+I ·. B>Z) then ~onstruct TAB[BI .. B2l such that TAB·CONC(T(A .. I) ,Z,T(I I ·. B)))

The system considers the goal (4) : Matching (4) wi th (I) fails because A can't be matched simul­ taneously with A+I(Find ... ) and A(Construct .. . ) So the system introduces a new generalized pro­ blem : INSERTGEN(T,A,B,Z,C) with :

INSERT(T,A,B,Z)~NSERT�EN(T,A,B,Z,A)

The input for INSERTGEN is : - (Find I between C and B such that AllT[C .. B)SZ) then (Verify AllT [I+I .. B)>Z) then (Construct

TAB(Bl .. B2) such that TAB,.CONC(T(A .. ll,Z,T(I+l .· B))

• For All I between A and B-1 T(I) ST(I+I)
• Apply i ng the decomposition rule leads to i f C>B then (2) i fnotifl(T(C) SZ) then (3) else (4)
• I+B then .... unchanged ... .
• I+C-1 then .... unchanged ... .
• (Find I between C+l and B such that ·. )then
• Now matching succeeds because A is matched wi t h A and C with C+l. So (4) is achieved by a recursive call to INSERTGEN(T,A,B,Z,C+I)
• (2) and (3) are rewritten as

(2') (Verify AllT[B+I .. B) >Z) then (Construct

TAB(BI . . B2) such that TAB=CONC(T(A .· B),z,T[B+I ·. B)))

(3') (Verify AllT[C .. B) >Z) then (Construct

TAB (B I .. B2) such that TAB,.CONC (T (A ·. c-1) ,z, 'I{C..B)) Verif i cations are very easy since in

• (2') T[B+I .. B]=~ and any property holds forevery element of an empty array

(3' ) the theorem prover uses the two conditions T(C) >Z (introduced by the case formation rule) T [A .. B) is sorted (input specification)

• *So (2') and (3') are rewritten as
• (2" ) TAB=CONC(T(A . . B) ,Z)
• (3" ) TAB=cONC(T(A .. C-I), Z,T(C .. B))

INSERT(T,A,B, Z )~INSERT�EN(T,A,B,Z,A) INSERTGEN(T,A,B,Z,C)-if C>B:TAB+CONC(T(A .. B) ,Z) i f notifl(T(C) SZ) :TAB~ONC(T(A ·· c-1) ,Z,T(C .. B]) else INSERTGEN(T,A,B,Z,C+I) endi f

6. CONCLUSION

This system has been implemented on a small co~ puter and works efficiently for all examples list ed below ·(and some others). The maximum time necessary for one example is less than one minute. There are three main reasons for efficiency: - the system has a thorough knowledge of the do­ main and so backtracking is strongly reduced - we use a very powerful first order matching algorithm

• the simplicity of the theorem-prover makes it very efficient .

This system, in our opinion, proves that the Manna and Waldinger approach is correct and can be very powerful in specific domains. This shows that studies in the field of automatic program synthesis can be relevant for practical applica­ tions.

Proaraaa conatructed :

lapreunutive ut~~plaa of the proar ... conttrucud by ovr ayttea a'te the follovina :

• fiadina the uxi.,. eleaent of an aruy
• teatina if an array il torted
• teat ina if a nullbar balona· to an array and fiad ina ita eubacript
• taetina if a number h leaa tMa avery al ... at of an array
• taniaa i f an array contai na duplicaua
• teat iaa if avery d.-eat of a a. array h lea a than every al .... t of aaothar
• inaartiaa an et .. nt in aft array (IlfSDt)
• rneraiaa an array
• findina an ale-nt equal to ita eubacript
• fiDd:in& tha 1r,th (in incnatina order) al ... nt of an array
• co.putina the number of elemenu areaur than a particular one
• taatina if tvo array· are identical
• ea~~putiq the iotaraeetion of tvo arr·J·
• firtd I utwo" A tmd B ...,h tltat AHT(I · · 8( >Z tmd 't(I-tJ<Z

(tll!nw :r[A ·· BI artd r ·[A ·· cJ are .:"""t IU'f'Cl¥·! .

• f(.rtd I u_.., A tmd B ouah tltat At!T(A .. I)"-4l!T'(I .. cl

a&~ua-.:&a

(I) li&twaDD, krhhn.aavaa.y "Con.rructina proarau froa .. :·pla c:oaaputatioo IDI Traae. on Softvare Eq., vol. 2, a· l , Sept. 1976 .

1. s.._.u P .D. "A Mthodoloay for LISP proaraa c:ooatruction fr011. exaaplet" . Jou1'DIIl of ACII 24-1, 1977.
2. (l) Cui ho C., Jouanuud J . P. 11 lnhrence of function· vitb an interactive eyet·". Machia.a Jatelliaeoc:a 9, 1977 .
3. lodratoff T. "Cboix d'un proar-. LISP correeporwtant l un axdlph". Coqrle APCIT, lac:onaahaance dea rora .. , 1971.
4. UJ Nanna Z. , Waldlnaar 1 . "Syntheai a : Dr····Proaraa". Techrial mcea 1)6 , su. 1977 .
5. [6) libel V., Purbach o., Schreiber J .r. "Strauait~ for the 1ynthaeh of alaorithat". AISI/Ct Conferaoc:a on Artificial Intelliaence , KMiboura, 1971.

(7) Valdiqer I . "Conatructina proaraa autoutically udq thaor .. provina". Pd.D thath. Carneai· Mellon, 1969 .

(I) Veabrait I . "Coal Directed proar· tranatorutioae" . DE Tranaa\ we .... lq. Vol. 2, a· 2, 1976.

[9) Huet C. "L'unUicatioa dane he lana·&·· 1,2, ··· w". 'D'ICh ct;,Ducb'at d'Et&at Unh·erdt' r.rh VII, 1976.

(10) Creu11ay P. "Contribut i on l la dffinition intarpdr·~lve « ?! l'i~Dl~tA­ tioe dee l·bda lana·a··"· Thf1a de Doctorat d'Etat, Uni.v . PArh Vll , 1977 . (Ill Craua C. It Cuiho C. "!tude comparative dee proar-· da eynthfu Je proar.-ae" . Conarfe A.FCET Infot'alt ique, 1971 .

(12) Cuttaa J. , Koroviu !., Mol~&r D. l . ·~. dalian of data typ·· ..,.~cit i ,a iun leeearch leport, lnforution Schncae lftltituta, Marina del lay, CAi itmi t·.