3
$\begingroup$

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.

  • 0
    @Raphael: I'm no computer scientist, I just have friends in computer science!2012-02-25

3 Answers 3

4

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.

3

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}

-2

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.