What are Alloy and the Alloy Analyzer?

Alloy is a structural modelling language based on first-order logic, for expressing complex structural constraints and behaviour. The Alloy Analyzer is a constraint solver that provides fully automatic simulation and checking. Alloy has been developed by the Software Design Group at MIT. The first Alloy prototype came out in 1997, and was a rather limited object modelling language. Later versions added quantifiers, higher arity relations, polymorphism, subtyping, and signatures (Alloy’s structuring mechanism). The performance and scalability of the tool have gradually increased. Much work has been devoted to user interface issues also, in particular in the development of a flexible visualization mechanism.