🚀 go-pugleaf

leavens@cs.iastate.edu (Gary Leavens) writes:


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

Weakest pre-condition semantics.

	wp(E1 -ac- E2, P) = wp(E1,P) or wp(E1,P)

Hoare-style

	{Q}E1{P} or {Q}E2{P}
	--------------------
	 {Q}(E1 -ac- E2){P}

This operator is usually termed "or". It is not the same as running in
parallel, but rather can be liken to backtracking.

For more information I suggest you read:

@techreport{Back:RefCal,
	Author = "R. J. R. Back and J. {von Wright}",
	title = "Refinement Calculus, Part {I}: Sequential Nondeterministic Programs",
	institution = {Institute f\"{o}r
	Informationsbehandling, Lemmink\"{a}inengatan},
	type = {Technical Report},
	number = {Ser. A, No 92},
	year = 1989
}

>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?

	wp((print 3) -ac- (loop-forever), output = 3)
	= wp((print 3), output = 3) or wp((loop-forever), output = 3)
	= true or false
	= true

Getting a semantics for an operator that correspond to running the
programs in parallel is a bit harder.
--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       |
Department of Computer Science   |
University of Queensland         |
Australia                        |