Refactoring Alloy Specifications
Rohit Gheyi, Paulo Henrique Monteiro Borba · Electronic Notes in Theoretical Computer Science · 2004
This paper proposes modeling laws for Alloy, a formal object-oriented modeling language. These laws are important not only to define the axiomatic semantics of Alloy but also to guide and formalize popular software development practices. In particular, these laws can be used to formaly refactor specifications. As an example, we formally refactor a specification for Java types.