Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.

Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.

The home page for Alloy is http://alloy.mit.edu/.

Tutorials and documentation

  1. MIT Alloy tutorial page
  2. Official Alloy documentation

Reference books

  1. Software Abstraction by Daniel Jackson