Abstract State Machines, Alloy, B and Z - Frappier, Marc; Glässer, Uwe; Glässer, Uwe; Khurshid, Sarfraz; Laleau, Régine; Reeves, Steve (Springer Berlin Heidelberg, 2010)