ArcAngel
ArcAngel: a tactic language for refinement. 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
Keywords for this software
References in zbMATH (referenced in 14 articles , 1 standard article )
Showing results 1 to 14 of 14.
Sorted by year (- Ribeiro, Pedro; Cavalcanti, Ana: Angelic processes for CSP via the UTP (2019)
- Zeyda, Frank; Oliveira, Marcel; Cavalcanti, Ana: Mechanised support for sound refinement tactics (2012)
- Cavalcanti, Ana; Clayton, Phil; O’Halloran, Colin: From control law diagrams to Ada via \textsfCircus (2011)
- Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana: A tactic language for refinement of state-rich concurrent specifications (2011)
- Zeyda, Frank; Cavalcanti, Ana: Automating refinement of Circus programs (2011)
- Aspinall, David; Denney, Ewen; Lüth, Christoph: Tactics for hierarchical proof (2010)
- Iliasov, Alexei; Troubitsyna, Elena; Laibinis, Linas; Romanovsky, Alexander: Patterns for refinement automation (2010)
- Utting, Mark; Malik, Petra; Toyn, Ian: Transformation rules for Z (2010)
- Zeyda, Frank; Oliveira, Marcel; Cavalcanti, Ana: Supporting ArcAngel in ProofPower (2009) ioport
- Aspinall, David; Denney, Ewen; Lüth, Christoph: A tactic language for hiproofs (2008)
- Oliveira, M. V. M.; Cavalcanti, A. L. C.: \textsfArcAngelC: a refinement tactic language for Circus (2008) ioport
- Xavier, Manuela; Cavalcanti, Ana: Mechanised refinement of procedures (2007) ioport
- Rukšėnas, Rimvydas: A rigorous environment for development of concurrent systems (2004)
- Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim: ArcAngel: a tactic language for refinement (2003)