[CST-2] Spec&Ver I

[Matt Williams]

On Mon, 27 May 2002, Jamie Shotton wrote:

> > I think the point is that the natural language specification
> > states that
> >
> > (ii) If x is not a number between 1 and n, then the
> > CASE-command has no
> >      effect.
> >
> > I believe that the "proof" of the case he states should have
> > come out as
> >
> > ------------------------- (ASSIGNMENT)  **********
> > |- {X=0 n 0=1} Y:=0 {Y=0}
> > --------------------------------------- (CASE)
> > |- {X=0} CASE 0 OF BEGIN Y:=0 END {Y=0}
> >
> > This is clearly false, since the CASE-command should do
> > nothing.  To fix the rule, simply add |- (P n E=0) -> Q to
> > the top row, giving
> >
> > |- (P n E=0) -> Q, |- {P n E=1} C_1 {Q}, ..., |- {P n E=n} C_n {Q}
> > --------------------------------------------------------------
> > ---- (CASE)
> > |- {P} CASE E OF BEGIN C_1; ... ; C_n END {Q}
> >
> > Does this make sense?
>
> Yup - I had not anticipated the fact that you could use the assignment
> axiom where you have.  I was under the impression that {X=0 /\ 0=1}
> could be instantly reduced to {F} but I take it that in fact, it is not
> possible to do these inline modifications - you still have to go through
> the axioms and rules of the system...?

I think you have to go through the axioms and rules of the system.

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.

Cheers,

Matt