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