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 &amp; B
  
  ... Thus the proof rule for a signal is:
  
  g &amp; 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.
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.
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.