A third year undergraduate course in the basics of specification of systems and a very rudimentary introduction to refinement/reification.

Both a state-based (a la VDM & Z) style and a trace-based (a la CSP) style are used.

The concrete notation used to express & explore the mathematics is Alloy.