Refine and Gabriel: Support for Refinement and Tactics

Oliveira, Marcel V. M. and Xavier, Manuela A. and Cavalcanti, Ana L. C. (2004) Refine and Gabriel: Support for Refinement and Tactics. In: Software Engineering and Formal Methods, 2004. SEFM 2004. Proceedings of the Second International Conference on. IEEE Computer Society Press pp. 310-319. ISBN 0-7695-2222-X . (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


Using Morgan's refinement calculus, we can write software in a precise and consistent way. Nevertheless, this may involve long and repetitive developments. Several refinement strategies are useful in different developments, and even in different points of a single development. A lot is gained by identifying these strategies, documenting them as tactics, and using them as single transformation rules. With this motivation, we have designed ArcAngel, a tactic language especially tailored for refinement; we have formalised its semantics and studied its algebraic laws. Even with the use of tactics, however, refinement can be a hard task and the use of tools is essential in practice. In this paper, we present Refine and Gabriel, interactive, user-friendly tools that allow us to use the refinement calculus with the support of ArcAngel tactics.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Refinement Calculus, Tactics, Tool Support
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01
Last Modified: 02 May 2014 08:26
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):