[CST-2] Spec&Ver I

[Jamie Shotton]

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

Ok then if you use precondition strengthening lots of times.

J