A rigorous approach for proving model refactorings

PDF DOI 10.1145/1101908.1101973 dblp

Abstract

Both model and program refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics. In this paper, we propose guidelines on how to rigorously prove model refactorings for Alloy, a formal object-oriented modeling language. We use the Prototype Verification System (PVS) to specify and prove the soundness of the transformations. Proposing refactorings in this way can facilitate not only design, but also improve the quality of refactoring tools.

BibTeX

@inproceedings{Gheyi-al:ASE05,
  author    = {Rohit Gheyi and
               Tiago Massoni and
               Paulo Borba},
  title     = {A rigorous approach for proving model refactorings},
  booktitle = {ASE},
  pages     = {372--375},
  publisher = {{ACM}},
  year      = {2005},
}

A rigorous approach for proving model refactorings

Abstract

Related papers