# 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.

-
Perhaps this is the eponymous Hoare logic? – Zhen Lin Feb 25 '12 at 0:25
@ZhenLin Looks like that's it! – DuckMaestro Feb 25 '12 at 0:57
@ZhenLin Maybe make this an answer and explain the basic idea of Hoare logic? – Raphael Feb 25 '12 at 9:54
@Raphael: I'm no computer scientist, I just have friends in computer science! – Zhen Lin Feb 25 '12 at 10:11

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.

-

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}

-

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.

-