Symbolic Execution in Algorithm Design

SYI\ilBOUC EXECUTION IN ALGOBITHM DESIGN

Oavid Steier and Elaine Kant 1

De p;:~rtrnent of Computer Science Carnegie-Mel lon University Pittsburgh, Pennsylvania 15213

Symbolic execution, also called symbolic evaluation, has been studied as an independent software engineering tool for use alter a program is written, but until recently little work has extended and integrated it into the problem-solving processes in design 4 In this paper. we focus on symbolic execution in design by describing our model of algor it11m design. a system that implements that model, and illustrate the use of symbolic execution in a detailed example.

Most of the early research on symbolic execution focused on execution or evaluation of complete programs to aid in testing, debugging , and verifying conventional lan-guages. Some more recent work considers evaluating, analyz:ing, and explaining higher-level specification languages. This related work is discussed in Section E. Since our primary interest is automating algorithm design, we operated independently of these efforts, although similar concepts appear in our system. We developed a model of algorithm design based on the analysis of some fifteen protocols of subjects designing geometric algorithms. The model underlies the implementation of an automatic algorithm design system we call DESIGNER [16] . Symbolic execution in this model shares a number of concerns with trad itional symbolic execution: serving as an inexpensive 1est process that effectively executes multiple inputs simultaneously; creating symbolic representations of outputs as functions on inputs (useful for generating invariants and formally verifying program:::. or algorithms); describing the conditions for following each path to detect non-executable segments and to define subdomains of the input; indicating coverage of concrete test data and helping to generate additional tests. We are concerned also with symbolically executing procedures efficiently (not by macro substitution) . The features of DESIGNER that differ from most other systems and modify symbolic execution for design purposes are:

1. DESIGNER executes incomplete algorithms in a data­ flow language rather than requiring a full program in a procedural language,
2. Failures in symbolic execution lead to the posting of difficulties. Other problem-solving processes in the system use this information to correct errors in the design automatically.
3. The data objects in DESIGNER may be arbitrarily complex structures (e.g. geometrical objects or sets). In contrast, most symbolic interpreters allow only variables subject to conjunctions of numerical constraints, which are inadequate to represent many algorithms. (However, there is no guarantee that

4 1he execution of program plans on concrete data lor debugging during design was however surme"l·od a decade aoo [?.4]. 1he execution ol plans in problem solving, which ha" been rnore heavi ly researched, lor example [9]. is also related .

Abstract

Syrnbu!ic executicn of part ial algorithm descriptions is a i>rHw;rfll! mc!!tod f(,, (l tJ idinu il1c (licJtlri\inn c!e:-; ign process (as is borne ou t !1y studyi:1u protoc(; l:> oi lwm:·q aluorilhPl designers). Yi"t t11e rol e of ~;yrnbo li c execut ion in algori thm design has not been c 1 0 $f! ly uxarnined, clesp~te th2 work c)n syrnbo! ic e:.-:ecution of complete prourams e.s an :);d in the valicl ::tion of software. In the cunter : of t!1e DESIGNER proj~ct . w,~ have deve l cpo~d a data-fiow lan juagc; for i'epresc;nli :ly partt~iiy designee! <ligorithrns and n pror.·! -.~ lc1 r .<; ~· tnlvll i c· · !i y r:xr:ctrt iniJ d:ltu-ll,lw cnnliuurations th ~tt c;tf1 u<:;cuver usdul kno\'!led<;e to quid; · desi<Jn . rilE: t2chniques O ' ~:;:.;r: i 11;d IHcre Cilntrillute si ~Jnificanlly tr,warcls cur goal of t:-,uik:it t!J ~~ fu ll y autunuted alyoritl ll l t C:cs iQn ~y:> lem.~ 1

A _Introduction

Our studies of how people design algorithms (14, 15) reveal that symbolic e><ecution is one of the principal design methods used in the absence of specific knowledge, 3 and we believe that symbolic execution will play an equally important role in the automatic design of algorithms. When specific design knowledge indicating what to do next is available, it should of course be followed. In its absence, however, executing an incomplete design allows an assessment of the consequences of the current set of design decisions to help decide on a next step. This execution may be either on specific data such as {point E, point B}, on abstract symbols such as "point-set," or on combinations of specific and abstract objects. By symbolic execution we mean the process of describing outputs in terms of inputs that are primarily abstract rather than concrete symbols. However, a continuous range of evaluation from wholly symbolic to wholly concrete falls under this heading , and all variants make contributions to the design process. When all items are concrete data values, we refer to the evaluation process as test-case e><ecution , these more complex structures can be reasoned about satisfactorily in all cases.)

1 Eiaine Kant is currently at Schlumberger-Doll Research, Old Quarry Road, Ridgefield , CT 06877.

2 This research was supported in part by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 3597, monitored by the Air Force Avionics Laboratory under Contract F33615-81-K-1539, and in part by the National Science Foundation under Grant DCR-8412139. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research 'Projects Agency, the National Science Foundation, or the U.S. Government. ·

3 our studies are supported by additional research on the human design of computer systems [1] ,

1. DESIGNEI1 represents t11e results of multiple execution paths as disjunctions of conditionals on a single object rather than requiring the user to specify the execution path(s)
2. Execut ion is controlled by assertions and rules rather than by a fi xed interpreter, so it can be customized to serve a variety of design goals.
3. Multiple options in symbolic execution address a variety of de~ign goals such as determining the run time of an algorithm, checking for consistency between adjacent steps in a design, and verifying that an algorithm produces the desired output.

An initial implementation of symbolic execution embodying most of the principles described in this paper is operational in DESIGNER. Algorithms are represented as collections of object instantiations in a object-based system with a few simple forms of inheritance; symbolic execution operators are implemented in LISP; and symbolic execution control rules are written in the production-system language OPSS [1 0]. This implementation has symbolically executed algorithms in several task domains including geometric algorithms (such as finding the convex hull of a set of points) , set operations, and numeric algorithms (such as Fibonacci and recursive factorial). Work continues on enlarging the set of geometric algorithms that can be represented and executed.

B The Design Model

In refining our model , we have concentrated on the following areas: definition of a data-flow representation for partial algorithm descriptions, implementation of operators for altering and executing the descriptions, collection of algorithm design heuristics in a number of task domains, specification of a subsystem for reasoning with visual images in geometric algorithm design, and development of a problem ~olving arc:hitecture for handling non-hierarchical goals effectively. Descriptions of this work have been published previously or will appear in future reports. so only the details needed to understand the role of symbolic execution are presented here.

One driving force in this research is the formulation of the problem spaces [18] in which the algorithm design activity takes place. This requires a precise definition of the representations for algorithm design and of the operations used to manipulate these representations. It also requires definition of the problem spaces for the task domains (not discussed in this paper).

The major algorithm problem spaces are cle!:iign and execution. The spaces share the same basic representation, but address difterent types of problems and make use of different operators. In the design space, the states are partial descriptions of algori thms. The current design state is elnborated by the application of des1gn operators (that edit algori thm descriptions) until a satisfactory specification is obtair.ed ("atisfactory is defined dynamicaliy by the design rules) . The algorithm modification process is guided by rules that describe what operators to apply to change the partial algorithm description: the rules have conditions that determine their applicability to the current state. If the search control knowledge is not sufficient to selec:t a design operator, the problem solver sets up a subgoal to obtain this knowledge. The subgoal is usually satisfied by problem solving in another space, often the execution space.

Execution is an information-gathering strategy that executes the current description of the algorithm on symbol1c or actual data objects to expose problems or oppo~tunities for refinement. In the execution space, the partial description of an algorithm is fixed, and the data objects change in structure and position to yield the different states. If execution on symbolic data doesn't produce enough information for further refinement, or if a concrete validation of the algorithm is desired, then a concrete example is generated, actual data items are substituted for the symbols. Symbolic execution is preferable to test-case execution in many cases. For example, it amasses more complete information for verification, and it may be better to use a description such as "integer less than 10" than actually to pick one, when the system is looking for a counter example or example and doesn't have all the constraints on an object yet. However, symbolic execution can be more expensive if considerable expression simplification is required. Furthermore, discoveries caused by the combination of unexpected assertions and previous experience are more likely to result from working with concrete examples than from abstract reasoning based on the results of symbolic execution.

C Representing Algorithms for Design and Execution

We have developed a language called AL (Algorithm Language) lor ro:;presenting algorithms during the design process. 5 Some key features of this representation, which distinguish it from similar representations (such as the plan calculus of the Programmer's Apprentice [19, 26, 20)), are its data-flow character, the fact that control flow can be defined implicitly by data-flow links rather than control-flow links (with a few exceptions), and the small number of initial built-in processes. Also, in the Programmer's Apprentice, all loops must be expressed as recursive calls, while in AL they can be expressed iteratively. In AL. the spectrum of description levels, from kernel ideas to fully refined algorithms. is easily represented. A consequence of this representation is that concern with the representation of data objects is largely absen t initially (except in algorithms that rely on special data structures) in favor of elaboration of the processes manipulating data objects.

In developmg AL, we tried to identify a set of algorithmic objects that correspond closely to the conceptual building blocks our subjects use. We call such blocks components. Components are connected by links between ports (lor input or output) of the components. A few basic component types are assumed. and the processing of a component may be modified by assertion~ on the component. New components may also be defined at any time in ·terms of other components and assertions. Our assertional language is a variant of first-order predicate calculus that can express the state of computations over time. A. collection of components, links, ports, and assertions grouped together forms a network called a configuration. Configurations are the partial algorithm descriptions.

This framework is not the basis for a "pure" data-flow representation. Our goal is to use objects that occur naturally as algorithmic steps, not a minimal set of primitive components. To avoid proliferation of object types, a design idea is initially represented as a component of approximately the right type with descriptive assertions. As design proceeds, any component representing a complex process that does not correspond directly to a single primitive action may be refined into a complete configuration called a refinement configuration. This ability to refine components into subconfigurations along with the ability to define new concepts by adding assertions to simpler concepts provides a natural abstraction mechanism in AL.

1-he level of detail in AL approximates that which people use to describe algorithms to one another. We do not claim that AL is an exact cognitive model for human algorithm design. only that the character of the language is useful for automated design.

Only a brief overview of AL's type hierarchies of components, ports, links and assertions will be given here since a detailed language description is the subject of another report in preparation [22).

• Components : In AL, active process components represent steps in algorithms: algorithms are generic procedures to be refined; applies create new data based on their inputs; selects extract an element from an input collection; recursive-calls apply a process recursively; tests conditionally alter the data flow; compares report the relationship between two items and generators produce individual items from a collection in any specified order. Another type of component is the memory, which holds a representation of an object or collection.

Generators cause certain components to be repeatedly executed. As the aigorithm design proceeds, it may be necessary to represent this repeated computat ion explicitl y, which we do with a loop-box. We classify the computation in a loop into separate conftgurations by function: the init ialization, the loop-body, the repet ition and the termination . All parts of a loop-box are opt ional (although the absence of an essential part may lead to a semantically in::;orrect design). During refinement , it is expected that somE: of the parts will be empty.

• Ports: Input ports and output ports represent data inputs and outputs of components. while signa/ ports serve control functions on specific component types, such as resetting a generator.
• Links: Links usually connect components or configurations at the same level of the hierarchy. Special kinds of links, ·vertical-input links and vertical -output links, connect components to their refinement subconfigurations.
• Assertions : Assertions are classified in AL by the domain of the operations they describe, for example numerical assertions and geometrical assertions. When used in a data-flow configuration, each assertion instance is assigned a role in accordance with its use. Roles relevant to symbolic execution are operational assertion , to specify how a component's output is derived from its inputs; description, to describe a data item; precondition and postcondition , to assert that certain conditions hold before and after the execution of a component; and complexity, to state time or space required for the execution of a component. Other assertions specify constraints on the order of execution the algorithm's components. Some of these assertions are predefined as being relevant to execution of all instances of a given type; for example, all selects must have a composite object as one of their inputs. Other assertions are added during the design phase to specific component instances; for example, a particular generator produces elements from its input collection in

increasing order, a particular test places its input numerical item on the true-exit port if the value of the item is greater than one.

Configurations are executed (in the execution problem spaces) on items. Items are data objects that are passed between components and stored on links. Items have associated domains, such as geometry and arithmetic. Several items may be grouped together into a collection (which correspond to mathematical sets or sequences) . Items may represent concrete objects or symbolic objects.

An example of a configuration representing a partially refined convex hull algorithm 6 is given in Figure 1. The speci fication given to the subject is to find the convex hull of a set of input points where a convex hull is defined as either a polygon made up of a subset of the input points that encloses all the input points or the set of points on that polygon . This ability to view the output as either a set of points or a polygon turns out to be important during the design. The Imide predicate that defines enclosure is defined in the geometry space (it assumes that a point on the boundary of a polygon is inside the polygon) . It is not necessary for the discovery that lmidr be defined by logical assertions as long as there is a domain-space operator to recognize examples of enclosure. The assertion is written as follows:

(Type( Output, polygon) 1\ Output. vertices~ Input 1\ (V x)(x E Input -+ lnside(x, Output))) v (Type( Output, point-set) 1\ (Output~ Input 1\ (J x)(Type(x, polygon) 1\ N y)(y E Output-+ On(x, y)) 1\ N y)(y E Input -+ lnside(y, x)))))

In the diagrams below this relation will be abbreviated to Convex-hull(Output, Input).

The configuration of Figure 1 represents an intermediate state in an initial attempt to get a working algorithm without using sophisticated design principles. The derivation is similar to one followed in a protocol that we have studied closely. The kernel schema follows the transfer paradigm as described by Barstow [2) in which the points in the input set are generated by the producer and built into an output set by the consumer. During the previous part of the design (not described here) this kernel schema was refined into a loop. In the graphic representation of our language, all configurations belonging to the same loop are enclosed in the same loop-box in a special format: initialization at the left side, termination at the right side, and repetition along the bottom. On each iteration of the loop, the algorithm arbitrarily selects a point (in select S1) from the set of input points that have not yet considered (stored in memory M1) , adds the point to the set of points found to be on the hull so far (stored in memory M2), and then tests if the expanded set could be included in the hull (in test T1) . If the test returns false, then the point just added is selected (in select S2) and deleted from M2. Symbolic execution of the kernel schema led to an expectation (recorded as an assertion) of an algorithm linear in the number of input points. The linear expectation arises because the producer is expected to be executed at most once for each input point to produce all the points on the hull. The refinement has not yet been symbolically executed to analyze its run time, so the fact that this expectation is not fulfilled has not yet been discovered. We will continue this example in the next section.

6 The convex hull algorithm discovered by this subject is not a particularly efficient one. Many other convex hull algorithms have been developed, and the problem can be solved inN logN time.

D Symbolic Execution in DESIGNER

One way to view the design process in our model is to consider each modification of a design as the imposition of a new constraint on the behavior of the algorithm. To usefully guide refinement , the constraints imposed by altering one part of the configuration must be propagated since typically refinement of algorithms is strongly locally driven. The propagation of a constraint imposed by one part of an algorithm serves to focus attention on potential problems in development of other parts of the algorithm and to bring together new combinations of facts that may lead to additional opportunities. This selective propagation of configuration-derived constraints is driven by execution.

Symbolic execution manipulates assertions on symbolic items that arrive on the input ports of a component to produce appropriate assertions on items on the output ports. The assertions on the output items describe the results of applying operations defined by the component and its operational assertions to the input items. Symbolic execution continually evaluates assertions and compares the results against expected values determined locally by the component being executed. If an expectation is violated, then a difficulty is posted to notify the rest of the system of the inconsistency. Knowledge of the inconsistency combined with search-control knowledge in the design space should guide the problem solver in selection of the next operator to apply. This process allows detection of interactions between components in a uniform and efficient manner. A more detailed description of the symbolic execution process may be found in another paper [23].

Here, we show how symbolic execution can be used to integrate a test predicate discovered in the domain space (geometry) into the current design and to notice that the algorithm is not linear, as was originally expected. Details of the discovery of the test predicate have been described elsewhere [15], and so will not be repeated here. The original goal was to find a test to determine if a point is on the hull, but the discovered predicate tests if a segment is not on the hull (a segment is not on the convex hull of a set of points if there are not points on both sides of the line segment). Therefore the system must modify the design to make use of the predicate. As a first approximation, the test is initially represented as an assertion on test T1.

Operational-assertion (Test predicate) on T1:

Points-bolh-sidcs(segmenl-input, Input)

Since this assertion has just been added to T1, T1 is symbolically executed to see if it is fully refined. The first problem that is uncovered is that the inputs are not well-defined , because the operational -assertion requires different input than is currently available. First, there is only one input port. and there need to be two ports, so execution is suspended, and another port (we'll call the existing one P1 and the new one P2) is added. A link is attached to the new port and preconditions on inputs to the test are added to distinguish P1 and P2:

Precondition on T1:

l:'qual(l'l.input, Input) 1\ Type(l'2.input, segment)

Using execution in this manner to uncover problems is an important part of DESIGNER. When a configuration can not be successfully executed , a problem called a difficulty is posted in the form of a goal or subproblem to be solved (not necessarily in the design space) . If the initial assertions are correct and the inference mechanism is correct and adequate, the configuration that implements the specifications is causing the problem, so a difficulty indicates that some element of the current configuration needs to be altered or refined. The difficulties fall into a small number of categories. Since the design rules need. only cover these few categories of failure, a few rules and a relatively simple problem-solving architecture allow DESIGNER to make progress in most cases, regardless of the task domain.

To continue the example, when symbolic execution of T1 is attempted again, the precondition on the inputs to T1 are compared to the descriptions of the input items. The clause in the precondition about P1 is not satisfied because the current link to P1 does not contain the entire input, only a subset of it. There is a design rule that applies to this problem:

If a precondition is not satisfied by an input link in the current design, and there is another output in the current configuration that will satisfy this precondition, then detach the input link from its present source and connect it to the desired output.

'When this rule fires, the link feeding P1 will be detached from M2 and connected to Input. The other clause of the precondition is still not satisfied though, since P2 is not connected to any1hing producing a segment. The previous rule will not apply, since no segment is present in the design. A new item must be created, which means that a component with a useful operational-assertion must be added to the configuration. but another rule does apply:

If a precondition is not satisfied by a link attached to a port in the current design, but it is known that an apply component with an appropriate operational­ assertion can create a component with the required output, then add an apply to the configuration with the required assertion and connect its output to the port described by the unsatisfied pre-condition.

In th1s case, the post-condition required is that the o~,;tput of the apply is a segment. This knowledge is used to find the opemtional-assertion for the apply by searching the domain knowledge base of the system for an assertion with an appropriate post -condition. This search suggests a draw-segment as an assertion. so apply A1 is added with a draw-segment assertion which takes a head point and a tail point and produces the segment connecting the two points.

Operational-assertion (Apply action) on A 1:

/)raw-srgnwnl(poilll· inpul, point· input)

In this example. since A 1 has just been added, that component is symbolically executed to see if it is complete. Symbolic execution again points out the difficulty that ports and links are missing from the segment-constructing component and collects information about the inputs. One point that is available is the point produced by S1 , so a link is added from S1 to A 1. Unless directed otherwise, the same input· should not be used twice for the same component (since that may produce only degenerate cases of the desired output) so another point is needed. The description of Output contains the fact that the output may be viewed as a polygon, so that the process of finding a convex hull may be seen as building a polygon and possible polygon fragments may be constructed by repeated extension from the most recently added vertex. Therefore, the other input to A1 is obtained by following the memory of the hull so far (M1) with a select component (S3) that gets the point most recently added.

Operational-assertion (Selection criterion) on S3: Select-most· recently-added(polygon· input)

Execution of S3 and A3 proceeds correctly, but M2 must now be changed to a component that manipulates polygon fragments by adding and deleting segments rather than adding or deleting from a point set. This is done by changing the port types and description assertion on M2.

Now M2. and T1 execute correctly, but DESIGNER notices that the output of the test T1 is a segment, and not a set of points as expected. But M2's delete-segment port requires a segment. This condition activates another design rule:

When the descriptions on some item satisfy all the preconditions on some input port of a component , then add a link (if there isn't one already) from the port producing the item to the input port with the satisfied preconditions.

So a link is added from T1 's true-exit port to M2's delete­ segment port. An "optimizing" rule now applies to this situation:

If data can flow through two different paths at one level of a configuration, but the paths produce symbolic items with equivalent descriptions, then one of the paths is redundant and the more complex one may be deleted from the configuration .

In this case, S2 is no longer necessary, so it is removed . The configuration resulting from all the changes described is shown in Figure 2. Further design will focus on the details of the initialization and termination of the loop, which were not previously addressed in refinement of the loop-body, but we wi ll not describe this here.

Another important feature of symbolic execution is the use of the act ive goal to limit the constraints propagated during execution. This promotes simplici ty and efficiency and also defines a simple criterion tor deciding when execution of a configuration is complete. For example, if the goal is to guarantee that the algorithm is correct, then symbolic execution is tantamount to a full formal verification in the data-flow language, a complete propagation of all constraints. If the goal is to analyze the efficiency of the algorithm, then only those constraints relevant to the time and space usage of each component are propagated. Since many of the constraints in the design are often irrelevant to the active goal, this selectivity limits the computation necessary for automated design_? However, the development of a surprising assertion can change the active goal or modify the type of information collected during symbolic execution. Unless interrupted by another process, execution generally proceeds by depth-first search of the graph formed by the configuration, restricted by the semantics of the data flows and bounded in depth when a component is sufficiently understood for present purposes (possibly from previous execution). Symbolic execution terminates when an active goal is satisfied, a difficulty is encountered or if nothing remains to be executed.

The design goals satisfiable through execution include:

• Checking the consistency of the design, including checking for missing inputs or specific errors such as data-type conflicts between components.
• Given actual test-case data for some or all of the input, applying the algorithm to the data to compare the resulting output items to expected values.

7 Other advantages of explicitly considering design goals in automated systems are explained in Maslow's survey of design research [17].

• Checking that the algorithm (or component) executed on symbolic data satisfies its specifications as indicated by its preconditions and postconditions and those of any subcomponents. In the extreme case this amounts to a full verification.
• Analyzing the time complexity of the algorithm.

We illustrate the use of execution for time complexity analysis using the convex hull example. Analysis proceeds by propagating constraints about the number of different items that may occur on links that force re·execution of certain components. This is equivalent to determining the size of the set of items on a link as a function of the size of the input, when considering the set as a temporal abstraction of all items that may flow on the link over the entire computation. The repetition and termination parts of loops are especially important to this analysis. In this example, at a later point in the design, it is seen that M1 is reset H times, corresponding to the number of points on the hull . which means that the worst ·case run time of this piece of the algorithm is ()( H N 7), where N is the number of points in Input and T is the time to execute T1 for each segment. Since the formulation of the test in the domain space requires comparing the input segment to each point in Input, the test takes time proportional to N, so the total time is O(H N 2 ). This violates the original expectation of linear time. However, the existing design rules suggest no way to remedy this problem without a complete change of algorithm.

Currently, the flexibility needed to satisfy these goals in symbolic execution is provided by allowing a variety of processing options. More than one option may be active at a time. Which options are activated depends on the reason for trying symbolic execution.

In addition to implementing these options, we are also currently examining the issues related to repeated computation, since the presence of repeated computation in an algorithm causes difficulties for all current symbolic execution systems, and indeed for human programmers as well. The problem is due to an undetermined, and hence potentially infinite, number of execution paths to be considered. One approach that has been taken [4, 27] is to try to automatically derive and solve recurrence relations to express the behavior of loops without the need for repeated ''xecution . People, on the other hand, usually recognize a correct loop when a small number of test cases work, and we wish to capture this ability to recognize familiar patterns from the structure of the c:lgorithm and from symbolic or test·case execution in our system. We are currently investigating an approach that shares some of the characteristics of temporal abstraction in the Programmer's Apprentice. If the number of iterations is not totally constrained as in symbolic execution, we execute each part of the loop once to checl~ internal consistency and give the re.sults to a set of rules that can recognize familiar configurations and results. Such rules could perform the temporal abstraction necessary to determine the behavior of a loop in the general case.

E Related Work on Symbolic Execution

Previous work on symbolic execution has focused primarily on the goals of testing (generating test data and exercising program paths) and verification , although debugging , understanding ,

Assertions:

explanation, and analysis also have been addressed. Here, we list the work in this area that is most relevant to algorithm design; a longer summary can be found in (23]. For a survey of the uses of symbolic execution for program testing specifically, see [6] .

EFFIGY [8], SELECT [3], DISSECT [12],_ the EL 1 evaluator [4] and ATTEST [5, 28] were some of the first systms to use symbolic execution !or testing and verification . Symbolic execution, in conjunction with other techniques, has also been used to analyze the run-time performance of simple programs [27, 13] More recent work considers symbolic evaluation of specifications (rather than program code) to help in the development process: the partition analysis method (6]; KOKO (7] , which symbolically evaluates GIST specifications and is used as the basis of an explanation system [25]; REASON (21], a component of the Programmer's Apprentice system (in addition to other MIT work on meta-evaluation in the context of the actors formalism [11, 29]). Finally, simulation, a process similar to symbolic execution, was identified (based on protocol analysis experiments) in a model of the human design process focusing on software systems rather than algorithms [1].

F Discussion

We have described a system that makes explicit the role of symbolic execution in the design process. We claim that execution has more uses than the testing and debugging applications described thus far; namely, that in uncovering opportunities for the refinement of a data-flow algorithm representation, execution is the principal method guiding design in the absence of specific knowledge. A standard set of difficulties combined with appropriate search control knowledge allows the automated selection of design operators even if the algorithm is incompletely described. The power and flexibility of this approach is being validated by our current work on writing derivations of complex algorithms (such as convex hull); the results of execution control the search in the design problem space.

Acknowledgements

We thank Allen Newell , Brian Milnes and Andrew Peterson for comments on earlier drafts of this ·paper, and Mary-Anne Wolf for co!!ccting many of the protocols. A!! of them have contributed in numerous ways to the ideas in and implementation of DESIGNER.