A complete set of object modeling laws for alloy

Abstract

Applying transformations to object-oriented systems usually affects source code and its associated models, involving complex maintenance efforts to keep those artifacts up to date. Most projects abandon design information in the form of models early in the life cycle, as their maintenance becomes extremely expensive. In this paper, we propose a complete catalog of object model laws (bidirectional semantics-preserving transformations) for Alloy, a formal object-oriented modeling language. We address relative completeness through a reduction process that transforms an arbitrary Alloy model into an equivalent model in a core language (normal form). We evaluate our completeness result using two distinct normal forms. © 2009 Springer-Verlag Berlin Heidelberg.