🚀 go-pugleaf

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