A Metatool for Exploring Program Algebras
Joakim Wright von · 1999
We describe how an existing tool is extended to allow exploratory reasoning in program algebras with theorem proving support. The existing tool (TkWinHOL and the Refinement Calculator) provides a graphical user interface to the window inference reasoning system for the HOL theorem prover. We show how a user with a small amount of work can build an extension to this tool, which can then be used to build, interactively and step-by-step, a whole theory for the program algebra in question. The ideas are illustrated with an extension for a simple while-language.