Re: Off Topic? Guarded commands...

[Viktor Kuncak <address@hidden>]

Peter H. Froehlich:

 > Isn't that the very "best" property of guarded commands, that they 
 > are non-deterministic? If you transform something like

They are nondeterministic, and that makes them handy for some things.

I used it in my intermediate language for role analysis

http://www.cag.lcs.mit.edu/~vkuncak/papers/RoleAnalysis.ps.gz

and many others use it as an intermediate language, as you pointed out. 
It is also used in the Dynamic logic:

@Book{HarelETAL00DynamicLogic,
  author =       {David Harel and Dexter Kozen and Jerzy Tiuryn},
  title =        {Dynamic Logic},
  publisher =    MIT-P,
  year =         2000,
  keywords =     {logic, verification},
  obtained =     {QA76.9.L63.37 2000},
  affiliation =  {Weizmann, Cornell, Warsaw}
}

Some people don't like it (not me) for the following reason:
if you have no syntactic restrictions on the guarded command
language, you can write in the intermediate representation
programs that would never be generated as a result of the
translation.  But that is not really a problem, because the
analysis can handle the general nondeterministic language
anyway.

 > if a -> A() | b -> B() | c -> C() fi
 > 
 > into (Python-esque)
 > 
 >    if a:
 >      A()
 >    elif b:
 >      B()
 >    elif c:
 >      C()
 >    else:
 >      raise "Condition not covered!"
 > 
 > your implementation will satisfy the "guarantees" that the guarded 
 > command makes and it will not be "inefficient" compared to the 
 > plain deterministic version.

In principle, I agree here as well, but there might be some
problems.

The translation you suggest is an "implementation" of the
guarded command language.  By implementation I mean that the
executions (traces) of the translated program are a subset
of the executions of the original guarded command language.
If you only care about partial program correctness (safety
properties, i.e. bad things don't happen), then the
translation is theoretically good enough.  I am not so sure
that the translation would be acceptable for liveness
properties (such as absence of deadlocks).

On the more practical side, if the language is specified as
nondeterministic and the implementation uses a particular
deterministic strategies than programmers (for some strange
psychological reasons) end up relying on the way this feature
is implemented.  Then programs do not work on the implementation
which translates the guarded command language e.g. backwards...
So my guess is that people just pick the order of tests to
avoid this thing from happening.

  Viktor