¿Por qué el estado permanece sin cambios en la semántica operacional de pequeños pasos de un ciclo while?

9

Por lo general, veo que en la representación semántica operacional estructural para el ciclo while, el estado del programa no cambia:

(whileBdoS,σ)(ifBthenS;(whileBdoS)elseSKIP,σ)

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á.B

¿Alguien puede explicar por qué el estado no cambia en esta regla?

El marce
fuente
Tenga en cuenta que esto solo es correcto si podemos suponer que no tiene efectos secundarios. Esto no es cierto en la mayoría de los lenguajes de programación. si
Raphael

Respuestas:

10

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

s:VarZ

que registra los valores de las variables. Entonces si , luego variable xsx=vx 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

whilebdoS,sifbthenS;whilebdoSelse skip,s

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.

Hans Hüttel
fuente
10

El estado puede cambiar en los pasos de reducción posteriores porque en el lado derecho de

while B do S,σif B then (S; while B do S) else skip,σ

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 .whileSSBfalse

Martin Berger
fuente
Entonces, ¿esto significa que el cambio de estado debería expresarse en otras reglas a las cuales S podría reducirse potencialmente en un programa concreto?
El Marce
@ElMarce Sí. Sugiero pasar por un ejemplo simple, por ejemplo y vea cómo funciona esto. x:=2; while x>0 do x:=x1
Martin Berger
9

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 σ .σBSBσ

Andrej Bauer
fuente
Esta explicación, si bien es esencialmente correcta, no se refiere a qué estados son (es decir, una función que nos dice los valores de varialbes) y qué significa un cambio de estado (es decir, que el valor de al menos una variable cambia).
Hans Hüttel
De hecho, es irrelevante qué son los estados o cómo se implementan para los fines de mi respuesta. La explicación se mantiene independientemente. Y, además, en realidad es un error decir que "los estados son realmente funciones" porque solo existe una forma de modelarlos matemáticamente. Hay otros modelos posibles. Y no confundamos los modelos matemáticos con el funcionamiento del hardware.
Andrej Bauer
Pero la pregunta se refiere a una semántica operativa específica de pequeños pasos, para la cual la noción de estado está bien definida.
Hans Hüttel
Nunca dije que no fuera así. Solo digo que su comentario es innecesario, porque mi explicación es válida sin una mención explícita de cómo se modela el estado. Quizás detectó que el OP no sabía que el estado era un mapa de variables a valores. Bien por ti, tu respuesta fue aceptada, y yo no. Felicidades. Por qué ahora me estás obligando a responder a tu modo de respuesta está más allá de mi comprensión. ¿Por qué precisamente sientes la necesidad de hacer que mi respuesta sea como la tuya? Mi respuesta tiene sentido sin los comentarios que crees que son necesarios. Tal vez alguien vendrá buscando mi respuesta algún día.
Andrej Bauer