Lógica antigua

Reglas para verificar la corrección de un programa informático

La lógica de Hoare (también conocida como lógica 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 informáticos . Fue propuesta en 1969 por el informático y lógico británico Tony Hoare , y posteriormente refinada 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 .

Triple hoare

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ómputo. Un triple de Hoare tiene la forma

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

donde y son afirmaciones y es un comando . ^{[nota 1]} se denomina condición previa y 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 la lógica de predicados . ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle P}$ ${\displaystyle Q}$

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, Hoare y muchos otros investigadores han desarrollado reglas para otras construcciones del lenguaje desde entonces. Hay reglas para concurrencia , procedimientos , saltos y punteros .

Corrección parcial y total

Usando la lógica estándar de Hoare, solo se puede probar una corrección parcial . La corrección total requiere además la terminación , que se puede probar por separado o con una versión extendida de la regla While. ^[3] Por lo tanto, la lectura intuitiva de una tripleta de Hoare es: Siempre que se cumple del estado antes de la ejecución de , entonces se cumplirá después, o no termina. En el último caso, no hay "después", por lo que puede haber cualquier enunciado. De hecho, uno puede elegir que sea falso para expresar que no termina. ${\displaystyle P}$ ${\displaystyle C}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle Q}$ ${\displaystyle Q}$ ${\displaystyle C}$

"Terminación" aquí y en el resto de este artículo se entiende en el sentido más amplio de que el cálculo terminará eventualmente, es decir, implica la ausencia de bucles infinitos; no implica la ausencia de violaciones de límites de implementación (por ejemplo, división por cero) que detengan el programa prematuramente. En su artículo de 1969, Hoare utilizó una noción más estrecha de terminación que también implicaba la ausencia de violaciones de límites de implementación, y expresó su preferencia por la noción más amplia de terminación ya que mantiene las aserciones independientes de la implementación: ^[4]

Otra deficiencia de los axiomas y reglas citados anteriormente es que no dan ninguna base para demostrar que un programa termina con éxito. El hecho de que no se termine puede deberse a un bucle infinito; o puede deberse a la violación de un límite definido por la implementación, por ejemplo, el rango de operandos numéricos, el tamaño de almacenamiento o un límite de tiempo del sistema operativo. Por lo tanto, la notación “ ” debe interpretarse como “siempre que el programa termine con éxito, las propiedades de sus resultados se describen mediante ”. Es bastante fácil adaptar los axiomas de modo que no se puedan usar para predecir los “resultados” de programas que no terminan; pero el uso real de los axiomas dependería ahora del conocimiento de muchas características dependientes de la implementación, por ejemplo, el tamaño y la velocidad de la computadora, el rango de números y la elección de la técnica de desbordamiento. Aparte de las pruebas de cómo evitar los bucles infinitos, probablemente sea mejor demostrar la corrección “condicional” de un programa y confiar en que una implementación dé una advertencia si ha tenido que abandonar la ejecución del programa como resultado de la violación de un límite de implementación. ${\displaystyle P\{Q\}R}$ ${\displaystyle R}$

Normas

Esquema axiomático de enunciado vacío

La regla de declaración vacía afirma que la declaración skip no cambia el estado del programa, por lo tanto, todo lo que es verdadero antes de skip también es verdadero después. ^{[nota 2]}

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

Esquema del 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, sea P una afirmación en la que la variable x es libre . Entonces:

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

donde denota la afirmación P en la que cada aparición libre de x ha sido reemplazada por la expresión E . ${\displaystyle P[E/x]}$

El esquema del axioma de asignación significa que la verdad de es equivalente a la verdad de P después de la asignación . Por lo tanto, si fuera verdadera antes de la asignación, según el axioma de asignación, entonces P sería verdadera después de la asignación. Por el contrario, si fuera falsa (es decir, verdadera) antes del enunciado de asignación, P debe ser falsa después. ${\displaystyle P[E/x]}$ ${\displaystyle P[E/x]}$ ${\displaystyle P[E/x]}$ ${\displaystyle \neg P[E/x]}$

Algunos 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 precondiciones que no se modifican con la expresión se pueden trasladar a la poscondición. En el primer ejemplo, la asignación no cambia el hecho de que , por lo que ambas afirmaciones pueden aparecer en la poscondición. Formalmente, este resultado se obtiene aplicando el esquema axiomático con P siendo ( y ), lo que da como resultado ( y ), que a su vez se puede simplificar a la precondición dada . ${\displaystyle y:=x+1}$ ${\displaystyle x+1=43}$ ${\displaystyle y=43}$ ${\displaystyle x+1=43}$ ${\displaystyle P[(x+1)/y]}$ ${\displaystyle x+1=43}$ ${\displaystyle x+1=43}$ ${\displaystyle x+1=43}$

El esquema del axioma de asignación equivale a decir que para encontrar la condición previa, primero se toma la condición posterior y se reemplazan todas las ocurrencias 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: ; esta regla conduce a ejemplos sin sentido como: ${\displaystyle \{P\}x:=E\{P[E/x]\}}$

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

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

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

Si bien una determinada poscondición P determina de manera única la precondición , lo inverso no es cierto. Por ejemplo: ${\displaystyle P[E/x]}$

• ${\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 del 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\}}$

es incorrecto si x e y se refieren a la misma variable ( alias ), aunque es una instancia apropiada del esquema del axioma de asignación ( siendo y ambos ). ${\displaystyle \{P\}}$ ${\displaystyle \{P[2/x]\}}$ ${\displaystyle \{y=3\}}$

Regla de composición

La regla de composición de Hoare se aplica a los programas ejecutados secuencialmente S y T , donde S se ejecuta antes que T y se escribe ( Q se denomina condición intermedia ): ^[5] ${\displaystyle S;T}$

${\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\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}}$

La regla condicional establece que una poscondición Q común a las partes then y else es también una poscondición de toda la declaración if...endif . ^[6] En las partes then y else , la condición no negada y negada B se pueden agregar a la precondición P , respectivamente. La condición, B , no debe tener efectos secundarios. Se da un ejemplo en la siguiente sección.

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

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

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

${\displaystyle {\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {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 for loop, do...until loop, switch , break , continue se pueden reducir 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 reforzar la condición previa y/o debilitar la condición posterior . Se utiliza, por ejemplo, para lograr condiciones posteriores literalmente idénticas para la parte then y else . ${\displaystyle P_{2}}$ ${\displaystyle Q_{2}}$

Por ejemplo, una prueba de

${\displaystyle \{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {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 la parte de entonces , 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 la parte demás .

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

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

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

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

De manera similar, para la parte else , la regla de asignación produce

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

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

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

Mientras que la regla

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

Aquí P es el invariante del bucle , que debe conservarse mediante el cuerpo del bucle S. Una vez finalizado el bucle, este invariante P sigue siendo válido y, además, debe haber provocado la finalización del bucle. Como en la regla condicional, B no debe tener efectos secundarios. ${\displaystyle \neg B}$

Por ejemplo, una prueba de

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

por la regla while se 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 se puede simplificar a . ${\displaystyle \{\neg x<10\wedge x\leq 10\}}$ ${\displaystyle \{x=10\}}$

Como otro ejemplo, la regla while se puede utilizar para verificar formalmente el siguiente programa extraño para calcular la raíz cuadrada exacta x de un número arbitrario a —incluso si x es una variable entera y a no es un número cuadrado:

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

Después de aplicar la regla while con P siendo verdadero , queda demostrar

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

lo cual se desprende de la regla de salto y de la regla de consecuencia.

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

Mientras que la regla de la corrección total

Si la regla while ordinaria anterior se reemplaza por la siguiente, el cálculo de Hoare también se puede utilizar para demostrar la corrección total , es decir, la terminación, así como la corrección parcial. Comúnmente, aquí se utilizan 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]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}}$

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

Dado el invariante de bucle P , la condición B debe implicar que t no es un elemento mínimo de D , ya que de lo contrario el cuerpo S no podría disminuir t más, es decir, la premisa de la regla sería falsa. (Esta es una de las diversas notaciones para la corrección total.) ^{[nota 3]}

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

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

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

${\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 disminuye en cada ciclo del bucle, aunque siempre permanece no negativa; este proceso solo puede continuar durante un número finito de ciclos. ${\displaystyle 10-x}$

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]}$,

Lo cual se puede demostrar 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 por la regla de asignación, y

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]}$puede reforzarse mediante la regla de consecuencia. ${\displaystyle [x<10\wedge 10-x=z]}$

Para el segundo ejemplo de la sección anterior, por supuesto no se puede encontrar ninguna expresión t que sea disminuida por el cuerpo del bucle vacío, por lo tanto no se puede probar la terminación.

Véase también

• Afirmación (desarrollo de software)
• Semántica denotacional
• Diseño por contrato
• Lógica dinámica
• Verificación formal
• Invariante de bucle
• Semántica del transformador de predicados
• Análisis de programas estáticos

Notas

1. Hoare originalmente escribió " " en lugar de " ". ${\displaystyle P\{C\}Q}$ ${\displaystyle \{P\}C\{Q\}}$
2. Este artículo utiliza una notación de estilo de deducción natural para las reglas. Por ejemplo, informalmente significa "Si tanto α como β se cumplen, entonces también φ se cumple"; α y β se denominan antecedentes de la regla, φ se denomina su sucedente. Una regla sin antecedentes se denomina axioma y se escribe como . ${\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}$ ${\displaystyle {\dfrac {}{\quad \phi \quad }}}$
3. El artículo de Hoare de 1969 no proporcionó una regla de corrección total; cf. su discusión en la p. 579 (arriba a la izquierda). Por ejemplo, el libro de texto de Reynolds ^[3] proporciona la siguiente versión de una regla de corrección total: cuando z es una variable entera que no aparece libremente en P , B , S o t , y t es una expresión entera (las variables de Reynolds se renombraron para que se ajusten a la configuración de este artículo). ${\displaystyle {\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}}$

Referencias

1. Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática". Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175.
2. RW Floyd . "Asignación de significados a los programas". Actas de los Simposios de la Sociedad Matemática Americana sobre Matemáticas Aplicadas. Vol. 19, págs. 19-31. 1967.
3. John C. Reynolds (2009). Teorías de lenguajes de programación . Cambridge University Press.) Aquí: Sect. 3.4, p. 64.
4. Hoare (1969), págs. 578-579
5. Huth, Michael; Ryan, Mark (26 de agosto de 2004). Lógica en informática (segunda edición). CUP. pág. 276. ISBN 978-0521543101.
6. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (diciembre de 2019). "Cincuenta años de lógica de Hoare". Aspectos formales de la informática . 31 (6): 759. doi :10.1007/s00165-019-00501-3. S2CID  102351597.

Lectura adicional

• Robert D. Tennent. Specifying Software (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 de teoremas KeY . Incluye un cálculo de Hoare para un lenguaje while simple.
• Módulo de cálculo de Hoare de j-Algo (j-Algo en GitHub , j-Algo en SourceForge ): una visualización del cálculo de Hoare en el programa de visualización de algoritmos j-Algo.