Skip to main content
Kent Academic Repository

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)

Abstract

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 Nov 2021 10:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21948 (The current URI for this page, for reference purposes)

University of Kent Author Information

Cavalcanti, Ana L. C..

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.