[CST-2] Spec&Ver I

[Barnaby Gray]

On Mon, May 27, 2002 at 11:42:33AM +0100, Jamie Shotton wrote:
> > 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.

Hehe.. if you feel like writing everyone of them out, I suspect you
can shortcut stuff like this fine and he won't mind.

Barnaby