La lógica de Hoare

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 15 de junio de 2021; las comprobaciones requieren 2 ediciones .

La lógica de Hoare ( eng. Lógica de Hoare , también lógica de Floyd-Hoare , o reglas de Hoare ) es un sistema formal con un conjunto de reglas lógicas diseñadas para probar la corrección programas de computadora Fue propuesto en 1969 por el informático y lógico matemático inglés Hoare , desarrollado posteriormente por el propio Hoare y otros investigadores. [1] La idea original fue propuesta por Floyd , quien publicó un sistema similar [2 ] aplicado a diagramas de flujo .

Trillizos Hoare

La característica principal de la lógica de Hoare es el triple de Hoare . El triple describe cómo la ejecución de una pieza de código cambia el estado del cálculo. El triple de Hoare tiene la siguiente forma:

\{P\}\;C\;\{Q\}

donde P y Q son afirmaciones y C es un comando . _ _ P se llama condición previa ( antecedente ) y Q se llama condición posterior ( consecuente ). Si la condición previa es verdadera, el comando hace que la condición posterior sea verdadera. Los enunciados son fórmulas de la lógica de predicados .

La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo simple . Además de estas construcciones descritas en el trabajo original de Hoare, Hoare y otros desarrollaron reglas para otras construcciones: ejecución concurrente , llamada a procedimiento , salto y puntero .

La idea principal de Hoare es dar a cada construcción de un lenguaje imperativo una condición previa y una condición posterior , escritas como una fórmula lógica. Por lo tanto, aparece un triple en el nombre : precondición , construcción del lenguaje, poscondición .

Está claro que para un operador vacío, las condiciones previas y posteriores coinciden.
Para un operador de asignación en una postcondición , además de la precondición , se debe tener en cuenta el hecho de que el valor de la variable ha cambiado.
Para una declaración compuesta (en Python es sangría, en C es {} ) tenemos una cadena de condiciones previas y posteriores . Como resultado, la primera condición previa y la última condición posterior se pueden dejar para la declaración compuesta .
La regla de inferencia dice que podemos fortalecer la condición previa y debilitar la condición posterior si lo necesitamos. No tiene sentido mantener todo el programa como una declaración que no ayude a resolver el problema.
Declaración de rama o simplemente si . Se puede dividir condicionalmente en dos ramas: entonces y más . Si añadimos la verdad de la condición lógica a la precondición (lo que está debajo del if ), entonces, después de la ejecución de la rama entonces , debería seguir la poscondición . De manera similar, si agregamos la negación de una condición lógica a la condición previa (lo que está debajo del if ), luego de la ejecución de la rama else , la condición posterior debería seguir
operador de bucle Este es el más no trivial y complejo, ya que el ciclo puede ejecutarse muchas veces y ni siquiera terminar. Para resolver el problema de la posible repetición repetida del cuerpo del bucle, se introduce la invariante del bucle . Un bucle invariante es algo que es verdadero antes de que se ejecute, es verdadero después de cada ejecución del cuerpo del bucle y, por lo tanto, es verdadero después del final del bucle. La precondición para una declaración de bucle es simplemente su bucle invariable . Si la condición de continuación del bucle es verdadera (lo que está debajo de while ), luego de la ejecución del cuerpo del bucle, debería seguir la verdad del invariante del bucle . Como resultado, después del final del ciclo, tenemos como poscondición la verdad del invariante del ciclo y la negación de la condición para continuar el ciclo.
Operador de bucle con total corrección. Para hacer esto, se agrega una función de limitación al párrafo anterior, con la ayuda de la cual es fácil demostrar que el bucle se ejecutará un número limitado de veces. Se le imponen condiciones de que siempre es >=0, disminuye estrictamente después de cada ejecución del cuerpo del ciclo y exactamente = 0 cuando finaliza el ciclo.

Un programa que funcione bien se puede escribir de muchas maneras y, en muchos casos, será eficiente. Esta ambigüedad complica la programación. Para hacer esto, introduce un estilo. Pero esto no es suficiente. Para muchos programas (por ejemplo, aquellos conectados indirectamente con la vida humana), también es necesario probar su corrección. Resultó que la prueba de corrección hace que el programa sea más caro en un orden de magnitud (alrededor de 10 veces).

Corrección parcial y total

En la lógica estándar de Hoare, solo se puede probar la corrección parcial, ya que la terminación del programa debe probarse por separado. Además, la regla de no usar partes de programa redundantes no puede expresarse en la lógica de Hoare. La comprensión "intuitiva" del triple de Hoare se puede expresar de la siguiente manera: si P ocurre antes de que se complete C , entonces ocurre Q o C nunca terminará. De hecho, si C no termina, no hay después, por lo que Q puede ser cualquier enunciado. Además, podemos elegir que Q sea falso para mostrar que C nunca terminará.

La corrección completa también se puede probar usando una versión extendida de la regla para la declaración Mientras .

Reglas

El axioma del operador vacío

La regla para una declaración vacía establece que la declaración de salto ( sentencia vacía ) no cambia el estado del programa, por lo que una declaración que era verdadera antes de saltar sigue siendo verdadera después de que se ejecuta.

{\displaystyle {\frac {}{\{P\}\ {\textbf {saltar}}\ \{P\))))

El axioma del operador de asignación

El axioma del operador de asignación establece que después de una asignación, el valor de cualquier predicado con respecto al lado derecho de la asignación no cambia con el reemplazo del lado derecho por el lado izquierdo:

{\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\))))

Aquí se entiende la expresión P en la que todas las apariciones de la variable libre x se sustituyen por la expresión E . $P[E/x]$

El significado del axioma de la asignación es que la verdad es equivalente después de que se ha realizado la asignación. Así, si era cierto antes de la cesión, según el axioma de la cesión será cierto después de la cesión. Por el contrario, si era igual a "falso" antes de la declaración de asignación, debería ser igual a "falso" después. $\{P[E/x]\}$ $\{PAGS\}$ $\{P[E/x]\}$ $\{PAGS\}$ $\{P[E/x]\}$ $\{PAGS\}$

Ejemplos de triples válidos:

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\))$
${\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\))$

El axioma de asignación en la formulación de Hoare no se aplica cuando más de un identificador se refiere al mismo valor. Por ejemplo,

\{ y = 3\} \ x := 2\ \{y = 3 \}

es falso si x e y se refieren a la misma variable, ya que ninguna condición previa puede asegurar que y sea 3 después de que a x se le haya asignado 2.

Regla de composición

La regla de composición de Hoare se aplica a la ejecución secuencial de los programas S y T , donde S se ejecuta antes que T , que se escribe S;T .

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{ R\}}}

Por ejemplo, considere dos instancias del axioma de asignación:

\{ x + 1 = 43\} \ y := x + 1\ \{y =43 \}

\{ y = 43\} \ z := y\ \{z = 43 \}

De acuerdo con la regla de composición, obtenemos:

\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}

Regla del operador condicional

{\frac {\{B\cuña P\}\ S\ \{Q\}\ ,\ \{\neg B\cuña P\}\ T\ \{Q\}}{\{P\ }\ {\textbf {si}}\ B\ {\textbf {entonces}}\ S\ {\textbf {si no}}\ T\ {\textbf {endif}}\ \{Q\}}}

Regla de inferencia

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime )){\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}

Regla de declaración de bucle

{\frac {\{P\cuña B\}\ S\ \{P\}}{\{P\}\ {\textbf {mientras}}\ B\ {\textbf {hacer}}\ S \ {\textbf {hecho}}\ \{\neg B\cuña P\}}}

Aquí P es un ciclo invariante .

Regla de declaración de ciclo con total corrección

{\frac {<\;{\text{está bien fundada,}}\;[P\cuña B\cuña t=z]\ S\ [P\cuña t<z]}{[P] \ {\textbf {mientras}}\ B\ {\textbf {hacer}}\ S\ {\textbf {hecho}}\ [\neg B\cuña P]}}

En esta regla, además de preservar la invariancia del bucle, la terminación del bucle se prueba mediante un término llamado variable del bucle (aquí t ), cuyo valor se reduce estrictamente de acuerdo con la relación bien fundada " < " con cada iteración. En este caso, la condición B debe implicar que t no es el elemento mínimo de su dominio, de lo contrario la premisa de esta regla será falsa. Debido a que la relación " < " está completamente bien fundamentada, cada paso del ciclo se define mediante miembros decrecientes de un conjunto ordenado linealmente finito .

La notación de esta regla usa corchetes, no llaves, para indicar la corrección completa de la regla. (Esta es una forma de denotar corrección completa).

Ejemplos

Ejemplo 1

{\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\))

— basado en el axioma de asignación.

Como , en base a la regla de inferencia, obtenemos:

( x + 1 = 43 \ flecha izquierda derecha x = 42 )

\{x=42\}\ y:=x+1\ \{y=43\land x=42\}

Ejemplo 2

{\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\))

— basado en el axioma de asignación.

Si x y N son enteros, entonces , y basándonos en la regla de inferencia, obtenemos:

(x < N) \implica (x+1 \leq N)

\{x<N\}\ x:=x+1\ \{x\leq N\}

Véase también

Enlaces

↑ COCHE Hoare . " Una base axiomática para la programación de computadoras . Archivado el 17 de julio de 2011 en Wayback Machine ". Comunicaciones de la ACM , 12(10):576-580,583 octubre 1969. doi : 10.1145/363235.363259
↑ RW Floyd . « Asignación de palabras a los programas. Archivado desde el original el 9 de diciembre de 2008. (enlace descendente desde 13-05-2013 [3444 días] - historia ) » (enlace descargado) Actas de los simposios de la American Mathematical Society sobre matemáticas aplicadas. vol. 19, págs. 19-31. 1967.

Literatura

Guts AK Lógica matemática y teoría de algoritmos. - M. : Casa del libro "LIBROKOM", 2009. - 117 p. — ISBN 9785397000567 .
https://web.archive.org/web/20110123200456/http://djvu-student.narod.ru/02-matematicheskaya-logika/metodichka/metoda_matlogika_i_teor_algoritm_g6.html

En catálogos bibliográficos	TIERRA : 4343105-7