Name
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. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/s00165-003-0003-8 | Formal Asp. Comput. |
Keywords | Field | DocType |
ensp,Formal methods,Program development,Refinement calculus | Notation,Programming language,Refinement calculus,Computer science,Denotational semantics,Proof theory,Theoretical computer science,Program Design Language,Formal methods,Semantics,Computer programming | Journal |
Volume | Issue | ISSN |
15 | 1 | 0934-5043 |
Citations | PageRank | References |
20 | 1.11 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcel Oliveira | 1 | 172 | 12.57 |
| Ana Cavalcanti | 2 | 224 | 18.41 |
| J. C. P. Woodcock | 3 | 519 | 53.82 |