Lógica hoare

La lógica de Hoare (también conocida como lógica de Floyd-Hoare o reglas de Hoare ) es un sistema formal con un conjunto de reglas lógicas para razonar rigurosamente sobre la corrección de los programas de computadora . Fue propuesto en 1969 por el científico informático y lógico británico Tony Hoare , y posteriormente refinado por Hoare y otros investigadores. ^[1] Las ideas originales fueron sembradas por el trabajo de Robert W. Floyd , quien había publicado un sistema similar ^[2] para diagramas de flujo .

Hoare triple

La característica central de la lógica de Hoare es el triple de Hoare . Un triple describe cómo la ejecución de un fragmento de código cambia el estado del cálculo. Un triple de Hoare es de la forma

${\displaystyle \{P\}C\{Q\}}$

dónde ${\displaystyle P}$ y ${\displaystyle Q}$son afirmaciones y${\displaystyle C}$es un comando . ^{[nota 1]} ${\displaystyle P}$se llama la condición previa y${\displaystyle Q}$la condición posterior : cuando se cumple la condición previa, la ejecución del comando establece la condición posterior. Las afirmaciones son fórmulas en lógica de predicados .

La lógica de Hoare proporciona axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo simple . Además de las reglas para el lenguaje simple en el artículo original de Hoare, desde entonces Hoare y muchos otros investigadores han desarrollado reglas para otras construcciones del lenguaje. Hay reglas para la simultaneidad , procedimientos , saltos y punteros .

Corrección parcial y total

Usando la lógica estándar de Hoare, solo se puede probar la corrección parcial , mientras que la terminación debe probarse por separado. Así, la lectura intuitiva de un triple de Hoare es: Siempre que${\displaystyle P}$ ostenta del Estado antes de la ejecución de ${\displaystyle C}$, luego ${\displaystyle Q}$ se mantendrá después, o ${\displaystyle C}$no termina. En el último caso, no hay "después", por lo que${\displaystyle Q}$puede ser cualquier declaración. De hecho, uno puede elegir${\displaystyle Q}$ ser falso para expresar eso ${\displaystyle C}$ no termina.

La corrección total también se puede demostrar con una versión extendida de la regla While. ^{[ cita requerida ]}

En su artículo de 1969, Hoare utilizó una noción más estrecha de terminación que también implicaba la ausencia de errores en tiempo de ejecución: "La falla en terminar puede deberse a un bucle infinito; o puede deberse a la violación de un límite definido por la implementación, por por ejemplo, el rango de operandos numéricos, el tamaño del almacenamiento o un límite de tiempo del sistema operativo ". ^[3]

Reglas

Esquema de axioma de declaración vacía

La regla de declaración vacía afirma que el${\displaystyle {\textbf {skip}}}$ declaración no cambia el estado del programa, por lo tanto, cualquier cosa que sea verdadera antes ${\displaystyle {\textbf {skip}}}$también es cierto después. ^{[nota 2]}

${\displaystyle {\dfrac {}{\{P\}{\textbf {skip}}\{P\}}}}$

Esquema de axioma de asignación

El axioma de asignación establece que, después de la asignación, cualquier predicado que antes era verdadero para el lado derecho de la asignación ahora es válido para la variable. Formalmente, deja${\displaystyle P}$ ser una aserción en la que la variable ${\displaystyle x}$es gratis . Luego:

${\displaystyle {\dfrac {}{\{P[E/x]\}x:=E\{P\}}}}$

dónde ${\displaystyle P[E/x]}$ denota la aserción ${\displaystyle P}$en el que cada ocurrencia libre de${\displaystyle x}$ha sido reemplazada por la expresión${\displaystyle E}$.

El esquema de axioma de asignación significa que la verdad de ${\displaystyle P[E/x]}$ es equivalente a la verdad posterior a la asignación de ${\displaystyle P}$. Así fueron${\displaystyle P[E/x]}$ verdadero antes de la asignación, por el axioma de asignación, entonces ${\displaystyle P}$sería verdadero después de lo cual. Por el contrario, fueron${\displaystyle P[E/x]}$ falso (es decir ${\displaystyle \neg P[E/x]}$ verdadero) antes de la declaración de asignación, ${\displaystyle P}$ luego debe ser falso.

Ejemplos de triples válidos incluyen:

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

Todas las condiciones previas que no son modificadas por la expresión se pueden transferir a la condición posterior. En el primer ejemplo, asignando${\displaystyle y:=x+1}$ no cambia el hecho de que ${\displaystyle x+1=43}$, por lo que ambas declaraciones pueden aparecer en la condición posterior. Formalmente, este resultado se obtiene aplicando el esquema de axioma con${\displaystyle P}$ ser (${\displaystyle y=43}$ y ${\displaystyle x+1=43}$), cuyos rendimientos ${\displaystyle P[(x+1)/y]}$ ser (${\displaystyle x+1=43}$ y ${\displaystyle x+1=43}$), que a su vez puede simplificarse a la condición previa dada ${\displaystyle x+1=43}$.

El esquema de axioma de asignación equivale a decir que para encontrar la condición previa, primero tome la condición posterior y reemplace todas las apariciones del lado izquierdo de la asignación con el lado derecho de la asignación. Tenga cuidado de no intentar hacer esto al revés siguiendo esta forma incorrecta de pensar:${\displaystyle \{P\}x:=E\{P[E/x]\}}$; esta regla conduce a ejemplos sin sentido como:

${\displaystyle \{x=5\}x:=3\{3=5\}}$

Otra regla incorrecta que parece tentadora a primera vista es${\displaystyle \{P\}x:=E\{P\wedge x=E\}}$; conduce a ejemplos sin sentido como:

${\displaystyle \{x=5\}x:=x+1\{x=5\wedge x=x+1\}}$

Mientras que una determinada poscondición ${\displaystyle P}$ determina de forma única la condición previa ${\displaystyle P[E/x]}$, lo contrario no es cierto. Por ejemplo:

• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}}$,
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}}$,
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}}$, y
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}}$

son instancias válidas del esquema de axioma de asignación.

El axioma de asignación propuesto por Hoare no se aplica cuando más de un nombre puede referirse al mismo valor almacenado. Por ejemplo,

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

está mal si ${\displaystyle x}$ y ${\displaystyle y}$se refieren a la misma variable ( aliasing ), aunque es una instancia adecuada del esquema de axioma de asignación (con ambos${\displaystyle \{P\}}$ y ${\displaystyle \{P[2/x]\}}$ ser ${\displaystyle \{y=3\}}$).

Regla de composicion

Verificación de código de intercambio sin variables auxiliares

Las tres declaraciones siguientes (línea 2, 4, 6) intercambian los valores de las variables ${\displaystyle a}$ y ${\displaystyle b}$, sin necesidad de una variable auxiliar. En la prueba de verificación, el valor inicial de ${\displaystyle a}$ y ${\displaystyle b}$ se denota por la constante ${\displaystyle A}$ y ${\displaystyle B}$, respectivamente. Es mejor leer la prueba al revés, comenzando desde la línea 7; por ejemplo, la línea 5 se obtiene de la línea 7 reemplazando ${\displaystyle a}$ (expresión de destino en la línea 6) por ${\displaystyle a-b}$(expresión fuente en la línea 6). Algunas simplificaciones aritméticas se utilizan tácitamente, a saber. ${\displaystyle a-(a-b)=b}$ (línea 5 → 3), y ${\displaystyle a+b-b=a}$ (línea 3 → 1). Nr Código Afirmaciones 1:       ${\displaystyle \{a=A\wedge b=B\}}$ 2: ${\displaystyle a:=a+b;}$       3: ${\displaystyle \{a-b=A\wedge b=B\}}$ 4: ${\displaystyle b:=a-b;}$ 5: ${\displaystyle \{b=A\wedge a-b=B\}}$ 6: ${\displaystyle a:=a-b}$ 7: ${\displaystyle \{b=A\wedge a=B\}}$

La regla de composición de Hoare se aplica a programas ejecutados secuencialmente ${\displaystyle S}$ y ${\displaystyle T}$, dónde ${\displaystyle S}$ se ejecuta antes de ${\displaystyle T}$ y esta escrito ${\displaystyle S;T}$ (${\displaystyle Q}$se llama condición intermedia ): ^[4]

${\displaystyle {\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}}$

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

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

y

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

Por la regla de secuenciación, se concluye:

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

Otro ejemplo se muestra en el cuadro de la derecha.

Regla condicional

${\displaystyle {\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\{Q\}}}}$

La regla condicional establece que una poscondición ${\displaystyle Q}$ común a ${\displaystyle {\textbf {then}}}$ y ${\displaystyle {\textbf {else}}}$ parte es también una condición posterior del todo ${\displaystyle {\textbf {if}}\cdots {\textbf {endif}}}$declaración. En el${\displaystyle {\textbf {then}}}$ y el ${\displaystyle {\textbf {else}}}$ parte, la condición innecesaria y negada ${\displaystyle B}$ se puede agregar a la condición previa ${\displaystyle P}$, respectivamente. La condición,${\displaystyle B}$, no debe tener efectos secundarios. En la siguiente sección se ofrece un ejemplo .

Esta regla no estaba contenida en la publicación original de Hoare. ^[1] Sin embargo, desde una declaración

${\displaystyle {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}}$

tiene el mismo efecto que una construcción de bucle de una sola vez

${\displaystyle {\textbf {bool}}\ b:={\textbf {true}};{\textbf {while}}\ B\wedge b\ {\textbf {do}}\ S;b:={\textbf {false}}\ {\textbf {done}};b:={\textbf {true}};{\textbf {while}}\ \neg B\wedge b\ {\textbf {do}}\ T;b:={\textbf {false}}\ {\textbf {done}}}$

la regla condicional se puede derivar de las otras reglas de Hoare. De manera similar, las reglas para otras construcciones de programas derivados, como${\displaystyle {\textbf {for}}}$ círculo, ${\displaystyle {\textbf {do}}\cdots {\textbf {until}}}$ círculo, ${\displaystyle {\textbf {switch}}}$, ${\displaystyle {\textbf {break}}}$, ${\displaystyle {\textbf {continue}}}$puede reducirse mediante la transformación del programa a las reglas del artículo original de Hoare.

Regla de consecuencia

${\displaystyle {\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}}$

Esta regla permite fortalecer la condición previa ${\displaystyle P_{2}}$ y / o debilitar la poscondición ${\displaystyle Q_{2}}$. Se utiliza, por ejemplo, para lograr condiciones posteriores literalmente idénticas para el${\displaystyle {\textbf {then}}}$ y el ${\displaystyle {\textbf {else}}}$ parte.

Por ejemplo, una prueba de

${\displaystyle \{0\leq x\leq 15\}{\textbf {if}}\ x<15\ {\textbf {then}}\ x:=x+1\ {\textbf {else}}\ x:=0\ {\textbf {endif}}\{0\leq x\leq 15\}}$

necesita aplicar la regla condicional, que a su vez requiere probar

${\displaystyle \{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}}$, o simplificado

${\displaystyle \{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$

Para el ${\displaystyle {\textbf {then}}}$ parte, y

${\displaystyle \{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}}$, o simplificado

${\displaystyle \{x=15\}x:=0\{0\leq x\leq 15\}}$

Para el ${\displaystyle {\textbf {else}}}$ parte.

Sin embargo, la regla de asignación para el ${\displaystyle {\textbf {then}}}$ parte requiere elegir ${\displaystyle P}$ como ${\displaystyle 0\leq x\leq 15}$; la aplicación de reglas, por tanto, produce

${\displaystyle \{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}}$, que es lógicamente equivalente a

${\displaystyle \{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$.

La regla de la consecuencia es necesaria para fortalecer la condición previa ${\displaystyle \{-1\leq x<15\}}$ obtenido de la regla de asignación a ${\displaystyle \{0\leq x<15\}}$ requerido para la regla condicional.

Del mismo modo, para el ${\displaystyle {\textbf {else}}}$ parte, la regla de asignación produce

${\displaystyle \{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}}$, o equivalente

${\displaystyle \{{\textbf {true}}\}x:=0\{0\leq x\leq 15\}}$,

por lo tanto, la regla de la consecuencia debe aplicarse con ${\displaystyle P_{1}}$ y ${\displaystyle P_{2}}$ ser ${\displaystyle \{x=15\}}$ y ${\displaystyle \{{\textbf {true}}\}}$, respectivamente, para fortalecer nuevamente la condición previa. De manera informal, el efecto de la regla de la consecuencia es "olvidar" que${\displaystyle \{x=15\}}$ se conoce a la entrada de la ${\displaystyle {\textbf {else}}}$ parte, ya que la regla de asignación utilizada para el ${\displaystyle {\textbf {else}}}$ parte no necesita esa información.

Mientras gobierna

${\displaystyle {\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\{\neg B\wedge P\}}}}$

Aquí ${\displaystyle P}$es el ciclo invariante , que debe ser preservado por el cuerpo del ciclo${\displaystyle S}$. Una vez finalizado el ciclo, este invariante${\displaystyle P}$ todavía se mantiene, y además ${\displaystyle \neg B}$debe haber causado el final del ciclo. Como en la regla condicional,${\displaystyle B}$ no debe tener efectos secundarios.

Por ejemplo, una prueba de

${\displaystyle \{x\leq 10\}{\textbf {while}}\ x<10\ {\textbf {do}}\ x:=x+1\ {\textbf {done}}\{\neg x<10\wedge x\leq 10\}}$

por el momento, la regla requiere probar

${\displaystyle \{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}}$, o simplificado

${\displaystyle \{x<10\}x:=x+1\{x\leq 10\}}$,

que se obtiene fácilmente mediante la regla de asignación. Finalmente, la poscondición${\displaystyle \{\neg x<10\wedge x\leq 10\}}$ se puede simplificar a ${\displaystyle \{x=10\}}$.

Para otro ejemplo, la regla while se puede usar para verificar formalmente el siguiente programa extraño para calcular la raíz cuadrada exacta ${\displaystyle x}$ de un número arbitrario ${\displaystyle a}$-incluso si ${\displaystyle x}$ es una variable entera y ${\displaystyle a}$ no es un número cuadrado:

${\displaystyle \{{\textbf {true}}\}{\textbf {while}}\ x\cdot x\neq a\ {\textbf {do}}\ {\textbf {skip}}\ {\textbf {done}}\{x\cdot x=a\wedge {\textbf {true}}\}}$

Después de aplicar la regla while con ${\displaystyle P}$ ser ${\displaystyle {\textbf {true}}}$, queda por probar

${\displaystyle \{{\textbf {true}}\wedge x\cdot x\neq a\}{\textbf {skip}}\{{\textbf {true}}\}}$,

que se sigue de la regla de salto y la regla de consecuencia.

De hecho, el extraño programa es parcialmente correcto: si terminara, es seguro que${\displaystyle x}$ debe haber contenido (por casualidad) el valor de ${\displaystyle a}$raíz cuadrada de. En todos los demás casos, no terminará; por lo tanto, no es del todo correcto.

Mientras que la regla para la corrección total

Si la regla while ordinaria anterior se reemplaza por la siguiente, el cálculo de Hoare también puede usarse para probar la corrección total , es decir, la terminación ^{[nota 3]} así como la corrección parcial. Comúnmente, aquí se usan corchetes en lugar de llaves para indicar la noción diferente de corrección del programa.

${\displaystyle {\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}[\neg B\wedge P\wedge t\in D]}}}$

En esta regla, además de mantener el ciclo invariante, también se prueba la terminación mediante una expresión${\displaystyle t}$, llamada variante de bucle , cuyo valor disminuye estrictamente con respecto a una relación bien fundada ${\displaystyle <}$ en algún conjunto de dominios ${\displaystyle D}$durante cada iteración. Desde${\displaystyle <}$está bien fundada, una cadena estrictamente decreciente de miembros de${\displaystyle D}$ solo puede tener una longitud finita, por lo que ${\displaystyle t}$no puede seguir disminuyendo para siempre. (Por ejemplo, el orden habitual${\displaystyle <}$está bien fundamentado en números enteros positivos ${\displaystyle \mathbb {N} }$, pero ni en los enteros ${\displaystyle \mathbb {Z} }$ni en números reales positivos ${\displaystyle \mathbb {R} ^{+}}$; todos estos conjuntos se entienden en el sentido matemático, no en el sentido informático, todos son infinitos en particular.)

Dado el ciclo invariante ${\displaystyle P}$, la condición ${\displaystyle B}$ debe implicar que ${\displaystyle t}$no es un elemento mínimo de${\displaystyle D}$, porque de lo contrario el cuerpo ${\displaystyle S}$ no pudo disminuir ${\displaystyle t}$más adelante, es decir, la premisa de la regla sería falsa. (Ésta es una de varias notaciones para una corrección total). ^{[Nota 4]}

Reanudando el primer ejemplo de la sección anterior , para una prueba de corrección total de

${\displaystyle [x\leq 10]{\textbf {while}}\ x<10\ {\textbf {do}}\ x:=x+1\ {\textbf {done}}[\neg x<10\wedge x\leq 10]}$

la regla while para la corrección total se puede aplicar con, por ejemplo, ${\displaystyle D}$ siendo los enteros no negativos con el orden habitual, y la expresión ${\displaystyle t}$ ser ${\displaystyle 10-x}$, que a su vez requiere probar

${\displaystyle [x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]}$

Hablando informalmente, tenemos que demostrar que la distancia ${\displaystyle 10-x}$disminuye en cada ciclo de bucle, mientras que siempre permanece no negativo; este proceso sólo puede continuar durante un número finito de ciclos.

El objetivo de prueba anterior se puede simplificar a

${\displaystyle [x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]}$,

que se puede probar de la siguiente manera:

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]}$ se obtiene mediante la regla de asignación, y

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]}$ puede ser fortalecido para ${\displaystyle [x<10\wedge 10-x=z]}$ por la regla de la consecuencia.

Para el segundo ejemplo de la sección anterior , por supuesto, no hay expresión${\displaystyle t}$ se puede encontrar que disminuye por el cuerpo del bucle vacío, por lo que no se puede probar la terminación.

Ver también

• Afirmación (informática)
• Comunicando procesos secuenciales
• Diseño por contrato
• Semántica denotacional
• Lógica dinámica
• Edsger W. Dijkstra
• Invariable de bucle
• Semántica del transformador de predicados
• Verificación del programa
• Cálculo de refinamiento
• Lógica de separación
• Cálculo secuencial
• Análisis de código estático

Notas

1. Hoare escribió originalmente "${\displaystyle P\{C\}Q}$" en vez de "${\displaystyle \{P\}C\{Q\}}$".
2. Este artículo utiliza unanotación de estilo de deducción natural para las reglas. Por ejemplo,${\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}$ informalmente significa "Si ambos ${\displaystyle \alpha }$ y ${\displaystyle \beta }$ espera, entonces también ${\displaystyle \phi }$ sostiene "; ${\displaystyle \alpha }$ y ${\displaystyle \beta }$ se llaman antecedentes de la regla, ${\displaystyle \phi }$se llama su sucesor. Una regla sin antecedentes se llama axioma y se escribe como${\displaystyle {\dfrac {}{\quad \phi \quad }}}$.
3. "Terminación" aquí se entiende en el sentido más amplio de que el cálculo finalmente se terminará; sí no implica que no hubo violación de límite (por ejemplo, división por cero) puede detener el programa antes de tiempo.
4. El artículo de Hoare de 1969 no proporcionó una regla de corrección total; cf. su discusión en la página 579 (arriba a la izquierda). Por ejemplo, el libro de texto de Reynolds ( John C. Reynolds (2009). Teoría de los lenguajes de programación . Cambridge University Press.), Sección 3.4, p.64 da la siguiente versión de una regla de corrección total: ${\displaystyle {\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}[P\wedge \neg B]}}}$ Cuándo ${\displaystyle z}$ es una variable entera que no aparece libre en ${\displaystyle P}$, ${\displaystyle B}$, ${\displaystyle S}$, o ${\displaystyle t}$, y ${\displaystyle t}$ es una expresión entera (el nombre de las variables de Reynolds se cambió para adaptarse a la configuración de este artículo).

Referencias

1. Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática" (PDF) . Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145 / 363235.363259 .
2. RW Floyd . " Asignación de significados a los programas " . Actas de los simposios de la American Mathematical Society sobre matemáticas aplicadas. Vol. 19, págs. 19–31. 1967.
3. p.579 arriba a la izquierda
4. Huth, Michael; Ryan, Mark (26 de agosto de 2004). Lógica en Ciencias de la Computación (segunda ed.). TAZA. pag. 276. ISBN 978-0521543101.

Otras lecturas

• Robert D. Tennent. Especificación de software (un libro de texto que incluye una introducción a la lógica de Hoare, escrito en 2002) ISBN  0-521-00401-2

enlaces externos

• KeY-Hoare es un sistema de verificación semiautomático construido sobre el demostrador del teorema de KeY . Cuenta con un cálculo Hoare para un lenguaje sencillo mientras.
• Cálculo j-Algo-modul Hoare : una visualización del cálculo Hoare en el programa de visualización de algoritmos j-Algo