The purpose of this model is to present a simple denotational semantics for the simple language depicted in Nielson. The syntax is represented by Alloy functions, the semantics by relations between states and domains appropriate to the construct.

---------------------------------------------------------------
      Relational Denotational Semantics of the While language
      Jason S. Reich and Jeremy L. Jacob
      {jr523,jeremy.jacob}@cs.york.ac.uk
      Department of Computer Science, University of York, UK

Language as described in Nielson and Nielson, Semantics with Applications: An appetizer, Springer, 2007.
@book{Nielson,
      author = {Hanne Riis Nielson and Flemming Nielson},
      title = {Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science)},
      year = {2007},
      isbn = {1846286913},
      publisher = {Springer-Verlag New York, Inc.},
      address = {Secaucus, NJ, USA},
}
------------------------------------------------------------