Tactics of Refinement

The refinement calculus is a modern technique to develop and implement software in a precise, complete, and consistent way. Its application, however, may lead to developments that are long and repetitive. In this paper we present a language which can be used to write refinement tactics that capture commonly used development strategies, and present examples of useful tactics. They encompass the application of several refinement laws, but can be used as a single transformation rule. Using tactics is not a novel idea, particularly in the area of theorem proving. Nevertheless, as far as we know in the context of refinement the only existing work uses Prolog to write tactics. Our language does not depend of any programming language or tool. Also, we are not aware of any presentation of refinement strategies written in the form of tactics as we present here. Our results are going to be incorporated in a tool to support the application of the refinement calculus that is under development.