Symbolic Execution of the Gist Specification Language

1. lnt reduction

Current research at lSI approaches software development in two steps. First a user translates his informal requirements into a formal specification . The specification language. Gist [Balzer 81 }. is significantly more powerful and expressive than a programming language, allowing the user to concentrate on specifying what is required rather than how it is to be accomplished . The second step is the implementation of the specification with the help of a transformation system. A sound transformation system guarantees a correct implementation of the specification . To support this specification-based paradigm we are developing tools to help a user create a specification , to explain its behavior to the user, and to allow a user to guide the implementation process at an appropriate level [London & Feather 82] [Fickas 82] . Two tools especially relevant to this work are the Gist to English paraphraser [Swartout 82] and the Trace explainer [Swartout 83]. ·

An important part of developing a specification is validation , i.e. , trying to be sure that what is specified is what is really desired. Specifications, like programs, may contain widely separated parts that interact in non-obvious ways. Finding such interactions is the job of symbolic execution. Symbolic execution derives information about the specified behaviors and tries to integrate it into a coherent description. This can help the user find errors in the specification by revealing unexpected consequences or increase his confidence by deducing consequences he desires.

2. Overview of Gist- the Problem

Gist was designed to allow people to specify behaviors in a natural way. It models the state of the world as a relational database consisting of a set of objects and relations among them.

1 This research is supported by the Air Force Systems Command, Rome Air Development Center under contract No. F30602 81 K 0056. and by the Defense Advanced Research Projects Agency under contract No. MDA903 81 c 0335. Views and conclusions contained in this report are the author's and should not be interpreted as representing the official opinion or policy of RADC, DARPA. the U.S. Government, or any person or agency connected with them.

2 Koko was the Lord High Executioner in Gilbert and Sullivan's ~[Sullivan 85] . He never actually executed anyone, but he did manage to describe in detail what would have happened ff he had.

The world may change by the addition or deletion of relations among objects, the creation of new objects, or the destruction of existing objects (which implies the deletion of any relationships in which they participate). A specification defines a set of allowable behaviors, i.e., sequences of world states. Gist allows reference to objects by description, e.g., a box that contains a big red ball . where Contains, Big, and Red are relations.

Gist is inherently nondeterministic. The descriptive reference above can refer to any box containing a big red ball . (Nondeterministic control constructs are also supported.) However, the set of allowable behaviors may be pruned by constraints. Any behavior which violates a constraint is excluded from the set of permissible behaviors. For example. a constraint that every yellow box be empty after a big red ball is put into a box restricts which box the ball can be put into. Constraints may be regarded as providing arbitrary look-ahead. in that all nondeterministic choices are constrained to the subset which do not eventually force the violation of a constraint.

• In addition , Gist provides control constructs such as conditional statements, procedure calls. demons, parallelism and others that are less common .
• It should be clear at this point that symbolic execution as the term applies to implementation languages [Clarke 81] is out of the question. Massive (even unbounded) nondeterminism makes the enumeration of execution paths infeasible. Reference by description poses severe problems of aliasing . The way the world changes is more complex than the familiar semantics of assignment statements, and constraints seem to have no analog at all.

3. Example of Symbolic Execution

Following is a very small specification, translated from Gist into English by the Gist paraphraser [Swartout 82] . (This has been edited because the original translation raises issues that we don't want to address here) .

There are sexes and persons. Male and female are the only sexes. Each person has one gender which is a sex. Each person may have a spouse which is a person.

To marry a person p2 to a person pl , the following happen atomically (simultaneously):

1. The person p2 becomes the spouse of the person pl .

2. The person pl becomes the spouse of the person p2.

If is always required that for all persons y and x, if the spouse of x is y then the spouse of y must be x.

It is always prohibited that there exists a person where the person 's gender is the gender of the person 's spouse.

The results of symbolically executing the action "marry" are paraphrased below by hand. (The Trace explainer is currently being extended to explain such results in English.)

Since spouses cannot have the same gender and every person has a gender, no person can ever be his own spouse.

Suppose two persons, p1 and p2, get married. Afterwards, p1 is the spouse of p2 and p2 is the spouse of p1. Since spouses of ·the same gender are prohibited, p1 must not have the same gender as p2. Also, p1 is distinct from p2. Before the marriage p 1 must have no spouse other than p2 and p2 must have no spouse other than p1.

This example confirms some of our expectations, e.g. , that a person cannot marry himself. On the other hand, one might have expected that the two people originally have no spouses. KOKO shows that this is not necessarily the case. Since Gist allows the insertion of relations that already hold, there is nothing in the specification to prevent the marriage of people who are already married .. provided that they are already married to each other! If this is not what the specifer intended, then symbolic execution has revealed a bug in the specification .

4. Overview of the Solution

Our approach to symbolic execution regards a specification as a large set of domain axioms, expressed in a first order temporal logic with typed variables. The axioms define the set of acceptable behaviors, i.e. , the specified behaviors correspond to the models of the set of axioms. Symbolic execution is a process of forward inference, computing consequences of these axioms. Notice that a specification need not determine the truth or falsehood of every relation, i.e. , a relation may be true in some behaviors and false in others.

This approach factors symbolic execution into two processes. First, each statement in the specification is translated into axioms about successive world states. Second, these axioms are used to derive certain interesting consequences, e.g. , hidden interactions among different parts of the specification . The success of this approach depends in large part upon the ability of the forward inference engine to find interesting consequences and avoid uninteresting ones. However, the control of forward inference is outside the scope of this paper. The rest of the paper describes how various Gist constructs are treated as axioms. We start with primitive constructs and then show how compound constructs are handled in terms of their components.

5. Constraints

Constraints are the easiest Gist construct to handle, in that they are already in the form of axioms. For example, the constraint that the spouse relation be symmetric is expressed as

'<is .x y (Spouse(x,y) :J Spouse(y.x)) ins state person' person

Actually, in the current implementation, facts about different states are stored separately; more on this later.

6. Descriptive Reference

Part of the meaning of a Gist statement like the constraint "require Contains(a box. a ball)" is that there must be referents of the object descriptions. KOKO creates a typed "symbolic instance" for each such description. If we call these symbolic instances box1 and ball2, symbolic execution simply proceeds by adding the axiom Contains(box1 ,ball2) . The interpretation in which this makes sense is that box1 and ball2 are not actually objects in the world, but rather names of objects. The distinction is that several names can refer to the same object. Thus we do not preclude the possibility that ball2 is actually the same object as some other ball that was referred to earlier.

Descriptive reference is merely a constrained form of nondeterministic reference, e.g., requiring a ba>: to contain a red ball is modelled by adding the axioms Contains(box1 ,ball2) and Red(ball2) .

One kind of consequence KOKO considers interesting is that two descriptions must (or cannot) refer to the same object.

Specifications often contain constraints that imply the identity or non-identity of such descriptions. The most common such constraint requires that a relation be a single-valued function of one of the arguments, e.g. , Gender. Another common constraint specifies that a relation describes an optional attribute, e.g. , Spouse.

The consequences of uniqueness constraints are found by forward inference. For instance, from Spouse(pl ,p2) and Spouse(p1 ,p3) KOKO deduces p2 = p3. Conversely, from Spouse(p1 ,p2) and -Spouse(p1 ,p3) it deduces p2;tp3. KOKO also uses uniqueness constraints to find consequences of facts with universally quantified variables or several arguments to compare, e.g., from Gender(p1 ,sex1) and Gender(p2,sex2) it deduces p1 = p2:Jsex1 = sex2.

7. Primitives that Change the World

The most direct effects of primitive changes are easy to axiomatize, e.g .. in the state after " insert Spouse(p1 ,p2)" it is required that Spouse(p1 ,p2) . However, such constraints cannot completely capture the effect of a change. In particular, first order predicate calculus cannot represent the notion that the before and after states are the same except for the effects of the change.

This notion is captured by predicate transformers [Dijkstra 76] . KOKO stores each state explicitly along with the set of facts known to be true in that state. Facts are propagated between neighboring states. Notice that propagating a constraint backward in time allows KOKO to identify its implications for earlier choices. We use Pre(S,F) to denote the consequences KOKO derives about the state preceding execution of the statement S given that the fact F holds afterward. Similarly, Post(S.F) denotes the consequences about the state resulting from S given that F was true beforehand . For readability, we use the notation "F1 before S = > afterwards F2" for "Post(S,F1) = F2" and "F1 after S =>beforehand F2" for "Pre(S,F1) = F2".

The computation of pre- and post-conditions 'is co-nsiderably simplified by the following considerations. For any executable statement S and any propositions P and 0 :

Pre(S,P 1\Q)::Pre(S,P)/\Pre(S,Q)

Pre(S,PVQ):: Pre(S.P) V Pre(S.Q)

Post(S,P 1\Q):: Post(S.P) 1\ Post(S,Q)

Post(S,P VQ):: Post(S, P) V Post(S,Q)

Quantifiers are eliminated by skolemization . This reduces the problem of computing pre- and post-conditions of general propositions to the special case of literals, i.e. , positive or negative instances of relations with constants, universally quantified variables, and function applications as arguments. (In the rest of this paper. "x" and "y" are universally quantified variables, "f" and "g" are functions , and other unquantified symbols are constants.) The rest of this section describes how this is done for different kinds of primitives.

7 .1 . Changing a Relation

In Gist , the insert and delete statements add and remove relations. The relation is named explicitly, but the objects may be named by description (and thus nondeterministically) , e.g .. " insert Red(a ball)" . Only one instance of a single relation is changed by each such statement ; "insert Red(ball1) V Green(ball1 )" has no meaning. An insertion results in a new state containing the inserted fact. Deletion is treated as insertion of a negated fact.

The problem of computing pre- and post-conditions of other facts with respect to insertion and deletion is simplified by the following considerations. Gist is a first order language, i.e., there are no variables ranging over relations. Thus any literal whose relation differs from the one being inserted or deleted is unaffected. (Gist supports "derived" relations, whose values are changed by changing other relations, but the handling of these is outside the scope of the present paper.) Also, if a positive literal is true before an insertion or a negative literal is true before a deletion, it will still be true afterward :

Red(ball1) before insert Red(ball2) =>afterwards Red(ball1)

Finally, if a positive literal is true after a deletion or a negative literal is true after an insertion, it must have been true before:

- Red(ball1) after insert Red(ball2) = >beforehand -Red(ball1 )

The only cases in which insertion or deletion changes an existing fact are those in which a literal true beforehand is changed by the insertion or deletion. or a literal that is true afterward is made true by the insertion or deletion. This happens just when the arguments of the fact all refer to the same objects as the corresponding arguments of the relation being changed:

P(a,x,f(x))) before delete P(b,c,d) = >

afterwards P(a,x,f(x))V(a = b/\x = c/\f(x) =d)

Recall that all of the variables are universally quantified, so after deleting P(b,c,d) . P(a,x,f(x)) is still true for all x with the possible exception of c, and that is only an exception if a= band f(c) = d. 3

7.2. Changing the Type of an Object

Types in Gist may be thought of as unary relations. Thus "pis a person" corresponds to Person(p) . An object 's type can be changed by a Gist reclassification statement, e.g .. "Pinocchio becomes a person" , which corresponds to " insert Person(Pinocchio) ".

Quantifiers in Gist always range over objects of a particular type. Therefore a universal statement may have exceptions in neighboring states where more objects have the specified type. e.g ..

'v' xperson3yperson Mother(y,x) before

Pinocchio becomes a person = > afterwards

'v'xperson3yperson (Mother(y,x) V x = Pinocchio)

This is exactly the effect that arises from treating types as unary relations: 'v'xperson3ypersonMother(y,x) means

'v'x3y(Person(x)::>(Person(y)/\Mother(y,x))) ,

where x and yare now untyped variables. KOKO would skolemize this to (Person(x)::>(Person(f(x))/\Mother(f(x),x))) , 4 translate ":::> " in terms of "V" and "- " , and apply the rules for computing a post·condition:

• Person(x) V (Person(f(x))/\ Mother(f(x) ,x)) before

insert Person(Pinocchio) = > afterwards

-Person(x)Vx = PinocchioV(Person(f(x))/\Mother(f(x) ,x))

This is equivalent to the post-condition above.

7 .3. Creating and Destroying Objects

In Gist, objects are always created with a type. Creating an object is like inserting a type relation except that (1) the created object is. different from any object that ever existed before and (2) this object is in only those relations inserted since its creation. (Objects in the initial state may be in arbitrary relationships as long as no constraints are violated.) Similarly, destroying an object is like deleting a type relation except that (1 ') the destroyed object differs from any object that ever exists after the destruction , and (2') destruction deletes all relations in which the destroyed object participateds These properties of creation and destruction cannot be expressed in first order predicate logic: instead. they are embodied in the inference engine and the predicate transformers. For example. in simplifying an equality KOKO checks to see whether one object existed before the other was created . The pre- and post-conditions of creation and destruction combine the effects of reclassification with the requirement that non -extant objects cannot participate in relations.

3 Readers familiar with unification will notice both similarities and differences. For example, P(f(a)) would match with P(f(b)) giving the "substitution" (f(a) = f(b)), i.e., it is not necessary that a= b, just that f(a) = f(b) . Also, it is perfectly acceptable to unify x with f(x) . In a sense we have a generalized version of unification which can be used for theorem proving, e.g., P(a,b)VQ is resolved with -P(c.d)VR to givea,.cVb,.dVQVR.

4 To make skolemized axioms well-defined, we treat skolem functions as immutable and defined over all objects that ever exist. but do not constrain the value of the skolem function on objects outside the original type.

Notice that the create and destroy statements are almost symmetric in the sense that each viewed backward in time looks like the other. The only difference is that a destroy statement deletes all of the relations involving the destroyed object. whereas the create statement is not empowered to insert arbitrary relations involving the created object.

The following table summarizes the conditions under which creations and destructions invalidate literals. We use P(x,a) as a representative literal , where "a" is a constant and "x" is a universal variable. The occurrences of "a= c" represent the condition that the created or destroyed object (c) is one of the parameters of the relation (we exclude variables since in one case they simplify out and in the other case they are included by the other condition) , e.g. ,

P(x.a,f(g(x))) before destroy c =>afterwards

P(x,a,f(g(x))) V c =aVe= f(g(x))

The occurrences of "x = c" represent the condition that the created or destroyed object is (instantiated by) any of the (universal) variables in the literal , e.g .,

P(f(x,y)) before create c = > afterward P(f(x,y))Vx = cVy = c Additional detail is contained in notes r; · ' 0 below.

Pre· and post-conditions for create and destroy

P(x,a) before create c => afterwards P(x,a)Vx = c ;

P(x,a) after destroy c => beforehand P(x,a)Vx = c 1

-P(x,a) before create c = > afterwards -P(x,a) ii.r

-P(x, a) after destroy c = > beforehand -P(x,a) V a = cVx = c '

P(x,a) before destroy c = > afterwards P(x,a) Va = c iii. ri

P(x,a) after create c = > beforehand P(x,a) ;, .. ,;

• -P(x,a) before destroy c = > afterwards -P(x, a)

-P(x,a) after create c => beforehand - P(x,a)

1 a= c is impossible unless the prior state was devoid of objects of the same type as x. i.e., the quantifier was vacuous. In this case P(x,a)Vx = c still holds if a= c

;, If creations were allowed to insert relations containing the new object, this entry would be "-P(x.a) Va = c V x = c " .

iii x = c reduces to false here since the quantified x only refers to objects that exist.

" Since creation does not insert relations. this case could only arise if insertions were done at the same time as the creation. See section 8.2. If creations were allowed to insert relations of the new object, this would be "P(x,a) Va = c" . The x = c reduces to false. See ;;, above.

' When Pis the equality relation, x:;ta, the result is x:;taVx = c n When Pis the equality relation, x =a, the result is x =a.

8. Compound Statements

In order to save space we describe only a few problematical constructs. It should be obvious how sequences and procedure calls can be handled. Conditionals are not hard, given a way to represent the truth of the branch condition as of the branching state. It should be mentioned that the branches are combined into a common state after a conditional , i.e. , rather than producing a tree of behaviors, KOKO describes the state after the conditional in terms of which branch was taken.

5 The equality relation can relate non·extant objects and is considered to be immutable. The table below is suitably altered for this case.

8.1. Loops

We distinguish between "simple" loops, which can currently be handled and "non-simple" loops which cannot. Simple loops are those in which the iterations are independent of each other, i.e. , the same thing is done to each of a set of objects. as in "move all old files off line" .

Most loops in implementations are not simple. e.g .. "for each file, if age(file)>age(oldestfile) set oldestfile to file". However, these loops tend not to appear in Gist specifications. They are replaced by descriptive reference, e.g.,

"a file1 such that Vfile2 age(file1 )2age(file2)"

Simple loops are symbolically executed for the entire set at once. Basically, the loop variables turn into universally quantified variables in the facts that are inserted. After "if file1 is old move it offline" we know old(file1 Poffline(file1), whereas after "for all files F, ifF is old move it offline" we know Vxtile old(x):Joffline(x). All of the symbolic instances that are generated in a loop are skolem functions of the loop variables. In general the computation of pre- and post-conditions introduces existential quantifiers, but is otherwise similar to the versions described above. e.g ..

• -P(a.b) before insert P(c.d) =>afterwards
• -P(a.b)V(c = aAd =b). whereas
• -P(a,b) before insert P(x.f(x)) =>afterwards
• -P(a,b)V(3x x = a/\f(x) =b))
• . Atomic Statements

The Gist "atomic" construct combines the effects of several constituent statements into a single state transition. An example is the marriage action that simultaneously inserts two spouse relations. It would not have been sufficient to insert one at a time because this would have led to an intermediate state of the world that violated the constraint that the spouse relation be symmetric. (Actually, that specification would still have been consistent , but now it would be possible to marry two people only if they were already each others' spouse .. another interesting result of symbolic execution .) Of course, the constituent statements of an atomic must themselves cause no more than one state transition.

The facts that become true because of the statements in the atomic must all be true in the final state, e.g ., if an atomic contains both insert P(a) and delete P(b), then a and b must be distinct. This points out a difference between executing two statements atomically and executing them in either order. There is no problem with inserting P(a) and then deleting it. A fact that is propagated through an atomic can be affected by any combination of the statements in the atomic. The pre- or post· condition of a fact with respect to an atomic statement is the disjunction of the pre- or post-conditions of the fact with respect to each constituent statement.

9. Conclusion

We have described a system that characterizes the behaviors permitted by a formal specification containing such constructs as descriptive reference, nondeterminism, and constraints. It translates a specification into a set of axioms and uses forward inference to compute interesting consequences of them. It uses predicate transformers to propagate facts between neighboring states; the computation of pre· and post-conditions in the relational database model has, to the author's knowledge, never been described before.

We have been pleasantly surprised to find that. although many problems that arise are very difficult (or even impossible) to solve in general , the most common and useful cases tend to be the easiest. We have also found that a high level specification can be easier to execute symbolically than a low level program. In retrospect this is not surprising, since the characterization of low level implementations involves a lot of work that could be described as de-compilation.

The decision to represent each state explicitly imposes certain limitations. In particular. arbitrarily long sequences of states cannot be represented . This precludes the description of non­ simple loops and certain types of historical reference. Historical reference (a special case of descriptive reference) is not yet handled. We also currently do not attempt to handle the arbitrary interleaving and merging of lines of control provided by Gist. We hope to attack these problems, but a great deal can be done without solving them. In particular, KOKO examines the "execution" of one line of control in isolation.

KOKO has produced fairly complete descriptions of some small but non-trivial specifications. Sample domains include a simplified postal package router. a world of ships and a simplified file system. Of course we expect to increase the coverage of the specification language so that more specifications can be so characterized. We believe that even without solving the difficult problems that remain , KOKO can be extended to characterize the behavior of a large class of interesting specifications.

Acknowledgements: This work was done in the context of a larger effort on the part of the Gist group at lSI. In particular, the specification language and the entire approach to the development of software defined the problem whose solution is presented (in part) here. This paper was greatly improved by the suggestions of Jack Most ow and other members of the group.