Specification and Verification Tools Seminar
			      Homework 2
		     $Date: 2008/09/21 16:14:25 $

For September 24, 2008.

Download and install Spec# from http://research.microsoft.com/SpecSharp/.
You can install Microsoft's Visual Studio (the system support staff
has a copy at UCF, which does not require payment or extra license) if
you have a Microsoft Windows XP or Vista machine.  If you use Visual
Studio, be sure to open up a Spec# project for working on this homework.

You can also use the downloaded Spec# executable without Visual
Studio.  Simply invoke C:\Program Files\Microsoft\Spec#\bin\ssc.exe
with the name(s) of the file(s) you want to check as argument(s).

Read the Spec# overview from

  http://research.microsoft.com/SpecSharp/papers/krml136.pdf 

While reading, play with Spec# to test out questions you have.
(You can also bring questions to the seminar.)

Then, using Spec#, specify and correctly implement a doubly-linked list.
with an invariant specifying how nodes must link to each other.
The particular properties and design are up to you; there's no right
answer.  We'll discuss your solution in the seminar.