Assignment 5 (due Wednesday, Feb 11 at the start of class)

Read Chapter 2 (sections 2.2 and 2.3 are just a collection of examples: read as much as you need). Read Sections 3.1-3.3. 

1. [20 points] Problem 1.9(a) of textbook.  To establish an invariant, give a
short argument about the relevant transitions.  [So for each invariant, list
the relevant transitions, and then, for each relevant transition, give a short
argument that it preserves the invariant.  The argument you give for a
transition can be informal.]

[Also, please prove all of the invariants listed, even if you don't need them
to prove mutual exclusion. We want to emphasize that a good way to attack a
new program is to first prove all the invariants that seem true and then use
them to prove the program properties that you care about, such as mutual
exclusion, etc.]


2. [20 points] Problem 2.2 of textbook.

3. [20 points] Problem 2.11 of textbook.