Imperative Alloy -- an imperative extension to Alloy

Joseph P. Near (jnear@csail.mit.edu)
March 2, 2010

Imperative Alloy is an extension of the Alloy specification language
with imperative programming constructs. This implementation of the
extension compiles specifications written in Imperative Alloy to
standard Alloy for analysis by the Alloy Analyzer.

Building the compiler requires a recent version of the Glasgow Haskell
Compiler (GHC) and the Parsec libraries. I used GHC 6.10.4 during
development. To build the compiler, type:

ghc --make compile.hs

To use it, type (e.g.):

./compile examples/farmer.als

The resulting Alloy model will appear in standard output; it is
usually redirected to a file for analysis using the Alloy Analyzer.

This prototype implementation has one important limitation: the loop
construct may have only a single named-action call in its body. Thus
the following loop is fine:

loop { write[] }

But this one will cause an error, since it contains a compound action:

loop { Cnt.idx := Cnt.idx + 1; write[] }

This limitation will be lifted in a later version.
