Oliveira JN, Ferreira M.? 2013.??Alloy Meets the Algebra of Programming: A Case Study. IEEE Transactions on Software Engineering. 39:305-326.