A language of refinements
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.
|Collections||ANU Research Publications|
|TR-CS-94-05.pdf||137.19 kB||Adobe PDF|