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

[Matt Williams]

On Mon, 27 May 2002, Matej Pfajfar wrote:

> |- { 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??

The pre- and post-conditions of the REPEAT command do not contain Vs (they
are substituted out).

The pre- and post-conditions of S do contain Vs.  However, we need a
variable to count iterations with.  I believe that we can perform any
substitution we like on the whole rule before we apply it, so we should be
able to replace V with any unused variable.  It might, in fact, be better
for us to use a ghost variable, e.g. v, to store the iteration count as
this means that we do not need the side condition that E and C cannot
touch V.

BTW, looking at the question, it says "n is the value of E in the initial
state".  This implies that E may change during the computation (otherwise
it would not be necessary to state when it is evaluated).  Therefore, I
think we need to evaluate E initially, store this value in a ghost
variable and use the ghost variable for our bounds checking, something
like this:

  |- { P /\ (1 <= v) /\ (v <= e) } S { P[v+1/v] }
--------------------------------------------------- (REPEAT)
|- { P[1/v] /\ (E = e) /\ (1 <= e) } S { P[e+1/v] }

We do not need any side conditions.

Any thoughts?

Matt