La semántica del transformador de predicados fue introducida por Edsger Dijkstra en su artículo seminal " Comandos guardados, 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 predicado correspondiente : una función total entre dos predicados en el espacio de estados del enunciado. En este sentido, la semántica del transformador de predicados es una especie de semántica denotacional . En realidad, en los comandos protegidos , Dijkstra utiliza solo un tipo de transformador de predicado: el conocidocondiciones previas más débiles (ver más abajo).
Además, la semántica del transformador predicado 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 del transformador de predicados (ya sea por las precondiciones más débiles o por las poscondiciones 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 del transformador 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 las precondiciones más débiles, o avanza en el caso de las poscondiciones 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 , si y solo si . En otras palabras, es el "más flojo" o menos restrictiva requisito necesario para garantizar que R tiene después de S . La unicidad se deriva fácilmente de la definición: si tanto Q como Q ' son condiciones previas más débiles, entonces según la definición entonces y entonces , y por lo tanto . Denotamos porla precondición más débil para la declaración S y postcondition R .
Saltar
Abortar
Asignación
Damos a continuación 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 apariciones libres de x se sustituyen por correo . Por lo tanto, aquí, la expresión E está implícitamente coaccionada en un término válido de la lógica subyacente: es, por tanto, una expresión pura , totalmente definida, terminante y sin efectos secundarios.
- versión 1:
donde y es una variable nueva (que representa el valor final de la variable x ) |
- versión 2:
La primera versión evita una posible duplicación de E en R , mientras que la segunda versión es más simple cuando hay como máximo una sola aparición de x en R . La primera versión también revela una profunda dualidad entre la condición previa más débil y la condición posterior 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 la variable de valor entero x es:
Esto significa que para que la condición posterior x> 10 sea verdadera después de la asignación, la condición previa x> 15 debe ser verdadera antes de la asignación. Esta es también la "condición previa más débil", ya que es la restricción "más débil" sobre el valor de x lo que hace que x> 10 sea verdadero después de la asignación.
Secuencia
Por ejemplo,
Condicional
Como ejemplo:
Mientras bucle
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 I , llamado invariante de bucle , generalmente proporcionado por el programador:
Esto simplemente establece que (1) el invariante debe mantenerse al comienzo del ciclo; (2) además, para cualquier estado inicial y , el invariante y la guarda tomados en conjunto deben ser lo suficientemente fuertes como para establecer la condición previa más débil necesaria para que el cuerpo del bucle pueda restablecer el invariante; (3) finalmente, si y cuando el bucle termina en un estado dado y , el hecho de que la protección del bucle sea falsa junto con el invariante debería poder establecer la poscondición requerida.
Corrección total
Para mostrar la corrección total, también tenemos que mostrar que el ciclo termina. Para esto definimos una relación bien fundada en el espacio de estados denotado "<" y llamado variante de bucle . Por tanto, tenemos:
donde y es una nueva tupla de variables |
De manera informal, en la conjunción anterior de tres fórmulas:
- el primer medio de uno que invariante I debe sostener inicialmente;
- el segundo significa que el cuerpo del bucle (por ejemplo, la declaración S ) debe preservar el invariante y disminuir la variante: aquí, la variable y representa el estado inicial de la ejecución del cuerpo;
- el último significa que R debe establecerse al final del ciclo: aquí, la variable y representa el estado final del ciclo.
En la semántica de los transformadores predicados, invariante y variante se construyen imitando el teorema de punto fijo de Kleene . A continuación, esta construcción se esboza en teoría de conjuntos . Suponemos que U es un conjunto que denota el espacio de estados. Primero, definimos una familia de subconjuntos de U denotadospor inducción sobre el número natural k . Informalmenterepresenta el conjunto de estados iniciales que hacen que R se satisfaga después de menos de k iteraciones del ciclo:
Entonces, definimos:
- invariante I como predicado.
- variante como la proposición
Con estas definiciones, se reduce a fórmula .
Sin embargo, en la práctica, los probadores de teoremas no pueden manejar eficientemente una construcción tan abstracta. Por lo tanto, los usuarios humanos proporcionan las invariantes y variantes de bucle, o se infieren mediante algún procedimiento de interpretación abstracta .
Comandos protegidos no deterministas
En realidad, Guarded Command Language (GCL) de Dijkstra es una extensión del lenguaje imperativo simple dado hasta aquí con declaraciones no deterministas. De hecho, GCL pretende ser una notación formal para definir algoritmos. Las declaraciones no deterministas representan opciones dejadas a la implementación real (en un lenguaje de programación efectivo): las propiedades probadas en declaraciones no deterministas están aseguradas para todas las opciones posibles de implementación. En otras palabras, las precondiciones más débiles de las declaraciones no deterministas aseguran
- que existe una ejecución de terminación (por ejemplo, existe una implementación),
- y que el estado final de toda ejecución de terminación satisface la condición posterior.
Observe que las definiciones de precondición más débil dadas anteriormente (en particular para while-loop ) conservan esta propiedad.
Selección
La selección es una generalización de la declaración if :
Aquí, cuando dos guardias y son simultáneamente verdaderas, entonces la ejecución de esta declaración puede ejecutar cualquiera de las declaraciones asociadas o .
Repetición
La repetición es una generalización de la declaración while de manera similar.
Declaración de especificación (o condición previa más débil de la llamada a procedimiento)
El cálculo de refinamiento extiende los enunciados no deterministas con la noción de enunciado de especificación . De manera informal, esta declaración representa una llamada a procedimiento en caja negra, donde se desconoce el cuerpo del procedimiento. Normalmente, utilizando una sintaxis cercana al método B , se escribe una declaración de especificación
- @
dónde
- x es la variable global modificada por la declaración,
- P es un predicado que representa la condición previa,
- y es una nueva variable lógica, ligada a Q , que representa el nuevo valor de x elegido de forma no determinista por la declaración,
- Q es un predicado que representa una poscondición, o más exactamente una guarda: en Q , la variable x representa el estado inicial e y denota el estado final.
La condición previa más débil de la declaración de especificación viene dada por:
@ donde z es un nombre nuevo |
Además, un enunciado S implementa dicho enunciado de especificación si y solo si el siguiente predicado es una tautología:
dónde es un nombre nuevo (que denota el estado inicial) |
De hecho, en tal caso, la siguiente propiedad está asegurada para todas las poscondiciones R (esto es una consecuencia directa de la monotonicidad de wp , ver más abajo):
- @
De manera informal, esta última propiedad asegura que cualquier prueba sobre alguna declaración que involucre una especificación siga siendo válida al reemplazar esta especificación por cualquiera de sus implementaciones.
Otros transformadores de predicado
Precondición liberal más débil
Una variante importante de la condición previa más débil es la condición previa liberal más débil. , Que produce la condición más débil en las que S sea no termina o establece R . Por tanto, se diferencia de wp en que no garantiza la rescisión. Por lo tanto, corresponde a la lógica de Hoare en una corrección parcial: para el lenguaje de enunciados dado anteriormente, wlp difiere con wp solo en while-loop , al no requerir una variante (ver arriba).
Postcondición más fuerte
Dado S un enunciado y R una precondición (un predicado del estado inicial), entonceses su poscondición más fuerte : implica cualquier poscondició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 el predicado a continuación se cumple:
Por lo general, las condiciones posteriores 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:
Por ejemplo, en la asignación tenemos:
donde y es fresco |
Arriba, la variable lógica y representa el valor inicial de la variable x . Por eso,
En secuencia, parece que sp corre hacia adelante (mientras que wp corre hacia atrás):
Transformadores de predicado de ganar y pecar
Leslie Lamport ha sugerido win y sin como transformadores predicados para la programación concurrente . [1]
Propiedades de los transformadores predicados
Esta sección presenta algunas propiedades características de los transformadores de predicado. [2] A continuación, T denota un predicado transformador (una función entre dos predicados en el espacio de estados) y P un predicado. Por ejemplo, T (P) puede denotar wp (S, P) o sp (S, P) . Mantenemos x como la variable del espacio de estados.
Monotónico
Los transformadores de predicado de interés ( wp , wlp y sp ) son monótonos . Un transformador de predicado T es monótono si y solo si:
Esta propiedad está relacionada con la regla de consecuencia de la lógica de Hoare .
Estricto
Un transformador de predicado T es estricto si:
Por ejemplo, wp es estricto, mientras que wlp generalmente no lo es. En particular, si la declaración S no puede terminar, entonceses satisfactorio. Tenemos
De hecho, verdadero es un invariante válido de ese bucle.
Terminando
Un transformador de predicado T está terminando sif:
En realidad, esta terminología solo tiene sentido para los transformadores de predicados estrictos: de hecho, es el más débil-precondición asegurar la terminación de S .
Parece que llamar a esta propiedad no abortiva sería más apropiado: en la corrección total, la no terminación es aborto, mientras que en la corrección parcial no lo es.
Conjuntivo
Un predicado transformador T es conjuntivo sif:
Este es el caso de , incluso si el enunciado S no es determinista como enunciado de selección o enunciado de especificación.
Disyuntivo
Un transformador de predicado T es disyuntivo sif:
Este no es generalmente el caso de cuando S no es determinista. De hecho, considere un enunciado no determinista S eligiendo un booleano arbitrario. Esta declaración se da aquí como la siguiente declaración de selección :
Luego, se reduce a la fórmula .
Por eso, se reduce a la tautología
Considerando que, la fórmula se reduce a la proposición equivocada .
El mismo contraejemplo se puede reproducir usando una declaración de especificación (ver arriba) en su lugar:
- @
Aplicaciones
- Los cálculos de las condiciones previas más débiles se utilizan en gran medida para comprobar estáticamente las afirmaciones en los programas que utilizan un comprobador de teoremas (como SMT-solvers o asistentes de prueba ): consulte Frama-C o ESC / Java2 .
- A diferencia de muchos otros formalismos semánticos, la semántica del transformador predicado 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 [3] y N. Wirth . [4] Ha sido formalizado aún más por R.-J. Back y otros en el cálculo de refinamiento . Algunas herramientas como el Método B ahora proporcionan un 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 la completitud relativa . [5]
Más allá de los transformadores predicados
Condiciones previas más débiles y condiciones posteriores más fuertes de las 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 los lenguajes de expresión imperativa y, en particular, para las 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 . [6] Este sistema se implementa actualmente como una biblioteca Coq llamada Ynot . [7] En este lenguaje, la evaluación de expresiones corresponde a cálculos de postcondiciones más fuertes .
Transformadores probabilísticos de predicados
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 utilizando algún ruido aleatorio), sistemas distribuidos (ruptura de simetría). [8]
Ver también
- Semántica axiomática : incluye semántica de transformador de predicado
- Lógica dinámica : donde los transformadores de predicados aparecen como modalidades
- Semántica formal de los lenguajes de programación : una descripción general
Notas
- ^ Lamport, Leslie (julio de 1990). " ganar y pecar : transformadores de predicado para la simultaneidad" . ACM Trans. Programa. Lang. Syst. 12 (3): 396–428. CiteSeerX 10.1.1.33.90 . doi : 10.1145 / 78969.78970 . S2CID 209901 .
- ^ Atrás, Ralph-Johan; Wright, Joakim (2012) [1978]. Cálculo de refinamiento: una introducción sistemática . Textos en Informática. Saltador. ISBN 978-1-4612-1674-2.
- ^ Dijkstra, Edsger W. (1968). "Un enfoque constructivo al problema de la corrección del programa". BIT Matemáticas numéricas . 8 (3): 174–186. doi : 10.1007 / bf01933419 . S2CID 62224342 .
- ^ Wirth, N. (abril de 1971). "Programa de desarrollo por refinamiento paso a paso" (PDF) . Comm. ACM . 14 (4): 221–7. doi : 10.1145 / 362575.362577 . hdl : 20.500.11850 / 80846 . S2CID 13214445 .
- ^ Tutorial sobre la lógica de Hoare : unabiblioteca Coq , que da una prueba simple pero formal de que la lógica de Hoare es sólida y completa con respecto a una semántica operativa .
- ^ Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars (septiembre de 2008). "Teoría de tipos de Hoare, polimorfismo y separación" (PDF) . Revista de programación funcional . 18 (5–6): 865–911. doi : 10.1017 / S0956796808006953 .
- ^ No es unabiblioteca Coq que implementa la teoría de tipos de Hoare.
- ^ Morgan, Carroll; McIver, Annabelle; Seidel, Karen (mayo de 1996). "Transformadores de predicados probabilísticos" (PDF) . ACM Trans. Programa. 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 del programa . Prentice Hall. ISBN 978-0-13-562132-5.
- Bonsangue, Marcello M .; Kok, Joost N. (noviembre de 1994). "El cálculo de condiciones previas más débil: recursividad 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). "Comandos vigilados, 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 protegido 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.