[Solved]: Why does the state remain unchanged in the small-step operational semantics of a while loop?

Problem Detail: 

Usually I see that in the structural operational semantics representation for the while loop, the program state don't change:

$(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> then \>S; (while \> B \> do \>S) \> else \> SKIP, \sigma)$

For me, this not intuitive, if the state don't change (i.e. the status of the memory stays the same) then $B$ will continue to stay true and the program will never terminate.

Can anyone please explain why the state don't change in this rule?

Asked By : El Marce

Answered By : Hans Hüttel

In programming language semantics, the notion of program state is not a vague philosophical notion, but a very precise mathematical one. A state $s$ in this small-step operational semantics is a partial function

$$ s : \mathbf{Var} \hookrightarrow \mathbb{Z} $$

that records the values of the variables. So if $s\, x = v$, then variable $x$ has value $v$. The state is necessarily a partial function, since it only makes sense to record the values of variables that actually occur.

The unfolding axiom

$$ \langle \texttt{while}\; b\; \texttt{do}\; S,s \rangle \Rightarrow \langle \texttt{if}\; b\; \texttt{then}\; S; \texttt{while}\; b\; \texttt{do}\; S \; \texttt{else skip},s \rangle$$

is simply telling us that we unfold a while-loop into a conditional statement, one of whose branches contains the loop. No variables will change their value because of this, and for this reason the state does not change.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/64675