A Methodology for Choosing Good Examples and Properties

The formulation of such a methodology is of course influenced by the actual language for properties, and by the actual synthesis mechanism. We here stick to the corresponding decisions taken throughout Part III of this book properties are here non-recursive definite clauses whose heads involve the specified predicate. 

This methodology abstracts away the internal apparatus of the synthesis mechanism, but algorithmic and mathematical concepts such as induction parameter, term size, decomposition decrement, and so on, are hard to avoid in its formulation. 

Note the interesting role of constants in examples constants almost act like variables. More precisely, within an example, the use of different constants at different positions should reflect non-unifiability of the variables into which these constants could be turned. And the use of the same constant at different positions should reflect unifiability, if not identity, of the variables into which these constants could be turned. However, across several examples, the use of different constants at the same positions should reflect their value-irrelevance, and hence unifiability of the variables into which these constants could be turned. But unifiability (if not identity) and non-unifiability are not all there is to say about the variables into which the constants could be turned, because otherwise properties would have no different semantics than the examples they generalize. Indeed, properties have more disambiguating expressive power, in the sense that predicates other than =/2 and may be used in their bodies. 

Given our perspective on formal specifications, we would like to call the act of choosing examples and properties an act of programming by examples and properties, 

---

This heuristic has an obvious influence upon the formulation of a methodology for choosing good examples and properties. In the absence of such good specifications, a stronger version of this heuristic would be needed. A heuristic similar to Heuristic 13-1 could be easily defined for LA(procComp). 

---