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.