Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
3  
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
1  
@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
add comment

2 Answers

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

share|improve this answer
add comment

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|improve this answer
add comment

Your Answer

 
discard

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.