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

[Matthew Monaghan]

On Mon, 27 May 2002, Matej Pfajfar wrote:

> Yes I agree that is a suitable rule. But you need a side condition - S
> must not assign to V.

Technically S shouldn't even read from V, because it doesn't actually
exist.  I think what Matt said (I think it was Matt?) about specifying V
as a variable that isn't used anywhere in the program would be a good
idea.

I don't know if we're meant to enforce the syntax of the language or not
with floyd-hoare logic.  But I guess it can't hurt?

> VCs are then :
>
> (i) P => R[1/V]
> (ii) R[e+1/V] => Q
> (iii) VCs for {R n 1<=V n v<=e} S {R[V+1/V]}
> (iv) syntactic condition that S does not assign to V

I'm assuming you meant V and not v in iii.
That looks fine to me, it's only a very slight change to the FOR rule
after all,

cya
-- 
Matt