Paper Info
Title
A Static Semantics for Alloy and its Impact in Refactorings
Abstract
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, not guaranteeing the absence of type errors or semantic changes. Consequently, developers using refactoring tools must rely on compilation and tests to ensure type-correctness and semantics preservation, respectively, which may not be satisfactory to critical software development. In this paper, we formalize a static semantics for Alloy, which is a formal object-oriented modeling language, and encode it in Prototype Verification System (PVS). The static semantics' formalization can be useful for specifying and proving that transformations in general (not only refactorings) do not introduce type errors, for instance, as we show here.
Year
DOI
Venue
2007
10.1016/j.entcs.2007.03.023
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
formal object-oriented modeling language,prototype verification system,static semantics,refactoring tool,type error,semantic change,theorem proving,object models,semantics preservation,critical software development,type system,refactoring,formal semantics,object model
Prototype Verification System,Operational semantics,Programming language,Computer science,Automated theorem proving,Modeling language,Failure semantics,Theoretical computer science,Code refactoring,Semantics,Software development
Journal
Volume
ISSN
Citations 
184,
Electronic Notes in Theoretical Computer Science
2
PageRank 
References 
Authors
0.47
19
3
Name
Order
Citations
PageRank
Rohit Gheyi161840.66
Tiago Massoni224517.18
Paulo Borba3108868.71