D. Carrington, I. Hayes, R. Nickson, G. Watson and J. Welsh
Software Verification Research Centre, Department of Computer Science, The University of Queensland, St. Lucia, 4072, Australia.
We also discuss how refinement and proof can be integrated, either using a multi-lingual document or by using a version of window inference that directly supports the refinement relation. The integration of refinement and proof has the benefit that tools supporting these activities can present a single consistent user interface. We describe prototype tools for refinement and proof, based on a window inference theorem prover with an Emacs interface, and using a sophisticated multi-lingual document editor.