Monitor Invariant - Buffer
Monitor Invariant - Buffer
A monitor invariant is an assertion which is true whenever no thread is executing in the monitor. It is permitted to be false while a a thread is executing but must be true when the thread leaves the monitor by method return or wait().
A suitable monitor invariant for Buffer which satisfies the safety properties is:
Buffer Invariant: [0 £ count £ size]
The count = 0 initialisation establishes the invariant.
synchronized public void put(Object o) {
// [0 £ count £ size]
while (count==size) {… wait() …}
… // [0 £ count < size]
++count;
… // [0< count £ size]