[CST-2] Spec&Ver I

[Jamie Shotton]

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

J