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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Oliveira, M., Cavalcanti, A. & Woodcock, J. ArcAngel: a Tactic Language for Refinement. Formal Aspects of Computing 15, 28–47 (2003). https://doi.org/10.1007/s00165-003-0003-8
Issue Date:
DOI: https://doi.org/10.1007/s00165-003-0003-8