A language of refinements
Trevor Vickers, Paul F. Gardner · ANU Open Research (Australian National University) · 1994
The refinement calculus is a formal technique for the development of programs which are provably correct with respect to their specifications. A formal language is presented for the description of program development using the refinement calculus. The language provides an abstract representation of the overall program development, reflecting its tree-like structure. The language is used for recording developments in the refinement editor -- an automated tool supporting the refinement calculus. 1 Introduction Formal techniques of program development [1, 2, 12, 14, 17] have the potential to revolutionise the way in which programs are constructed. The formalization of the process of program development brings with it the benefits of rigour, and increases confidence in the program's correctness. These formal methods also provide a history of the program's development from the initial specification. This is an important aspect, but one which is often overlooked. Our method applies to progra...