Program refinement is the process of transforming formal specifications of software systems into implementations. I have worked in this area for a number of years, and am interested in supervisting projects addressing the application of refinement to particular problems and the development of software tools to support program refinement.
The following are some examples of possible projects in this area:
The development of a program from a formal specification can be described as a sequence of applications of transformation rules. If the specification is changed, we would like to adapt the derivation to the new specification to obtain a new implementation. Various approaches have been taken to mechanise this process for different formalism (usually using either functional or logic programs as both specification and implementation); similar ideas have also been used to adapt formal proofs to modified theorems or robot plans to satsify different goals. The aim of this project is to adapt these techniques to the refinement calculus, where specifications are given as pre/post condition apirs, and implementations are imperative programs.
Refinement structure diagrams are a graphical notation for describing derivations of programs from formal specifications in the refinement calculus. A previous project involved designing and implementing an interactive editor for these diagrams, with a view to supporting a flexible development process allowing a mixture of formal and informal development. The aim of this project is to extend the refinement structure diagram notation to allow subdiagrams, corresponding to procedures, and to extend the existing editor to support them.
This is joint work with Waikato University, funded by FRST.