Pourquoi l'état reste-t-il inchangé dans la sémantique opérationnelle à petite étape d'une boucle while?

Habituellement, je vois que dans la représentation sémantique opérationnelle structurelle pour la boucle while, l'état du programme ne change pas:

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

Pour moi, ce n'est pas intuitif, si l'état ne change pas (c'est-à-dire que l'état de la mémoire reste le même) alors continuera à rester vrai et le programme ne se terminera jamais.$B$

Quelqu'un peut-il expliquer pourquoi l'État ne change pas cette règle?

Dans la sémantique du langage de programmation, la notion d'état de programme n'est pas une notion philosophique vague, mais une notion mathématique très précise. Un état dans cette sémantique opérationnelle à petite étape est une fonction partielle$s$

qui enregistre les valeurs des variables. Donc, si , alors la variable a la valeur . L'état est nécessairement une fonction partielle, car il n'a de sens que d'enregistrer les valeurs des variables qui se produisent réellement.x $s\, x = v$$x$$v$

L'axiome qui se déroule

nous dit simplement que nous déplions une boucle while dans une instruction conditionnelle, dont l'une des branches contient la boucle. Aucune variable ne changera leur valeur à cause de cela, et pour cette raison l'état ne change pas.

L'état peut changer au cours des étapes de réduction ultérieures car sur le côté droit de

le -loop est gardée (précédée) par . Le calcul de peut changer l'état de sorte que la condition puisse être évaluée à .S S B f a l s $while$$S$$S$$B$$\mathsf{false}$

L'état ne change pas lorsque l' on considère de décider d'effectuer une itération de la boucle, mais il peut changer plus tard quand nous courons le corps . Et donc, la prochaine fois que nous considérons , il peut y avoir un changement de .B S B $\sigma$$B$$S$$B$$\sigma$