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

[Matej Pfajfar]

> 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
>
Yes I agree that is a suitable rule. But you need a side condition - S
must not assign to V.

When you get down to writing
the VCs, then you presumably have to use e instead of E? I.e.

Annotate after (E) so that a properly anontated spec is of the form :
|- {P} REPEAT (E) {R} S {S}

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

Does this look OK?


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.