This is an outright lie; the proof technique that follows is way too simple to
actually prove liveness properties. For example, P doesn't have to be
true every time execution hits it; it just has to be true one of those times.
Also, you can assume that all previous times that execution hit P, it was
equivalent to false (otherwise, you would have completed the proof).
The methods and techniques required to prove general liveness properties are involved and subtle. It will be enough for this class, and for concurrent programming in general, that you remember what liveness properties are and be able to argue their liveness with hand-waving, but convincing, arguments.
This page last modified on 25 June 2003.