Building our knowledge of Alloy on top of our existing experience of Object Z was intuitive. With hindsight, we believe not having prior knowledge of Object Z would not have made learning Alloy much more difficult. The ASCII based syntax makes for easy reading and unambigious models.

Using the Alloy Analyzer was straight-forward and the visualisation feature really helped our understanding. Nothing about the GUI is over-complex and compatibility over Linux, Mac OS and Windows is very good. The fully automated analysis feature is really helpful, instant feedback on your model makes learning more efficient.

The main disadvantage is not used very widely (yet) which can make it hard to find answers to very specific questions. Solutions to most of these issues are in Daniel Jackson's book and addressed by the official (and our!) website! Also, there is a discussion group which is unfortunately closed: you have to ask for moderator approval to be able to access it!

In our opinion, Alloy is a great starting point for beginners to specification languages because of its interactive tool support. We think that we would have preferred learning Alloy over Object-Z.