For operational semantics, you can just specify a list of inference rules.

Code:

for(i = 0; i < 10; i++)
{
// do something
}

Let b = the condition i < 10

c = the commands in the block of the loop

S = state notation

The rules would be:

Code:

<b, S> --> false
-----------------------------------
<for (i=0; b; i++) do c, S> --> S
and
<b, S> --> true <c, S> --> S'' <for (i=0; b; i++) do c, S''> --> S'
--------------------------------------------------------------------------
<for (i=0; b; i++) do c, S> --> S'