An Overview of a Refinement Editor
Trevor Vickers · Australian Software Engineering Conference · 1990
The refinement calculus is a formal technique for the development of programs which are provably correct with respect to a given specification. The refinement editor provides automated support for the interactive derivation of programs using the refinement calculus. A novel aspect of the editor is that the user edits the record of refinements rather than manipulating the programs which they produce.