How has Alloy been used in teaching?

Alloy is an attractive teaching tool, for two reasons. First, the language is very close to first order logic with relational operators. The syntax and semantics are very simple and uniform. The latest version improves on its predecessor in this respect: the language semantics is now untyped, so it can be explained without reference to types, and the language is more flexible (but at the same time the type checker itself is actually more powerful!). Second, the Analyzer gives students immediate, concrete feedback; the graphical display seems to help a lot too.

Alloy has been taught in courses at about 15 universities worldwide, in most cases as one of two or three approaches, including: Michigan State (by Laura Dillon), Imperial College (by Michael Huth), National University of Singapore (by Jin Song Dong), University of Iowa (by Cesare Tinelli), Queen’s University (by Juergen Dingel), University of Waterloo (by Joanne Atlee), Worcestor Polytechnic (by Kathi Fisler), University of Wisconsin (by Somesh Jha), University of California at Irvine (by David Rosenblum), Kansas State University (by John Hatcliff and Matt Dwyer), University of Southern California (by Nenad Medvidovic), Georgia Tech (by Colin Potts), Politecnico di Milano (by Carlo Ghezzi), University of Washington (by Rob DeLine), Auckland (John Hamer). The courses at Kansas State, Imperial and Politecnico di Milano include several weeks’ worth of material on Alloy, and the latest version of the textbook by Michael Huth and Mark Ryan (Logic in Computer Science: Modelling and reasoning about systems; Cambridge University Press) includes a chapter on Alloy. At MIT, we have found that students can learn Alloy in a few weeks with only limited background in discrete maths.