🚀 go-pugleaf

Has anyone written a relatively complete Hoare-style proof
rule for the angelic choice construct?
(See Broy's article in TCS, Vol. 45, Number 1, 1986.)
The idea is that
	E1 -ac- E2
executes either E1 or E2, but will angelically choose
the one that terminates if there one.
This is like running both E1 and E2
in parallel, and picking the result of the first
to terminate.  For example,
	(print 3) -ac- (loop-forever)
will print 3, and
	(print 3) -ac- (print-or-loop-forever 4)
may print either 3 or 4, but will not loop forever.

The obvious proof rule is that the desired post-condition
has to follow from the desired pre-condition for both
E1 and E2.  But such a rule is incomplete if one
is reasoning about total-correctness, as one cannot,
for example, prove that the expression
	(print 3) -ac- (loop-forever)
will print 3.  Has anyone done better?

	Gary Leavens
P.S. I realize that this is more of a verification
question, as opposed to a specification question.
But there's no comp.verification :-).
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State University, Ames, Iowa 50011-1040, USA
	phone: (515) 294-1580