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. Computer aid would relieve this problem and facilitate learning, experimentation, and use of formal refinement methods.
This tool provides the computer aid by combining a syntax-directed editor and a theorem prover. Using the syntax-directed editor, the human enters and modifies refinements and expressions. The editor is aware of the syntax of the expressions entered, i.e., as operators and operands, and the human can copy, replace, or delete an entire subexpression. The human then issues commands to prove refinements; these commands are carried out by the theorem prover. Thus, mundane parts of proofs are automated, and multiple attempts (to correct mistakes or to even try out different approaches) are feasible.
This tool was developed as a Master thesis: