Mechanised Refinement of Procedures

Refine is a tool that supports the application of Morgan's refinement calculus. It was designed to support teaching and use by beginners; it is already in use. We describe here the extension of Refine to support the development of (possibly recursive) procedures in the algebraic style of the refinement calculus already adopted by Refine.