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

[Matej Pfajfar]

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.

Any ideas?

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
         30/09/2002. PLEASE USE mp@cantab.net.