Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.


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

share|cite|improve this question
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
up vote 4 down vote accepted

As Zhen Lin points out, this Hoare logic, a logical calculus. It is designed to model pre- and post-conditions of programs:

{ P }
{ 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\}}$


$\qquad\displaystyle \frac{}{\{P[c/x]\}x:=c\{P\}}$

that effectively define your language's semantics.

share|cite|improve this answer

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}

share|cite|improve this answer

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.