gotchaModerate
Why does the state remain unchanged in the small-step operational semantics of a while loop?
Viewed 0 times
whythewhilesemanticsloopunchangedremainsmallstatedoes
Problem
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?
$(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?
Solution
The state can change in subsequent reduction steps because on the right hand side of
$$
\langle while\ B\ do\ S, \sigma \rangle
\quad\rightarrow\quad
\langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle
$$
the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the condition $B$ can evaluate to $\mathsf{false}$.
$$
\langle while\ B\ do\ S, \sigma \rangle
\quad\rightarrow\quad
\langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle
$$
the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the condition $B$ can evaluate to $\mathsf{false}$.
Context
StackExchange Computer Science Q#64675, answer score: 10
Revisions (0)
No revisions yet.