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. (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):
