Structured Presentation of Refinements and Proofs

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.
{davec,ianh,nickson,gwat,jim}@cs.uq.edu.au

Abstract

Refinement is a transformational method for developing programs from specifications. It generates a hierarchical structure representing design decisions. Proofs may also be viewed as hierarchical structures. The window inference proof paradigm explicitly takes advantage of hierarchical structure in proofs, and is well suited to program refinement. Both program refinements and proofs structures are complex, and powerful tools are needed to manage and present them. We discuss several approaches to the presentation of such structures, and tools to support these approaches.

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.

Conference Home Page