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 you have read our privacy policy.

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