Semántica del transformador de predicados

Reformulación de la lógica Floyd-Hoare

La semántica de transformadores de predicados fue introducida por Edsger Dijkstra en su artículo seminal " Ordenes guardadas, no determinación y derivación formal de programas ". Definen la semántica de un paradigma de programación imperativa asignando a cada enunciado en este lenguaje un transformador de predicados correspondiente : una función total entre dos predicados en el espacio de estados del enunciado. En este sentido, la semántica de transformadores de predicados es un tipo de semántica denotacional . En realidad, en los comandos guardados , Dijkstra utiliza solo un tipo de transformador de predicados: las conocidas precondiciones más débiles (ver más abajo).

Además, la semántica de transformadores de predicados es una reformulación de la lógica de Floyd-Hoare . Mientras que la lógica de Hoare se presenta como un sistema deductivo , la semántica de transformadores de predicados (ya sea por precondiciones más débiles o por postcondiciones más fuertes, ver más abajo) son estrategias completas para construir deducciones válidas de la lógica de Hoare. En otras palabras, proporcionan un algoritmo eficaz para reducir el problema de verificar un triple de Hoare al problema de probar una fórmula de primer orden . Técnicamente, la semántica de transformadores de predicados realiza una especie de ejecución simbólica de declaraciones en predicados: la ejecución se ejecuta hacia atrás en el caso de precondiciones más débiles, o hacia adelante en el caso de postcondiciones más fuertes.

Condiciones previas más débiles

Definición

Para un enunciado S y una poscondición R , una precondición más débil es un predicado Q tal que para cualquier precondición P , si y solo si . En otras palabras, es el requisito "más flexible" o menos restrictivo necesario para garantizar que R se cumple después de S . La unicidad se deduce fácilmente de la definición: si tanto Q como Q' son precondiciones más débiles, entonces por la definición tal y tal , y por lo tanto . A menudo usamos para denotar la precondición más débil para el enunciado S con respecto a una poscondición R . ${\displaystyle \{P\}S\{R\}}$ ${\displaystyle P\Rightarrow Q}$ ${\displaystyle \{Q'\}S\{R\}}$ ${\displaystyle Q'\Rightarrow Q}$ ${\displaystyle \{Q\}S\{R\}}$ ${\displaystyle Q\Rightarrow Q'}$ ${\displaystyle Q=Q'}$ ${\displaystyle wp(S,R)}$

Convenciones

Usamos T para denotar el predicado que es verdadero en todas partes y F para denotar el que es falso en todas partes. No deberíamos confundirnos, al menos conceptualmente, con una expresión booleana definida por alguna sintaxis del lenguaje, que también podría contener verdadero y falso como escalares booleanos. Para tales escalares, necesitamos hacer una conversión de tipo de modo que tengamos T = predicado(verdadero) y F = predicado(falso). Tal promoción se lleva a cabo a menudo de manera casual, por lo que la gente tiende a tomar T como verdadero y F como falso.

Saltar

Abortar

Asignación

A continuación, damos dos condiciones previas más débiles equivalentes para la declaración de asignación. En estas fórmulas, es una copia de R donde las ocurrencias libres de x se reemplazan por E . Por lo tanto, aquí, la expresión E se convierte implícitamente en un término válido de la lógica subyacente: es, por lo tanto, una expresión pura , totalmente definida, terminante y sin efectos secundarios. ${\displaystyle R[x\leftarrow E]}$

• versión 1:

• versión 2:

Siempre que E esté bien definido, simplemente aplicamos la llamada regla de un punto en la versión 1. Entonces

La primera versión evita una posible duplicación de x en R , mientras que la segunda versión es más simple cuando hay como máximo una única ocurrencia de x en R. La primera versión también revela una profunda dualidad entre la precondición más débil y la poscondición más fuerte (ver más abajo).

Un ejemplo de un cálculo válido de wp (usando la versión 2) para asignaciones con una variable x de valor entero es:

${\displaystyle {\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\&\Leftrightarrow &x>15\end{array}}}$

Esto significa que para que la poscondición x > 10 sea verdadera después de la asignación, la precondición x > 15 debe ser verdadera antes de la asignación. Esta es también la "precondición más débil", ya que es la restricción "más débil" sobre el valor de x que hace que x > 10 sea verdadero después de la asignación.

Secuencia

Por ejemplo,

${\displaystyle {\begin{array}{rcl}wp(x:=x-5;x:=x*2\ ,\ x>20)&=&wp(x:=x-5,wp(x:=x*2,x>20))\\&=&wp(x:=x-5,x*2>20)\\&=&(x-5)*2>20\\&=&x>15\end{array}}}$

Condicional

A modo de ejemplo:

${\displaystyle {\begin{array}{rcl}wp({\texttt {if}}\ x<y\ {\texttt {then}}\ x:=y\ {\texttt {else}}\;\;{\texttt {skip}}\;\;{\texttt {end}},\ x\geq y)&=&(x<y\Rightarrow wp(x:=y,x\geq y))\ \wedge \ (\neg (x<y)\Rightarrow wp({\texttt {skip}},x\geq y))\\&=&(x<y\Rightarrow y\geq y)\ \wedge \ (\neg (x<y)\Rightarrow x\geq y)\\&\Leftrightarrow &{\texttt {true}}\end{array}}}$

Bucle While

Corrección parcial

Ignorando la terminación por un momento, podemos definir la regla para la precondición liberal más débil , denotada wlp , usando un predicado INV , llamado Loop INV ariant , típicamente suministrado por el programador:

Corrección total

Para demostrar que esto es totalmente correcto, también tenemos que demostrar que el bucle termina. Para ello, definimos una relación bien fundada en el espacio de estados denotada como ( wfs , <) y definimos una función variante vf , de modo que tengamos:

De manera informal, en la conjunción anterior de tres fórmulas:

• el primero significa que la variante debe ser parte de la relación bien fundada antes de entrar al bucle;
• el segundo significa que el cuerpo del bucle (es decir, la declaración S ) debe preservar la invariante y reducir la variante;
• El último significa que la postcondición del bucle R debe establecerse cuando el bucle termina.

Sin embargo, la conjunción de esos tres no es una condición necesaria. Exactamente, tenemos

Comandos de vigilancia no deterministas

En realidad, el lenguaje de órdenes vigiladas de Dijkstra (GCL) es una extensión del lenguaje imperativo simple dado hasta aquí con enunciados no deterministas. De hecho, el GCL pretende ser una notación formal para definir algoritmos. Los enunciados no deterministas representan elecciones que quedan en manos de la implementación real (en un lenguaje de programación eficaz): las propiedades probadas en enunciados no deterministas están aseguradas para todas las posibles elecciones de implementación. En otras palabras, las precondiciones más débiles de los enunciados no deterministas aseguran

• que existe una ejecución que termina (por ejemplo, existe una implementación),
• y, que el estado final de toda ejecución que termina satisface la condición posterior.

Tenga en cuenta que las definiciones de la condición previa más débil dadas anteriormente (en particular para el bucle while ) preservan esta propiedad.

Selección

La selección es una generalización de la declaración if :

^{[ cita requerida ]}

Aquí, cuando dos guardias y son simultáneamente verdaderos, entonces la ejecución de esta declaración puede ejecutar cualquiera de las declaraciones asociadas o . ${\displaystyle E_{i}}$ ${\displaystyle E_{j}}$ ${\displaystyle S_{i}}$ ${\displaystyle S_{j}}$

Repetición

La repetición es una generalización de la declaración while de manera similar.

Declaración de especificaciones

El cálculo de refinamiento extiende GCL con la noción de enunciado de especificación . Sintácticamente, preferimos escribir un enunciado de especificación como

  ${\displaystyle x:l[pre,post]}$

que especifica un cálculo que comienza en un estado que satisface pre y se garantiza que terminará en un estado que satisface post cambiando solo x . Llamamos constante lógica a una constante empleada para ayudar en una especificación. Por ejemplo, podemos especificar un cálculo que incremente x en 1 como ${\displaystyle l}$

  ${\displaystyle x:l[x=l,x=l+1]}$

Otro ejemplo es el cálculo de la raíz cuadrada de un número entero.

  ${\displaystyle x:l[x=l^{2},x=l]}$

La declaración de especificación parece una primitiva en el sentido de que no contiene otras declaraciones. Sin embargo, es muy expresiva, ya que pre y post son predicados arbitrarios. Su condición previa más débil es la siguiente:

Combina la idea sintáctica de Morgan con la idea de nitidez de Bijlsma, Matthews y Wiltink. ^[1] La ventaja de esto es su capacidad de definir wp de goto L y otras declaraciones de salto. ^[2]

Ir a la declaración

La formalización de sentencias de salto como goto L es un proceso muy largo y accidentado. Una creencia común parece indicar que la sentencia goto solo podría argumentarse de manera operacional. Esto probablemente se deba a que no se reconoce que goto L es realmente milagroso (es decir, no estricto) y no sigue la Ley de los Milagros Excluidos acuñada por Dijkstra, tal como se define en sí misma. Pero disfruta de una visión operacional extremadamente simple desde la perspectiva de la condición previa más débil, lo cual fue inesperado. Definimos

Para goto L la ejecución transfiere el control a la etiqueta L en la que la precondición más débil tiene que cumplirse. La forma en que se hace referencia a wpL en la regla no debe tomarse como una gran sorpresa. Es solo ⁠ ⁠ para algún Q calculado hasta ese punto. Esto es como cualquier regla wp, que usa declaraciones constituyentes para dar definiciones de wp, aunque goto L parece un primitivo. La regla no requiere la unicidad de las ubicaciones donde wpL se cumple dentro de un programa, por lo que teóricamente permite que la misma etiqueta aparezca en múltiples ubicaciones siempre que la precondición más débil en cada ubicación sea la misma wpL. La declaración goto puede saltar a cualquiera de esas ubicaciones. Esto realmente justifica que podríamos colocar las mismas etiquetas en la misma ubicación varias veces, como ⁠ ⁠ , que es lo mismo que ⁠ ⁠ . Además, no implica ninguna regla de alcance, lo que permite un salto al cuerpo de un bucle, por ejemplo. Calculemos wp del siguiente programa S, que tiene un salto al cuerpo del bucle. ${\displaystyle wp(L:S,Q)}$ ${\displaystyle S(L:L:S1)}$ ${\displaystyle S(L:S1)}$

 wp(hacer x > 0 → L: x := x-1 od; si x < 0 → x := -x; ir a L ⫿ x ≥ 0 → omitir fi, publicar) = { reglas de composición secuencial y alternancia } wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; ir a L, publicar)) ∨ (x ≥ 0 ∧ publicar) = {composición secuencial, goto, reglas de asignación} wp(haz x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ publicación) = { regla de repetición } La solución más fuerte de Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ publicación ]  = { regla de asignación, encontrada wpL = Z(x ← x-1) } La solución más fuerte de Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ publicación] = { sustitución } La solución más fuerte de Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ publicación ] = { resolver la ecuación por aproximación } publicación(x ← 0)

Por lo tanto,

wp(S, publicación) = publicación(x ← 0).

Otros transformadores de predicados

La condición liberal más débil

Una variante importante de la precondición más débil es la precondición liberal más débil , que produce la condición más débil bajo la cual S no termina o establece R. Por lo tanto, se diferencia de wp en que no garantiza la terminación. Por lo tanto, corresponde a la lógica de Hoare en corrección parcial: para el lenguaje de enunciados dado anteriormente, wlp difiere de wp solo en while-loop , en que no requiere una variante (ver arriba). ${\displaystyle wlp(S,R)}$

Postcondición más fuerte

Dado S una declaración y R una precondición (un predicado sobre el estado inicial), entonces es su postcondición más fuerte : implica cualquier postcondición satisfecha por el estado final de cualquier ejecución de S, para cualquier estado inicial que satisfaga R. En otras palabras, un triple de Hoare es demostrable en la lógica de Hoare si y solo si se cumple el predicado siguiente: ${\displaystyle sp(S,R)}$ ${\displaystyle \{P\}S\{Q\}}$

${\displaystyle \forall x,sp(S,P)\Rightarrow Q}$

Por lo general, las poscondiciones más fuertes se utilizan con corrección parcial. Por lo tanto, tenemos la siguiente relación entre las precondiciones liberales más débiles y las poscondiciones más fuertes:

${\displaystyle (\forall x,P\Rightarrow wlp(S,Q))\ \Leftrightarrow \ (\forall x,sp(S,P)\Rightarrow Q)}$

Por ejemplo, en la tarea tenemos:

Arriba, la variable lógica y representa el valor inicial de la variable x . Por lo tanto,

${\displaystyle sp(x:=x-5,x>15)\ =\ \exists y,x=y-5\wedge y>15\ \Leftrightarrow \ x>10}$

En secuencia, parece que sp corre hacia adelante (mientras que wp corre hacia atrás):

Transformadores de predicados de victoria y pecado

Leslie Lamport ha sugerido win y sin como transformadores de predicados para la programación concurrente . ^[3]

Propiedades de los transformadores de predicados

En esta sección se presentan algunas propiedades características de los transformadores de predicados. ^[4] A continuación, S denota un transformador de predicados (una función entre dos predicados en el espacio de estados) y P un predicado. Por ejemplo, S(P) puede denotar wp(S,P) o sp(S,P) . Mantenemos x como la variable del espacio de estados.

Monótono

Los transformadores de predicado de interés ( wp , wlp y sp ) son monótonos . Un transformador de predicado S es monótono si y solo si:

${\displaystyle (\forall x:P:Q)\Rightarrow (\forall x:S(P):S(Q))}$

Esta propiedad está relacionada con la regla de consecuencia de la lógica de Hoare .

Estricto

Un transformador de predicado S es estricto si y solo si:

${\displaystyle S({\texttt {F}})\ \Leftrightarrow \ {\texttt {F}}}$

Por ejemplo, wp se hace estricto artificialmente, mientras que wlp generalmente no lo es. En particular, si la declaración S no puede terminar, entonces es satisfacible. Tenemos ${\displaystyle wlp(S,{\texttt {F}})}$

${\displaystyle wlp({\texttt {while}}\ {\texttt {true}}\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}},{\texttt {F}})\ \Leftrightarrow {\texttt {T}}}$

De hecho, T es un invariante válido de ese bucle.

Los transformadores de predicados no estrictos pero monótonos o conjuntivos se denominan milagrosos y también se pueden utilizar para definir una clase de construcciones de programación, en particular, sentencias de salto, por las que Dijkstra no se preocupaba tanto. Esas sentencias de salto incluyen goto L directo, break y continue en un bucle y sentencias de retorno en un cuerpo de procedimiento, manejo de excepciones, etc. Resulta que todas las sentencias de salto son milagros ejecutables, ^[5] es decir, se pueden implementar pero no son estrictas.

Terminando

Un transformador de predicado S está terminando si:

${\displaystyle S({\texttt {T}})\ \Leftrightarrow \ {\texttt {T}}}$

En realidad, esta terminología sólo tiene sentido para transformadores de predicados estrictos: de hecho, es la condición previa más débil que garantiza la terminación de S. ${\displaystyle wp(S,{\texttt {T}})}$

Parece que sería más apropiado llamar a esta propiedad no abortante : con total corrección, la no terminación es aborto, mientras que con corrección parcial, no lo es.

Conjuntivo

Un transformador de predicado S es conjuntivo si y solo si:

${\displaystyle S(P\wedge Q)\ \Leftrightarrow \ S(P)\wedge S(Q)}$

Este es el caso de , incluso si la declaración S no es determinista como una declaración de selección o una declaración de especificación. ${\displaystyle wp(S,.)}$

Disyuntivo

Un transformador de predicado S es disyuntivo si y solo si:

${\displaystyle S(P\vee Q)\ \Leftrightarrow \ S(P)\vee S(Q)}$

En general, este no es el caso cuando S no es determinista. De hecho, considere una declaración no determinista S que elige un booleano arbitrario. Esta declaración se da aquí como la siguiente declaración de selección : ${\displaystyle wp(S,.)}$

${\displaystyle S\ =\ {\texttt {if}}\ {\texttt {true}}\rightarrow x:=0\ [\!]\ {\texttt {true}}\rightarrow x:=1\ {\texttt {fi}}}$

Luego, se reduce a la fórmula . ${\displaystyle wp(S,R)}$ ${\displaystyle R[x\leftarrow 0]\wedge R[x\leftarrow 1]}$

Por lo tanto, se reduce a la tautología ${\displaystyle wp(S,\ x=0\vee x=1)}$ ${\displaystyle (0=0\vee 0=1)\wedge (1=0\vee 1=1)}$

Considerando que la fórmula se reduce a la proposición errónea . ${\displaystyle wp(S,x=0)\vee wp(S,x=1)}$ ${\displaystyle (0=0\wedge 1=0)\vee (1=0\wedge 1=1)}$

Aplicaciones

• Los cálculos de las precondiciones más débiles se utilizan en gran medida para verificar estáticamente las afirmaciones en programas que utilizan un demostrador de teoremas (como los solucionadores SMT o los asistentes de prueba ): consulte Frama-C o ESC/Java2 .
• A diferencia de muchos otros formalismos semánticos, la semántica de transformadores de predicados no fue diseñada como una investigación sobre los fundamentos de la computación. Más bien, se pretendía proporcionar a los programadores una metodología para desarrollar sus programas como "correctos por construcción" en un "estilo de cálculo". Este estilo "de arriba hacia abajo" fue defendido por Dijkstra ^[6] y N. Wirth ^[7]. Ha sido formalizado aún más por R.-J. Back y otros en el cálculo de refinamiento . Algunas herramientas como B-Method ahora proporcionan razonamiento automatizado para promover esta metodología.
• En la metateoría de la lógica de Hoare , las precondiciones más débiles aparecen como una noción clave en la prueba de completitud relativa . ^[8]

Más allá de los transformadores de predicados

Precondiciones más débiles y poscondiciones más fuertes de expresiones imperativas

En la semántica de los transformadores de predicados, las expresiones están restringidas a términos de la lógica (ver arriba). Sin embargo, esta restricción parece demasiado fuerte para la mayoría de los lenguajes de programación existentes, donde las expresiones pueden tener efectos secundarios (llamada a una función que tiene un efecto secundario), pueden no terminar o abortar (como la división por cero ). Hay muchas propuestas para extender las precondiciones más débiles o las poscondiciones más fuertes para lenguajes de expresión imperativos y en particular para mónadas .

Entre ellos, la teoría de tipos de Hoare combina la lógica de Hoare para un lenguaje similar a Haskell , la lógica de separación y la teoría de tipos . ^[9] Este sistema está implementado actualmente como una biblioteca Coq llamada Ynot . ^[10] En este lenguaje, la evaluación de expresiones corresponde a los cálculos de las postcondiciones más fuertes .

Transformadores de predicados probabilísticos

Los transformadores de predicados probabilísticos son una extensión de los transformadores de predicados para programas probabilísticos . De hecho, estos programas tienen muchas aplicaciones en criptografía (ocultación de información mediante ruido aleatorio) y sistemas distribuidos (ruptura de simetría). ^[11]

Véase también

• Semántica axiomática : incluye semántica de transformador de predicados
• Lógica dinámica : donde los transformadores de predicados aparecen como modalidades
• Semántica formal de los lenguajes de programación : una visión general

Notas

1. Chen, Wei y Udding, Jan Tijmen, "La declaración de especificación refinada" WUCS-89-37 (1989). https://openscholarship.wustl.edu/cse_research/749
2. Chen, Wei, "Una caracterización de las declaraciones de salto", Simposio internacional sobre aspectos teóricos de la ingeniería de software (TASE) de 2021, 2021, págs. 15-22. doi: 10.1109/TASE52547.2021.00019.
3. Lamport, Leslie (julio de 1990). "win and sin: Predicate Transformers for Concurrency" (ganar y pecar: transformadores de predicados para concurrencia). ACM Trans. Program. Lang. Syst. 12 (3): 396–428. CiteSeerX  10.1.1.33.90 . doi :10.1145/78969.78970. S2CID  209901.
4. Volver, Ralph-Johan; Wright, Joakim (2012) [1978]. Cálculo de refinamiento: una introducción sistemática. Textos en informática. Springer. ISBN 978-1-4612-1674-2.
5. Chen, Wei, "Las declaraciones de salida son milagros ejecutables" WUCS-91-53 (1991). https://openscholarship.wustl.edu/cse_research/671
6. Dijkstra, Edsger W. (1968). "Un enfoque constructivo al problema de la corrección de programas". BIT Numerical Mathematics . 8 (3): 174–186. doi :10.1007/bf01933419. S2CID  62224342.
7. Wirth, N. (abril de 1971). "Desarrollo de programas mediante refinamiento paso a paso" (PDF) . Comm. ACM . 14 (4): 221–7. doi :10.1145/362575.362577. hdl : 20.500.11850/80846 . S2CID  13214445.
8. Tutorial sobre lógica Hoare: una biblioteca Coq que ofrece una prueba simple pero formal de que la lógica Hoare es sólida y completa con respecto a una semántica operacional .
9. Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars (septiembre de 2008). "Teoría de tipos de Hoare, polimorfismo y separación" (PDF) . Journal of Functional Programming . 18 (5–6): 865–911. doi :10.1017/S0956796808006953. S2CID  6956622.
10. Ynot es una biblioteca Coq que implementa la teoría de tipos de Hoare.
11. Morgan, Carroll; McIver, Annabelle ; Seidel, Karen (mayo de 1996). "Transformadores de predicados probabilísticos" (PDF) . ACM Trans. Program. Lang. Syst . 18 (3): 325–353. CiteSeerX 10.1.1.41.9219 . doi :10.1145/229542.229547. S2CID  5812195. 

Referencias

• de Bakker, JW (1980). Teoría matemática de la corrección de programas . Prentice-Hall. ISBN 978-0-13-562132-5.
• Bonsangue, Marcello M.; Kok, Joost N. (noviembre de 1994). "El cálculo de precondiciones más débiles: recursión y dualidad". Aspectos formales de la informática . 6 (6): 788–800. CiteSeerX  10.1.1.27.8491 . doi :10.1007/BF01213603. S2CID  40323488.
• Dijkstra, Edsger W. (agosto de 1975). "Órdenes protegidas, no determinación y derivación formal de programas". Comm. ACM . 18 (8): 453–7. doi : 10.1145/360933.360975 . S2CID  1679242.
• Dijkstra, Edsger W. (1976). Una disciplina de programación . Prentice Hall. ISBN 978-0-613-92411-5.— Una introducción sistemática a una versión del lenguaje de comandos protegidos con muchos ejemplos resueltos
• Dijkstra, Edsger W.; Scholten, Carel S. (1990). Cálculo de predicados y semántica de programas. Textos y monografías en informática. Springer-Verlag. ISBN 978-0-387-96957-2.— Un tratamiento más abstracto, formal y definitivo
• Gries, David (1981). La ciencia de la programación . Springer-Verlag. ISBN 978-0-387-96480-5.