documentation

Alloy 4 is a self-contained executable, which includes the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples. The same jar file can be incorporated into other applications to use Alloy as an API, and includes the source code. See the release notes for details of new features. To execute, simply double-click on the jar file, or type java -jar alloy4.jar in a console.

Materials available

FAQ
Frequently asked questions about Alloy
reference
Language reference for Alloy 4
comparisons
Comparisons to Z, B, VDM and OCL
grammar
A grammar for Alloy 4 in plain text
quick guide
Overview of new features in Alloy 4
Alloy API
Documentation for Alloy API
online tutorial
A step-by-step walkthrough and tutorial for Alloy 4
tutorial slides
Slides for day-long tutorial by Rob Seater and Greg Dennis
digital humanities tutorial
A tutorial introducing Alloy for digital humanities work, by C. M. Sperberg-McQueen