ArcAngel: a tactic language for refinement

Oliveira, M.V.M and Cavalcanti, A.L.C. and Woodcock, J.C.P. (2003) ArcAngel: a tactic language for refinement. Formal Aspects of Computing, 15 (1). pp. 28-47. ISSN 0934-5043 . (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://www.cs.kent.ac.uk/pubs/2003/1793

Abstract

Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this paper, we present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we are extending, no other tactic language has a denotational semantics and proof theory of its own.

Item Type: Article
Additional information: The full version of this work can be found in the Masters Thesis by M Oliveira
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:00
Last Modified: 14 Mar 2009 17:56
Resource URI: http://kar.kent.ac.uk/id/eprint/13853 (The current URI for this page, for reference purposes)
  • Depositors only (login required):