A Static Semantics for Alloy and its Impact in Refactorings

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 c...