I'm trying to construct the small-step semantic rules involving the for-loops, but I can't find anything about it in the literature (only about while-loops).

I was wondering if anyone could help me out with this? This is a first attempt, where $s$ represents a statement and $e$ an expression:

$\quad \displaystyle\sigma, \text{for } s_1 \, e_1 \, e_2 \, s_2 \, \rightarrow \, \sigma, \text{if } e_1 \text{ then (} s_2 ; \, e_2; \, \text{for } s_1 \, e_1 \, e_2 \, s_2 \text{ ) else } skip$

Where $\sigma$ is a local value store, $s_1$ is for example $i = 0$, $e_1$ could equal $i < 4$ and $e_2$ $i=i+1$.


1 Answer 1


Your attempt does not work. Note that $s_1$ is never executed. (And if you prepend the right-hand side with "$s_1;$", it will be executed multiple times.)

What you can do is to translate the for loop into an equivalent while loop:

$$\sigma,\text{for } s_1, e_1, e_2, s_2 \text{ endfor} \to \sigma, s_1; \text{while } e_1 \text{ do } s_2; e_2 \text{ endwhile}.$$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.