Functional Alloy Modules

The Alloy language was developed as a lightweight modelling language that allows fully automatic analysis of software design models
via SAT solving. The practical application of this type of analysis is
hampered by two limitations: first, the analysis itself can become quite
time consuming when the scopes become even moderately large; second,
determining minimal scopes for the entity types (limiting the number of
entities of each type) to achieve better running times is itself a non-trivial problem.

In this paper we show that for the special case of Alloy modules specifying
transformations we may be able to circumvent these limitations. We
define the corresponding notion of functional module and define precise
conditions under which such functional modules can be efficiently interpreted
rather than analysed via SAT solving and we also explain how
interpretation of functional Alloy modules can be seamlessly integrated
with the SAT-based analysis of other modules. We provide evidence that
for complex transformations interpreting functional modules may result
in significant time savings.