Specifications by Examples and Properties

When contrasting the pros and cons of specifications by axioms (as seen in Section 2.1) and specifications by examples (as seen in Section 3.1), it turns out that these specification approaches are quite complementary, each alleviating the drawbacks of the other by its own advantages. This gives rise to the idea of combining these two specification approaches so as to preserve only their benefits, while diminishing their disadvantages. But we must bear in mind the fundamental difference between the two approaches, namely specification completeness and specification incompleteness. 

Merely amalgamating the two formalisms into specifications by axioms and examples is thus not a good idea, as the incomplete example-set would only play an illustrative side-role to the complete axiom-set. 

on the other hand, one could aim at incomplete specifications and add some stronger form of axioms to the examples so as to overcome the weaknesses of specifications by examples only. We call properties [Hener and Deville 92, 93ab] such a strong form of axioms, and only require them to be written in (some subset of) logic. Indeed, until Part III, we do not restrict ourselves to any syntax or required computational content of properties. We only assume that properties are an incomplete source of information. Actually, in case properties were a complete source of information, most of the results hereafter would remain valid, but not always be relevant. 

Let be the relation one has in mind when elaborating a specification of a procedure for predicate r. We call the intended relation, in contrast to the relation actually specified, called the specified relation. This distinction is very important in general, but crucial with incomplete specifications, where one deliberately admits a gap between the two. 

Deflnition 6-1 A specification by examples and properties of a procedure for predicate r n, denoted EP r), consists of  

---

Definition 6-2 The specified relation of a specification by examples and properties is the set of tuples extracted from the set of its Herbrand-logical consequences. 

Let s illustrate the notion of specifications by examples and properties by a few sample specifications (others may be found in Section 14.4.2). The chosen language for properties is, strictly for the sake of illustration, non-recursive normal clauses that have a head with the predicate of the examples. Universal quantifiers are usually dropped for convenience. Also, negative examples are not allowed. Note that most of this Part II is independent of such choices. Our claim is that such properties and examples, if carefully chosen, embody the minimal knowledge that doesn t give away the solution, but is sufficient for successful algorithm design. 

Overall, the specification language is quite expressive and readable. Specifications by examples and properties are usually incomplete, and hence ambiguous, but minimal. There is a danger of internal inconsistency and redundancy in such specifications, though. 

Note that this discussion is independent of the used specification formalism, and hence of their completeness or incompleteness. In this book, we investigate a particular niche of automatic algorithm synthesis in the context of (incomplete) specifications by examples and properties, we develop methods of predicate-variable instantiation, and apply them to the step/variable mapping identified in Example 8-8. 

Note that the MSG Method is part of our tool-box for solving sub-problems occurring during synthesis, and not a solution to the overall problem of synthesis from specifications by examples (and properties). 

How to achieve a synthesis that yields logic algorithms that are correct wrt their intentions This is impossible to guarantee with specifications by examples and properties. However, the stepwise synthesis framework of Section 7.3.2 and the correctness theorems of the seven synthesis steps clearly identify the critical points, where interaction with the specifier should thus take place. 

A logic algorithm LA(procComp) can now be synthesized from the inferred specification by examples and properties. We use the synthesis mechanism described in the two previous chapters for this. The predicate procComp is assumed to be a new primitive. 

In Chapter 6, we define a specification approach that is based on the notions of examples and properties. It requires examples that are chosen in a consistent way by a specifier who knows the intended relation. The presence of properties (whose actual language is application-specific, and thus left unspecified for a while) is meant to overcome the problems of ambiguity and limited expressive power of examples, while still preserving their virtues of naturalness and conciseness. Such specification languages are quite expressive and readable. Specifications by examples and properties are usually incomplete, and hence ambiguous, but minimal. This specification approach holds the promise of more efficient and more effective synthesis than from examples alone. 

In Part III, we develop an actual logic algorithm synthesis mechanism from specifications by examples and properties, as seen in Chapter 6. It fits the particular non-incremental synthesis strategy presented in Chapter 7, is guided by the divide-and-conquer algorithm schema seen in Chapter 8, and uses the tool-box of methods developed in Chapters 9 and 10. 

---