[CST-2] Spec&Ver I

[Matej Pfajfar]

The rule *is* wrong.
The problem with it is that it does not specify wha happens when none of
the commands get executed (i.e. when x is not a number between 1 and n).

Modify the rule to include the antecedent |- (P /\ E=0) => Q .

I think?

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?
>
> Cheers,
> Jamie
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>

Matej Pfajfar
St John's College, University of Cambridge, UK

GPG Public Key @ http://matejpfajfar.co.uk/keys
Most people are good people, the rest of us are going to
run the world. -- badbytes

WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
         15/07/2002. PLEASE USE mp@cantab.net.