Por lo general, veo que en la representación semántica operacional estructural para el ciclo while, el estado del programa no cambia:
Para mí, esto no es intuitivo, si el estado no cambia (es decir, el estado de la memoria permanece igual) entonces continuará siendo verdadero y el programa nunca terminará.
¿Alguien puede explicar por qué el estado no cambia en esta regla?
Respuestas:
En la semántica del lenguaje de programación, la noción de estado del programa no es una noción filosófica vaga, sino matemática muy precisa. UNA estado en esta semántica operacional de pequeños pasos es una función parcials
que registra los valores de las variables. Entonces si , luego variable xsx=v x tiene el valor . El estado es necesariamente una función parcial, ya que solo tiene sentido registrar los valores de las variables que realmente ocurren.v
El axioma desplegado
simplemente nos dice que desarrollamos un ciclo while en una declaración condicional, una de cuyas ramas contiene el ciclo. Ninguna variable cambiará su valor debido a esto, y por esta razón el estado no cambia.
fuente
El estado puede cambiar en los pasos de reducción posteriores porque en el lado derecho de
la -loop está vigilado (precedido) por S . El cálculo de S puede cambiar el estado para que la condición B pueda evaluarse a f a l s e .while S S B false
fuente
El estado no cambia cuando consideramos B para decidir si se debe realizar una iteración del bucle, pero se puede cambiar más tarde cuando corremos el cuerpo S . Y así, la próxima vez que consideremos B , puede haber un cambio de σ .σ B S B σ
fuente