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

In article <4106@uqcspe.cs.uq.oz.au> brendan@batserver.cs.uq.oz.au writes:
>leavens@cs.iastate.edu (Gary Leavens) writes:
>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 Institution line is not complete, and seems to be in Swedish
(although in Finland, Swedish is used in Abo Akademi). The 
complete English version is:
Abo Akademi University,
Department of Computer Science,
Lemmink{inengatan 14,
20520 Abo,
Finland
({ is a with two dots, i.e., a diaresis or "umlaut a")

You may also be interested in the second part:
R. J. R. Back, Refinement Calculus, Part II, Parallel and Reactive Programs


-----
Hannu-Matti Jarvinen, hmj@tut.fi
Opinions of tut != opinions of mine, and vice versa.
TTKK on samaa mielt{ kanssani siit{, ett{ en edusta sen mielipidett{.

Sorry for wasting bandwidth with this extension to my earlier message.

>Hoare-style
>
>	{Q}E1{P} or {Q}E2{P}
>	--------------------
>	 {Q}(E1 -ac- E2){P}
 
I think you mean

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

The rule as given has silly behaviours like {Q}((x := 3) -ac- (x:=4)){x=3}
is valid, and of course {Q}((x:=3) -ac- (loop)){ANYTHING} is valid since
a looping program vacously satisfies any post-condition.

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

This tableau is not quite correct, the reason is as given above the looping
part of it will be vacously true.

>Brendan Mahony

A. Mahmood
LFCS
Edinburgh University
Scotland
---------------------------------

arshad@lfcs.ed.ac.uk (Arshad Mahmood) writes:

>The rule as given has silly behaviours like {Q}((x := 3) -ac- (x:=4)){x=3}
>is valid, and of course {Q}((x:=3) -ac- (loop)){ANYTHING} is valid since
>a looping program vacously satisfies any post-condition.

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

>This tableau is not quite correct, the reason is as given above the looping
>part of it will be vacuously true.

Actually the term is miraculous behaviour. My semantics of loop would be

	wp(loop,R) = false,	for all predicates R

that is loop never terminates, and vacuously fails any post-condition.
The tableau is correct and is not vacuous.
--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       |
Department of Computer Science   |
University of Queensland         |
Australia                        |