What is this proof syntax (Hoare 1974)? 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.
 A: As Zhen Lin points out, this Hoare logic, a logical calculus. It is designed to model pre- and post-conditions of programs:
{ P }
statement;
{ Q }

This means that if property P (always) holds before the statement, then Q (always) holds after its execution.
You can think of it as program annotation; you would start with some preconditions, write properties between lines and get postconditions of your programs. If these imply the desired property (given by a formal specification) your program is correct. Note that you can not annotate arbitrary properties, of course. You have to conform to rules like
$\qquad\displaystyle \frac{\{P\}S_1\{Q_1\} \quad \{Q_2\}S_2\{R\}}{\{P\}S_1;S_2\{R\}}$
or
$\qquad\displaystyle \frac{}{\{P[c/x]\}x:=c\{P\}}$
that effectively define your language's semantics.
A: By the way, in the paper cited by the OP, Hoare uses the syntax

P {statement} Q

but more recently

{P} statement {Q}

has become the norm. So you might prefer to read the given excerpts as

{g} b.wait {g & B}
{g & B} b.signal {g}

A: In proving programs correct ,some assertions are made of the format {P} Code {Q} where P and Q are Per and post conditions respectively.
For example:
{ x is even }
x = x+1
{ x is even }
Here pre condition and post condition are  shown, by using these we can easily check our programs correctness.
