Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!mintaka!bloom-beacon!eru!luth!sunic!mcsun!ukc!edcastle!lfcs!arshad
From: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Newsgroups: comp.specification
Subject: Re: Proof rules for angelic choice?
Keywords: Hoare logic, verification
Message-ID: <4972@castle.ed.ac.uk>
Date: 30 Jun 90 10:11:28 GMT
References: <2103@dino.cs.iastate.edu> <4106@uqcspe.cs.uq.oz.au>
Reply-To: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Distribution: comp
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 33

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