I'm reading the seminal "Monitors" paper by Hoare. On page 4 he proceeds with a logical proof using syntax I've never seen before, and neither know what it's called or how to properly read it.
Excerpts:
... This gives the proof rule for waits:
g {b.wait} g & B
... Thus the proof rule for a signal is:
g & B{b.signal}g
How does one interpret this syntax? When I think of proofs I think of quantifiers and implications, of which I see none here.