[CST-2] Spec Ver I - 1997/7/1

[Matej Pfajfar]

> His definition of FOR on page 20 says FOR has a "BEGIN VAR V" itself
> anyway.  If you just use FOR and specify as a side conditon that V can't
> be used at all inside C it should work.
>
> I think the FOR rule enforces the BLOCK rules side condition through the
> P[E1/V] and P[E2+1/V] conditions, the V is never let out into the wild.
But if you apply the FOR rule, you get something like :

REPEAT (E) S = FOR V := 1 to E DO C

So :

|- { P /\ (1 <= V) /\ (V <= E) } C {P[V+1/V]}
---------------------------------------------- (REPEAT)
|- { P[1/V] /\ (1 <= E) } REPEAT (E) C {P[E+1/V]}

where C does not assign to E or V.

I am confused thogh, as to how this can work with the Vs in the pre- and
post- conditions. The original repeat statement has no Vs in it, and
neither should the pre-/post conditions??


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.