Tactics of Refinement

Oliveira, M.V.M. and Cavalcanti, A.L.C. (2000) Tactics of Refinement. In: 14th Brazilian Symposium on Software Engineering, 4-6 October, 2000, Joao Pessoa - Paraiba - Brazil. (Full text available)

PDF
Download (164kB)
[img]
Preview

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: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 13 Sep 2009 18:18
Last Modified: 06 Sep 2011 04:08
Resource URI: http://kar.kent.ac.uk/id/eprint/21948 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year