Skip to main content

Tactics of Refinement

Oliveira, Marcel V. M., Cavalcanti, Ana L. C. (2000) Tactics of Refinement. In: 14th Brazilian Symposium on Software Engineering. . pp. 117-132. (KAR id:21948)

Language: English
Download (288kB) Preview
[thumbnail of Tactics_of_Refinement.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Formal methods, program development, refinement calculus, tactic language
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 13 Sep 2009 18:18 UTC
Last Modified: 16 Feb 2021 12:32 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year