School of Computing

Refine and gabriel: Support for refinement and tactics

M V M Oliveira, M A Xavier, and A L C Cavalcanti

In 2nd IEEE International Conference on Software Engineering and Formal Methods, pages 182-196. IEEE Computer Society Press, September 2004 To appear.

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.



Bibtex Record

@inproceedings{1950,
author = {M V M Oliveira and M A Xavier and A L C Cavalcanti},
title = {Refine and Gabriel: Support for Refinement and Tactics},
month = {September},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {To appear},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1950},
    publication_type = {inproceedings},
    submission_id = {10904_1093006843},
    booktitle = {2nd IEEE International Conference on Software Engineering and Formal Methods},
    publisher = {IEEE Computer Society Press},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014