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

[Matthew Monaghan]

On Sun, 26 May 2002, Matej Pfajfar wrote:

> Can anyone help me out with this question? It asks you to devise a proof
> rule for |- {P} REPEAT (Y) S {Q}.
>
> I've tried rewriting it as BEGIN VAR V; FOR V := 1 to Y DO S END and
> deriving the rule from that but it doesn't seem to work due to
> side conditions in the BLOCK rule.

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.

This means there should be no trouble putting another BEGIN...END
statement around it.  In fact it shouldn't alter the basic FOR rule at
all?

I hope this makes sense (and is right, it's a bit late to be thinking
after all :)

cya
-- 
Matt