[CST-2] Spec&Ver I

[Barnaby Gray]

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.

Barnaby