🚀 go-pugleaf

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                        |