Tactics of Refinement
Marcel Oliveira, Ana Cavalcanti · 2000
The refinement calculus is a modern technique of formal program development. Its application, however, may lead to long and repetitive developments. In this paper we present a language to write refinement tactics, and present examples of useful tactics. They encompass the application of several refinements laws, but can be user as a single transformation rule. Using tactics is not a novel idea, but apparently, in the context of refinement the only existing work uses Prolog as a tactic language. 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.