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?