[CST-2] Spec&Ver I

[Barnaby Gray]

On Mon, May 27, 2002 at 11:37:57AM +0100, Jamie Shotton wrote:
> > 
> > On Mon, May 27, 2002 at 11:22:33AM +0100, Matt Williams wrote:
> > > I think that in fact there's a mistake in my proof.  I suspect that 
> > > you need to use pre-condition strengthening and post-condition 
> > > weakening so that you convert (X=0 n 0=1) into (X=0 n 0=1 n 
> > 0=0) and 
> > > you convert (X=0 n 0=1 n Y=0) into (Y=0).  You then apply the 
> > > assignment axiom.
> > 
> > I think it's clearer just to say (X=0 n 0=1) is clearly 
> > false, and since F => anything, then choose the anything to 
> > be 0=0, and by precondition strengthening you then get the 
> > assignment axiom.
> 
> But then that's not technically following the rules of the system...

Yes it is:
 X=0 n 0=1 => X=0 n F => F

I'm sure you can do that?

Barnaby