Design via executable specification

A description is presented of two approaches to the design of a simple string matching machine: a direct approach and a transformational approach. In the latter approach, Horn clause logic is chosen as the specification language. It has the advantage that the specifications themselves are executable as logic programs: hence they can be used as prototype implementations. The simple formal semantics of Horn clause logic allows one to perform equivalence-preserving transformations semi-automatically on the specifications to derive more `efficient´ ones. When using the specifications as executable prototypes, immediate feedback is gained on the design specifications. Any errors uncovered from these executable prototypes relate directly to the designs themselves. Thus, the risk of introducing unintended errors in a prototype implementation, such as careless coding errors, translation errors caused by misunderstanding, etc., is reduced