0
$\begingroup$

We add the following derivation rule to the structural operational semantic:

< repeat S until b, s >$\Rightarrow$ < S; if b then skip else (repeat S until b) >

Prove that "repeat S until b" is equivalent to "S; if b then skip else (repeat S until b)" in the structural operational semantic.

I've tried the following:

In one direction:

Asumming < S; if b then skip else (repeat S until b), s > $\Rightarrow^*$ s'

We can prove < repeat S until b, s > $\Rightarrow$ s'

by using the specified derivation rule and the assumption:

< repeat S until b, s >$\Rightarrow$ < S; if b then skip else (repeat S until b) > $\Rightarrow$ s'

How can we prove the other direction?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.