Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!uakari.primate.wisc.edu!ames!uhccux!munnari.oz.au!bunyip!brolga!uqcspe!batserver.cs.uq.oz.au!brendan
From: brendan@batserver.cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification
Subject: Re: Proof rules for angelic choice?
Keywords: Hoare logic, verification
Message-ID: <4154@uqcspe.cs.uq.oz.au>
Date: 4 Jul 90 04:48:31 GMT
References: <2103@dino.cs.iastate.edu> <4106@uqcspe.cs.uq.oz.au> <4972@castle.ed.ac.uk>
Sender: news@uqcspe.cs.uq.oz.au
Reply-To: brendan@batserver.cs.uq.oz.au
Distribution: comp
Lines: 25

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                        |