Name
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. Even developers using refactoring tools have to rely on compilation and tests to guarantee the semantics preservation, which may not be satisfactory to critical software development. This work proposes a set of primitive structural semantics-preserving transformations for Alloy, a formal object-oriented modeling language. We use the Prototype Verification System (PVS), which contains a formal specification language and a theorem prover, to specify and prove the soundness of the transformations. Although our transformations are primitive, we can compose them in order to derive coarse grained transformations, such as a model refactoring to introduce a design pattern into a model. Moreover, proposing refactorings in this way can not only facilitate design, but also improve the quality of model refactoring tools. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1094855.1094938 | OOPSLA Companion |
Keywords | DocType | ISBN |
design pattern,coarse grained transformation,program refactorings,formal object-oriented modeling language,prototype verification system,primitive structural semantics-preserving transformation,object model,semantics preservation,refactoring tool,formal refactorings,formal specification language,formal semantics,software development,theorem prover,theorem proving | Conference | 1-59593-193-7 |
Citations | PageRank | References |
1 | 0.36 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rohit Gheyi | 1 | 618 | 40.66 |
| Tiago Massoni | 2 | 245 | 17.18 |