Extensions to SETL to support problem specification and transformation of imperative programs

Candidate: Lewis,Henry Merriman


Programming by transformation is a reliable and efficient way to develop algorithms. An ideal methodology begins with high-level specifications of the problem to be solved. Such dictions are by nature concise, easy to understand, and easy to verify. They are free from the details that determine the method by which the solution is found, yet promote transformations leading to derivation of solutions. The user of the transformation system applies refinements and modifications that transform the problem specifications into algorithm specifications, and so is able to derive programs that solve the original problem. We propose extensions to the set-theoretic programming language SETL to support problem specifications. The resulting language realizes the ideals of problem specifications. The resulting language realizes the ideals of problem specification, and further supports direct execution of the highest-level specifications as a search over a solution space. Its dictions are imperative at all levels of derivation, so as to provide consistency of style among all versions, from problems to programs. We show how dictions of the form find variables $\vert$ conditions serve to specify problems, and how transformation of the conditions promotes derivation of algorithms. We propose dictions that allow concise specification of problems that require minimization of a function, and a variant that allows specification of problems that are inherently non-rigorous, or whose solutions admit approximation or tolerance. We suggest transformations of expressions that lead to algorithms employing formal differentiation of expressions or dynamic programming. Through examples we show that the method of transformational programming constitutes a tool for the specification, derivation, and discovery of algorithms.