Tutorial for Alloy Analyzer 4.0

Alloy is a lightweight modelling language for software design. It is amenable to a fully automatic analysis, using the Alloy Analyzer, and provides a visualizer for making sense of solutions and counterexamples it finds.

This introduction to Alloy includes:

This tutorial does not:

Instructions for using this tutorial

The main text of the tutorial will appear in this frame of the window. We will use running sample models, displayed in the top-right frame. Relevant side notes will be loaded in the bottom-right frame. Sidenotes provide supplemental information and can be skipped without impeding your understanding of the current model.

The Chapters (start here)

Alloy was developed at MIT by the Software Design Group under the guidance of Daniel Jackson. This research was funded by grant 0086154 from the ITR program of the National Science Foundation, by a grant from NASA, and by an endowment from Doug and Pat Ross.

This tutorial was originally written by Rob Seater and Greg Dennis. It has since been updated to match the new Alloy4 syntax by Daniel Le Berre and Felix Chang.