Tool Support for the Refinement Calculus

Abstract

This thesis describes a project that considers how to provide tool support for the refinement calculus. Some extensions are made to the calculus that better represent the context in which a program development by refinement is done. Some of the aims of the project were to provide an environment for developing programs using the refinement calculus, and to explore the kind of support that might be useful in a tool based on that method. A model of the process of doing refinement is developed, and the design of a tool for supporting that model is described. With such a tool, we were able to more easily investigate properties of the refinement calculus itself, understanding the structure of developments and exploring ways of making developments easier to produce and understand. One of the main features of the project (and of the tool) is the emphasis on discovering, representing and automating strategies for discovering refinements and for structuring the description thereof. We developed a hierarchy of reusable derivation fragments that could be used to automate development steps. The use of our prototype tool is illustrated by means of two case studies, which are then used to illustrate various aspects of the detailed design of the tool, and to illustrate the strategies.