Re: Off Topic? Guarded commands...

["Peter H. Froehlich" <address@hidden>]

Hi there!

On Wednesday, December 12, 2001, at 04:59 , Michael Vanier wrote:

> Can someone give a quick explanation of
> what is meant by guarded commands?

Guarded commands refer to particular kinds of control structures 
invented (if I remember correctly) by Dijkstra. The "canonical" 
reference seems to be his classic book "Structured Programming". 
Here is what they look like:

Guard = Condition "->" Instructions .
If = "if" Guard { "|" Guard } "fi" .
Do = "do" Guard { "|" Guard } "od" .

I don't want to define Condition and Instructions, but whatever you 
imagine is probably right.

For the If, the "semantics" are as follows: If the set of "true" 
Guards is not empty, choose any Guard (non-deterministically) and 
execute it's instructions; then execute whatever follows the If. 
Otherwise abort the computation ("throw an exception").

For the Do, the "semantics" are as follows: While the set of "true" 
Guards is not empty, choose any Guard (non-deterministically) and 
execute it's instructions. Otherwise execute whatever follows the 
Do.

So for example, instead of writing

   def max( a, b ):
     if a > b:
       return a
     else:
       return b

and just "lumping" a lot of assumptions into the "else", you would write

    def max( a, b ):
      if
        a >= b: return a
       |a <= b: return b
      fi

and be real explicit about what you mean, especially about the fact 
that it does not matter whether a or b is returned if a == b holds. 
Anyway, that's my short version of it. Seems that it is easier to 
proof things about guarded commands than about the common 
deterministic control structures, but I leave that for someone else 
to explain. Hope it helps.

Peter
--
Peter H. Froehlich @ http://www.ics.uci.edu/~pfroehli/