[CST-2] Spec&Ver I

[Jamie Shotton]

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

J