Specifications by Examples

We first define a possible language for specifications by examples. Later in this section, we list alternative approaches. 

Definition 3-1 A specification by examples of a procedure for predicate r n consists of a finite set (r) of ground examples of r n, split into ... 

Example 3-1 A possible specification by examples of the member problem is (member) = ... 

It should be noted that Definition 3-1 is not the only possible definition for specifications by examples. It is too much geared towards the synthesis of algorithms. So let s generalize it to the larger framework of empirical learning from examples. Specification approaches vary according to the following criteria ... 

Anyway, whatever the actual setting, the advantages of specifications by examples are the following ... 

The work of [Jorge and Brazdil 94] is another attempt at trace-based synthesis of logic programs. Their specifications by examples are augmented with partial execution traces, called algorithm sketches. 

The first building block is the actual specification formalism used to elaborate the input to algorithm synthesis. An arbitrary choice has been made here to investigate synthesis from incomplete specifications. Starting from the pros and cons of specifications by examples, and of specifications by axioms, as outlined in Part I, we define, in Section 6.1, a specification approach that is based on examples and properties. Then, in Section 6.2, we illustrate this approach on a few sample problems. Future work and related work are discussed in Section 6.3 and Section 6.4, respectively, before drawing some conclusions in Section 6.5. 

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. 

But, 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. 

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. 

In terms of related work, specifications by examples are surveyed in Section 3.1. Also, the notion of specifying property can be traced back to the notion of specifying axiom, and specifications by axioms are surveyed in Section 2.1. In this section, we only survey research on extending example-based specifications by another incomplete information source. 

Shapiro s idea has also been picked up by [Drabent et al 88] they define four kinds of assertions that may be added to a specification by examples. These assertions describe approximate knowledge about the intended model of the specified program. These assertions are used for partly mechanizing the oracle of Shapiro s MIS. They constitute a possible instantiation of our notion of properties. 

The presence of properties (whose actual language is application-specific, and thus left unspecified in this part) is meant to overcome the problems of ambiguity and limited expressive power of specifications by examples, while still preserving the virtues of naturalness and conciseness of such specifications. The predicates used in the properties constitute a partial basis set, and thus a partial conceptual bias for synthesis. 

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. 

This specification approach holds the promise of more effective and more efficient synthesis of algorithms than from specifications by examples alone. 

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 3, we survey the use of inductive inference in automatic programming. Specifications by examples are concise and natural, but are usually also incomplete and ambiguous, due to the insufficient expressive power of examples. As inductive inference is much less known than deductive inference, we first survey this field. Inductive synthesis from specifications by examples can be classified into trace-based synthesis and model-based synthesis. We survey the achievements of inductive synthesis of LISP functions and Prolog predicates. 

---