A Design for an Automatic Programming System

AmTRACT

The algorithm design problem is concerned with the construction of an algorithm satisfying a given specification of a problem. We present an overview of a system, called NAPS, which designs algorithms in a to~own manner. Given a formal specification of a problem NAPS produces a top level algorithm plus specifications for any necessary subalgp­ rithms. The specifications for the subalgprithms are produced in such a w~ that the top level algo­ rithm will satisfy the original specifications if and only if subalgorithms can be built which satisfY the subalgprithm specifications.

I OVERVIIDN

A·formal specification of a problem@ has the form

ECx) = z such that zcS & P(z,x) where xeD & I(x)

where D and S are the input and output data types respectively, and I and P are the input and output conditions respectively. The algorithm design problem [1 ,2,3,4,5,6] is to prOduce an ~rithm which satisfies a given formal specificat1on. We present here an overview of an automatic algprithm design system called NAPS which is currently under developnent.

Figure 1 shows the organization and flow of information in NAPS.

* The work reported herein was supported by the Foundation Research Program of the Naval Postgraduate School with funds provided by the Chief of Naval Research.

Douglas R. Smith

Naval Postgraduate School Monterey, California

The algorithm design process proceeds in a top down manner with the production of higher level algo­ rithms resulting in the generation of specifica­ tions for lower level algorithms. The workings of NAPS are described below via a description of the main sources of information which the design con­ trol module of NAPS uses.

A. Data Structure Knowledge Base

The data structure knowledge base (DSKB) is organized around alternate algebraic descriptions of various data types. The central part of a description consists of a definition of the type by means of a set of primitive objects and an operator which generates the rest of the type. For example, the data type INTID:rnLIS'rS has the set of primitive objects PRIM= !nil, (0), (-1), (1), (-2), (2), ··· 1 and at least two distinct generators 1 ) FUNNY CONS: PRIM x INTIDmLIS'r -7 INTID:rnLIS'r where FUNNYCONS( (3) (1 2 4) ) = (3 1 2 4), and 2) APP:EllD: INTID:rnLIS'r x INTID:rnLIS'r -7 INTIDmLIS'r where APPEND ( (3 1) (2 4) ) = (3 1 2 4). Other algebraic properties of a type which are included in a description include any well-founded orderings on the type (used to prove termination of loops), and congruence relations with respect to the gen­ erator (used for formulating subproblems).

Also included in a description are various operators on the data type. These operators are used in the construction of the target algorithm. Properties of the operations and their interaction with other operations are expressed by transforma­ tion rules. These rules are used by NAPS for sim­ plifying expressions and for theorem proving pur­ poses in the deductive mechanism of the design con­ trol module.

B. Control Structure Knowledge Base

The Control Structure Knowledge Base (CSKB) is organized about a small collection of algorithm schemas. The algorithm schemas are classified as basic or complex. The basic schemas are abstracted forms of typical control structuring mechanisms from programming languages: 1) o~ration sequenc­ ing, 2) Dijkstra's IF statement [3J, (see section IIA below) , and 3) the WHILE loop. The complex schemas result from our unified theory of combina­ torial search algorithms [7] and presently consist of schemas for divide and conquer, branch and bound, greedy, and dynamic programming algorithms. It is our view [8] that well designed algorithms are often adaptations of one of a small number of generic algorithms rather than being arbitrary well-formed compositions of the usual control structures (IF-THEN-ELSE, WHILE loops, etc.).

Associated with each schema in the CSKB is a correctness schema. A correctness schema is parameterized in two ways. First, there are arbi­ trary predicate symbols in those places where the input and output conditions and types are expected. Given a formal specification we can instantiate those symbols in the correctness schema. Secondly, there are arbitrary function and predicate symbols in place of those data operations which are them­ selves parameterized in the algorithm schema. Dur­ ing the design process these function symbols will be replaced by formal subspecifications for the corresponding data operations. These subspecifica­ tions are generated in such a way as to guarantee that the fully instantiated correctness schema will be a true formula (under the natural interpretation which is in essence provided by the DSKB). The parameterized data operations in the algorithm schema are then replaced by calls to procedures which are generated by NAPS from the subspecifica­ tions.

Each algorithm schema in the CSKB also has associated with it a collection of heuristics for guiding the process of adapting the schema to the problem at hand and for generating subspecifica­ tions. The heuristics generally work by selecting some operators from the DSKB and substituting them into both the algorithm schema and the correctness schema. NAPS then attempts to prove the correct­ ness schema making use of knowledge in the DSKB about the data types and operators. Whenever the proof of the output assertion of the correctness schema reduces to an expression which cannot be proved, NAPS attempts to transform that expression into the output assertion of one of the data opera­ tions which has not been instantiated by the

heuristic.

II EXAMPLES

A. Maximum of two integers

Suppose that a user supplies the following specification of the problem of finding the maximum of two integers:

The appropriate algorithm schema for this problem is an IF schema:

which i s parameterized by the predicates Qi(x) for 1~i~n and operations fi(x) for 1~i~n. The correct­ ness schema is

where D and S are the input and output types respectively and P is the output condition. A heuristic for the IF schema suggests instantiating the data operations fi by elements of the out~t domain if the output domain is small and/or expll­ citl~ given. Here we can replace f 1 (x) by a and f 2 (x) by b. Combining these substitut1ons with the substitution of INTEGERc for D (the input type), !a,bl for S (the output type), and z~!a,bl for P (the output condition), we get the following par­ tially instantiated correctness schema.

which can be simplified via transformation rules to

At this point we need either target lan~ expressions or specifications for 01 and 0 2 such that the resulting correctness formula is true. The right hand side of the implications in our example have simplified to computable target language expressions so we can set Q1 and Q2 to the expressions a>b and b>a respectively. ~ quick check confirms the soundness of these choices and the resulting algorithm for MAX2 is

B. Sorting !! list of integers

In this section we will only sketch the derivation of sort al~orithms based on a divide and conquer schema. See LB] for more details. A typi­ cal specification for the sort problem is

A simplified binary divide and conquer schema has the form

FI

Before the schema can be used a selection must be made of a description of the input and output data types as discussed in section IA. For the sort problem the selection of a description of the INTEGERLIST data type containing the generator FUN­ NYCONS will ultimately lead to the production of insertion sorts and selection sorts. The selection of the APPEND generator leads to the production of quicksort and mergesort algorithms. The underlined function names in the divide and conquer schema are data operations to be filled in by the adaptation process. The predicate PRIM returns true exac~ly when its argument is an element of the set of prlm­ itive objects of the input data type. PRIMSOL pro­ duces the correct output for the problem when its argument is a primitive object. DECOMPOSE splits its argument into smaller pieces on which the algo­ r i thm · recurses · Finally COMPOSE takes the results of the two recursive calls and combines them to form the output object.

We will i~ore the heuristics for guiding the instantiation of the PRIM and PRIMSOL operations and focus instead on the two heuristics for han­ dling the nonprimitive case. One of these heuris­ tics suggests selecting an operator for DECOMPOSE from the DSKB and then solving for the specifica­ tions of COMPOSE. Selection of the simplest DECOM­ POSE operator leads to mergesort and insertion sort algorithms (depending on the previous choice of generator). The dual heuristic suggests selecting an operator for the COMPOSE and then solving for the specifications of the DECOMPOSE operation. Selection of the simplest such COMPOSE operator for the sort problem leads to the production of quick­ sort and insertion sort. In the case of quicksort we select APPEND as our COMPOSE operation and derive the following specification for DECOMPOSE

• & PERMUTATION(x,APPEND(y1 ,y2))
• & Vr,sEINTEGER [rEy1 & SEY2 ~ r~s].

Here y<wtx iff the length of y is less than the length of x. Adapting the divide and conquer schema to this specification leads to the construc­ tion of a form of the usual partition subalgorithm of quicksort.

lii CONCLUSION

An overview has been presented of a system for generating algorithms from user supplied specifica­ tions. The system attempts to adapt one of a small number of algorithm schemas to the specifications. The process of adapting a schema generates specifi­ cations for subalgprithms. The resulting algo­ rithms are guaranteed to be correct since the adap­ tation process works by attempting to instantiate a correctness schema in order to make it a true for­ mula.

We are continuing to generalize and extend our theory of combinatorial search algorithms which supplies the knowledge and organizing principles underlying our control structure and data structure knowledge bases. For experimental p.~rposes we have a prototype system running that is able to handle the proofs of correctness formulas and the genera­ tion of subspecifications for the sorting algo­ rithms discussed in section IIB.