[CST-2] Spec&Ver I

[Matt Williams]

On Mon, 27 May 2002, Jamie Shotton wrote:

> On page 27 of the notes he gives an apparently incorrect rule for CASE
> statements.  The hint he gives to prove the rule incorrect doesn't seem
> to help, as you simply get a load of {F}C_i{Q} on the top row of the
> rule and so cannot derive the bottom row so there doesn't seem to be a
> problem...?  Anyone know what he's driving at?

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?

Matt