The Role of the High Level Specification in Programming by Transformation: Specification and Transformation by Parts

Candidate: Merritt,Susan Mary


Specification by parts is a technique for constructing a very high level specification of a problem. The specification is then the target of transformation by parts, a global transformation strategy, which yields a family of high level algorithms which are correct and which solve the problem. The specifications are easy to construct, to understand and to modify. The key to the specification by parts technique is the use of weak parts. Output conditions are factored into conjunctions of weaker conditions, called weak parts, each of which is easier to satisfy than the original condition. In the transformation by parts, an initial guess is made for the output object. The guess satisfies some subset of the weak parts; the conditions in this subset are called the invariant conditions. A general iterative structure is built, which incrementally changes the initial guess, keeping the invariant conditions true, and converging to the remaining conditions. The methodology demonstrates the relationship between invariance and convergence in algorithm construction. In particular it demonstrates that algorithms for the same problem are often the result of different choices of invariant and convergent conditions. The methods are illustrated in three case studies and in three supplementary examples (which are smaller in scope than the case studies), all of which are fundamental computer science problems. These applications demonstrate the flexibility and ease with which the high level specifications can be constructed and transformed. They also demonstrate the potential which this methodology offers for the discovery of new algorithms, the illustration of connections among known algorithms, and the possible semi-automation or automation of algorithm construction.