leavens@cs.iastate.edu (Gary Leavens) (06/27/90)
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
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (06/28/90)
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 |
hmj@kuukkeli.tut.fi (J{rvinen Hannu-Matti) (06/28/90)
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{.
arshad@lfcs.ed.ac.uk (Arshad Mahmood) (06/30/90)
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 ---------------------------------
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (07/04/90)
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 |