A formal refinement method is a method of constructing correct programs and proving programs correct: one constructs a program the way one would perform stepwise refinement, except that specifications are formal and refinements are justified by theorems. Thus, the program and its proof of correctness are developed in parallel, which is mentally easier than developing the program and the proof separately.
A major problem with the actual use of formal refinement methods is that, when carried out on paper, they could be mundane, tedious, error-prone, and hard to edit.
We build a computer tool for using Hehner's Theory, a formal refinement method. It combines the advantages of both the syntax-directed editor MathSPad of Backhouse et al. and the proof checker driven Refinement Calculator of Butler et al.: an editor aware of the recursive operator-operand structure of expressions, with computer proof assistant support behind. The computer will do the mundane chore, and correcting mistakes and making changes will be convenient.