Specifying the user interface to a program transformation assistant
Catherine Burton · Formal Methods · 1989
A study on program transformation which was motivated by the possibility of systematically developing correct efficient programs from their specifications, is presented. The particular approach taken involves a formal notion of simulation between programs. This idea of 'simulation' is algebraic in nature-in fact it can be defined simply in terms of theory morphisms and natural transformations which are standard notions from universal algebra and category theory. To emphasise that programs are objects in a category, and simulations arrows in that category, the latter are referred to as program morphisms. This, together with 'theory morphism', gives the acronym 'TMPM' for the approach. The author also describes the implementation in ML of a transformation assistant (also called TMPM) to act both as a check on the accuracy of workings performed and also as a means for expediting them. The usefulness of any ultimate realistic version of TMPM depends critically on the user interface. Hence the first stage of implementing TMPM was followed by a process of reflection on the characteristics of the kind of user-interface desired. The author discusses this and other stages of the implementation.