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.
To execute, simply double-click on the jar file, or type java -jar alloy4.jar in a console.
| FAQ | Frequently asked questions about Alloy |
| reference | Download language reference for Alloy 4 (PDF) |
| comparisons | Comparisons to Z, B, VDM and OCL (PDF) |
| grammar | A grammar for Alloy 4 in plain text (TXT), also see the cup file |
| quick guide | Overview of new features in Alloy 4 |
| Alloy API | Documentation for Alloy API |
| Alloy API Examples | examples of using the compiler, the ast, the evaluator |
| 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 |