Lógica de Hoare

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

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

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 se cumple 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\}}}}$

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

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

Ejemplos de tríos 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 por la expresión pueden trasladarse a la postcondición. En el primer ejemplo, asignando${\displaystyle y:=x+1}$eso no cambia el hecho de que${\displaystyle x+1=43}$, por lo que ambas afirmaciones pueden aparecer en la postcondición. Formalmente, este resultado se obtiene aplicando el esquema axiomático con P siendo (${\displaystyle y=43}$y${\displaystyle x+1=43}$), lo que produce${\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 del axioma de asignación equivale a decir que para encontrar la precondición, primero se toma la postcondición y se reemplazan todas las ocurrencias del lado izquierdo de la asignación con el lado derecho. Tenga cuidado de no intentar hacerlo al revés siguiendo esta forma incorrecta de pensar:${\displaystyle \{P\}x:=E\{P[E/x]\}}$; esta regla da lugar 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\}}$; esto lleva a ejemplos sin sentido como:

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

Mientras que una postcondición dada P determina de manera única la precondición${\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 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 ( aliasing ), aunque es una instancia adecuada del esquema del axioma de asignación (con ambos${\displaystyle \{P\}}$y${\displaystyle \{P[2/x]\}}$ser${\displaystyle \{y=3\}}$).

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

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

Por ejemplo, consideremos los dos siguientes casos del axioma de asignación:

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

y

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

Según la regla de secuenciación, se concluye:

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

En el recuadro de la derecha se muestra otro ejemplo.

${\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 postcondición Q común a la parte then y else también es una postcondición de toda la instrucción if...endif . ^{[ 5 ]} En la parte then y else , la condición B no negada y negada se puede 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 demás reglas de Hoare. De manera similar, las reglas para otras construcciones de programas derivadas, como el bucle for , el bucle do...until , switch , break y continue , se pueden reducir mediante la transformación del programa a las reglas del artículo original de Hoare.

${\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.${\displaystyle P_{2}}$y/o debilitar la condición posterior${\displaystyle Q_{2}}$Se utiliza, por ejemplo, para lograr postcondiciones literalmente idénticas para la parte then y la parte else .

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 demostrar

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

por 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 otra parte.

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

${\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 reforzar 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.

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${\displaystyle P_{1}}$y${\displaystyle P_{2}}$ser${\displaystyle \{x=15\}}$y${\displaystyle \{{\texttt {true}}\}}$, respectivamente, para reforzar nuevamente la condición previa. De manera informal, el efecto de la regla de consecuencia es "olvidar" que${\displaystyle \{x=15\}}$se conoce al inicio de la parte else , ya que la regla de asignación utilizada para la parte else no necesita esa información.

${\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 ser preservado por el cuerpo del bucle S. Después de que el bucle haya terminado, este invariante P todavía se cumple, y además${\displaystyle \neg B}$debe haber provocado que el bucle terminara. Como en la regla condicional, B no debe tener efectos secundarios.

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 del mientras que 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 postcondición${\displaystyle \{\neg x<10\wedge x\leq 10\}}$se puede simplificar a${\displaystyle \{x=10\}}$.

Por 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 por demostrar

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

lo cual se deduce de la regla de omisión y la regla de consecuencia.

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

Si se reemplaza la regla while ordinaria anterior por la siguiente, el cálculo de Hoare también puede utilizarse para demostrar la corrección total , es decir, la terminación, así como la corrección parcial. Generalmente, se utilizan corchetes en lugar de llaves para indicar la diferente noción 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 el invariante del bucle, también se demuestra la terminación mediante una expresión t , llamada variante del bucle , cuyo valor disminuye estrictamente con respecto a una relación bien fundada < en algún conjunto de dominio D durante cada iteración. Dado que < está bien fundada, una cadena estrictamente decreciente de miembros de D solo puede tener una longitud finita, por lo que t no puede seguir disminuyendo indefinidamente. (Por ejemplo, el orden usual < está bien fundado en enteros positivos${\displaystyle \mathbb {N} }$pero tampoco en los números 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 computacional; en particular, todos son infinitos).

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 enteros no negativos con el orden usual, y la expresión t siendo ${\displaystyle 10-x}$, lo cual a su vez requiere demostrar

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

En términos informales, tenemos que demostrar que la distancia${\displaystyle 10-x}$disminuye en cada ciclo del bucle, mientras que siempre permanece no negativo; este proceso solo puede continuar durante un número finito de ciclos.

El objetivo de la demostración anterior se puede simplificar a

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

lo cual puede demostrarse 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 fortalecerse 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 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.