Abstract | ||
---|---|---|
Using Morgan's refinement calculus, we can write software in a precise and consistent way. Nevertheless, this may involve long and repetitive developments. Several refinement strategies are useful in different developments, and even in different points of a single development. A lot is gained by identifying these strategies, documenting them as tactics, and using them as single transformation rules. With this motivation, we have designed ArcAngel, a tactic language especially tailored for refinement; we have formalised its semantics and studied its algebraic laws. Even with the use of tactics, however, refinement can be a hard task and the use of tools is essential in practice. In this paper, we present Refine and Gabriel, interactive, user-friendly tools that allow us to use the refinement calculus with the support of ArcAngel tactics. |
Year | DOI | Venue |
---|---|---|
2004 | 10.1109/SEFM.2004.37 | SEFM |
Keywords | Field | DocType |
refinement strategy,algebraic law,different point,refinement calculus,single development,hard task,repetitive development,different development,arcangel tactic,single transformation rule,formal specification | Programming language,Refinement calculus,Computer science,Formal specification,Software,Refinement,Semantics,Computer programming,Algebraic laws | Conference |
ISBN | Citations | PageRank |
0-7695-2222-X | 11 | 0.90 |
References | Authors | |
8 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Marcel Oliveira | 1 | 172 | 12.57 |
Manuela Xavier | 2 | 19 | 1.87 |
Ana Cavalcanti | 3 | 668 | 59.95 |