Hoare logica

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

Reglas para verificar la corrección del programa informático

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 el razonamiento. rigurosamente sobre la corrección de los programas informáticos. Fue propuesto en 1969 por el informático y lógico británico Tony Hoare, y posteriormente perfeccionado por Hoare y otros investigadores. Las ideas originales fueron sembradas por el trabajo de Robert W. Floyd, quien había publicado un sistema similar para diagramas de flujo.

Hoare triple

La característica central de la lógica Hoare es el triple Hoare. Un triple describe cómo la ejecución de una pieza de código cambia el estado de la computación. Un triple de Hoare es de la forma

{displaystyle {P}C{Q}}

Donde $P$ y $Q$ son afirmaciones y $C$ es un comando. $P$ se llama condición previa y $Q$ el condición previa: cuando se cumple la condición previa, ejecutar el comando establece la condición previa. Las aserciones son fórmulas en lógica predicada.

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

Corrección parcial y total

Uso estándar Lógica de Hoare, sólo se puede probar la corrección parcial. La corrección total requiere además la terminación, que puede ser probada por separado o con una versión ampliada de la regla de Mientras. Así la lectura intuitiva de un triple Hoare es: Siempre $P$ del estado antes de la ejecución de $C$ , entonces $Q$ se mantendrá después, o $C$ no termina. En este último caso, no hay "después", así que $Q$ puede ser cualquier declaración en absoluto. De hecho, uno puede elegir $Q$ ser falso para expresar eso $C$ no termina.

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

Otra deficiencia en los axiomas y reglas citados anteriormente es que no dan base para una prueba de que un programa termina con éxito. La falta de terminación 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 operados numéricos, el tamaño del almacenamiento o un límite de tiempo del sistema operativo. Así la notación “ ${displaystyle P{Q}R}$ ” debe ser interpretado “siempre que el programa termina con éxito, las propiedades de sus resultados se describen por $R$ . Es bastante fácil de adaptar los axiomas para que no puedan utilizarse para predecir los “resultos” de los programas que no están terminando; pero el uso real de los axiomas ahora dependería 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 la evitación de bucles infinitos, es probablemente mejor probar la corrección "condicional" de un programa y depender de una implementación para dar 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.

Reglas

Esquema de axioma 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, lo que sea cierto antes de skip también vale después.

{displaystyle {dfrac {}{{P}{texttt {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 se cumple para la variable. Formalmente, sea $P$ una afirmación en la que la variable $x$ es gratis. Entonces:

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

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

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

Ejemplos de triples válidos incluyen:

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

Todas las condiciones previas que no sean modificadas por la expresión se pueden llevar a la condición previa. En el primer ejemplo, asignación ${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 previa. Formally, este resultado se obtiene aplicando el esquema axiom con $P$ Siendo ${displaystyle y=43}$ y ${displaystyle x+1=43}$ ), que rinde ${displaystyle P[(x+1)/y]}$ Siendo ${displaystyle x+1=43}$ y ${displaystyle x+1=43}$ ), que a su vez se puede simplificar a la condición previa dada ${displaystyle x+1=43}$ .

El esquema de axioma de asignación es equivalente a decir que para encontrar la condición previa, primero tome la condición previa y reemplace todos los casos de la parte izquierda de la asignación por la parte derecha de la asignación. Tenga cuidado de no tratar de hacer esto al revés siguiendo esto incorrecta forma de pensar: ${displaystyle {P}x:=E{P[E/x]}}$ ; esta regla conduce a ejemplos no sensibles como:

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

Otro incorrecta regla mirando tentación a primera vista es ${displaystyle {P}x:=E{Pwedge x=E}}$ ; conduce a ejemplos no sensibles como:

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

Mientras que una condición posterior dada $P$ determina la condición previa ${displaystyle P[E/x]}$ , el contrario no es cierto. Por ejemplo:

${displaystyle {0leq ycdot ywedge ycdot yleq 9}x:=ycdot y{0leq xwedge xleq 9}}$ ,
${displaystyle {0leq ycdot ywedge ycdot yleq 9}x:=ycdot y{0leq xwedge ycdot yleq 9}}$ ,
${displaystyle {0leq ycdot ywedge ycdot yleq 9}x:=ycdot y{0leq ycdot ywedge xleq 9}}$ , y
${displaystyle {0leq ycdot ywedge ycdot yleq 9}x:=ycdot y{0leq ycdot ywedge ycdot yleq 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. $x$ y $Sí.$ referencia 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]}}$ estar ${displaystyle {y=3}}$ ).

Regla de composición

Código de intercambio verificador
sin variables auxiliares

Las tres declaraciones siguientes (línea 2, 4, 6) intercambian los valores de las variables $a$ y $b$ , sin necesidad de una variable auxiliar. En la prueba de verificación, el valor inicial $a$ y $b$ es denotado por la constante $A$ y $B$ , respectivamente. La prueba es mejor leer hacia atrás, a partir de la línea 7; por ejemplo, la línea 5 se obtiene de la línea 7 sustituyendo $a$ (expresión objetivo en la línea 6) por $a-b$ (expresión de fuente en la línea 6). Algunas simplificaciones aritméticas se utilizan tácitamente, viz. ${displaystyle a-(a-b)=b}$ (line 5→3), and ${displaystyle a+b-b=a}$ (line 3→1).
Nr	Código	Asserciones
1:		${displaystyle {a=Awedge b=B}}$
2:	${displaystyle a:=a+b;}$
3:		${displaystyle {a-b=Awedge b=B}}$
4:	${displaystyle b:=a-b;}$
5:		${displaystyle {b=Awedge a-b=B}}$
6:	${displaystyle a:=a-b}$
7:		${displaystyle {b=Awedge a=B}}$

La regla de composición de Hoare se aplica a los programas de ejecución secuencial $S$ y $T$ , donde $S$ ejecutadas antes de $T$ y está escrito ${displaystyle S;T}$ () $Q$ se llama de mitad de período):

{displaystyle {dfrac {{P}S{Q}quadquad {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}}

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

Por la regla de secuencia, uno 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 {{Bwedge P}S{Q}quadquad {neg Bwedge P}T{Q}}{{P}{texttt {if}} B {texttt {then}} S {texttt {else}} T {texttt {endif}}{Q}}}}

La regla condicional establece que una condición posterior $Q$ común a entonces y La parte else también es una condición posterior de toda la instrucción if...endif. En la parte then y else, la condición no negada y negada $B$ se puede agregar a la condición previa $P$ , respectivamente. La condición, $B$ , no debe tener efectos secundarios. En la siguiente sección se da un ejemplo.

Esta regla no figuraba en la publicación original de Hoare. Sin embargo, desde 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}} Bwedge b {texttt {do}} S;b:={texttt {false}} {texttt {done}};b:={texttt {true}};{texttt {while}} neg Bwedge 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 de Hoare&# 39;s papel original.

Regla de consecuencia

{displaystyle {dfrac {P_{1}rightarrow P_{2}quadquad {P_{2}}S{Q_{2}}quadquad Q_{2}rightarrow Q_{1}}{{P_{1}}S{Q_{1}}}}}

Esta norma permite fortalecer la condición previa $P_{2}$ y/o debilitar la condición previa $Q_{2}$ . Se utiliza por ejemplo para lograr condiciones literales idénticas para las entonces y el más parte.

Por ejemplo, una prueba de

<math alttext="{displaystyle {0leq xleq 15}{texttt {if}} x{}0≤ ≤ x≤ ≤ 15}six.15entoncesx:=x+1másx:=0endif{}0≤ ≤ x≤ ≤ 15}[displaystyle {0leq xleq 15}{textt {if}x}ccccccccH}ccc\cH}\ccH00}ccc\ccH00}\cH00}\cH0cH0\cH0}\\cH0}\\\cH00}}}\\\cH0cH0cH0cH0cccH3c\ccccccccccccH}}}}}}}}\cc\c\\cccccH3ccH3}}}\cH3}}}cccccc\ccccccH<img alt="{displaystyle {0leq xleq 15}{texttt {if}} x

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

<math alttext="{displaystyle {0leq xleq 15wedge x{}0\leq \leq x\leq \leq 15\land \land x.15}x:=x+1{}0\leq \leq x\leq \leq 15}{displaystyle {0leq xleq 15wedge xiere15}x:=x+1{0leq xleq 15}} <img alt="{displaystyle {0leq xleq 15wedge x

, o simplificado

<math alttext="{displaystyle {0leq x{}0\leq \leq x.15}x:=x+1{}0\leq \leq x\leq \leq 15}{displaystyle {0leq x 10}x:=x+1{0leq xleq 15} <img alt="{displaystyle {0leq x

para la parte luego, y

{displaystyle {0leq xleq 15wedge xgeq 15}x:=0{0leq xleq 15}}

, o simplificado

{displaystyle {x=15}x:=0{0leq xleq 15}}

para la parte else.

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

{displaystyle {0leq x+1leq 15}x:=x+1{0leq xleq 15}}

, que es lógicamente equivalente a

<math alttext="{displaystyle {-1leq x{}- - 1\leq \leq x.15}x:=x+1{}0\leq \leq x\leq \leq 15}{displaystyle {-1leq x 10}x:=x+1{0leq xleq 15} <img alt="{displaystyle {-1leq x

La norma de consecuencia es necesaria para fortalecer la condición previa $<math alttext="{displaystyle {-1leq x{}- - 1\leq \leq x.15}{displaystyle {-1leq x won15} <img alt="{displaystyle {-1leq x$ obtenido de la regla de asignación a $<math alttext="{displaystyle {0leq x{}0\leq \leq x.15}{displaystyle {0leq x won15} <img alt="{displaystyle {0leq x$ requerido para la regla condicional.

Del mismo modo, para la parte else, la regla de asignación produce

{displaystyle {0leq 0leq 15}x:=0{0leq xleq 15}}

, o equivalente

{displaystyle {{texttt {true}}}x:=0{0leq xleq 15}}

por lo tanto, la norma de consecuencia debe aplicarse con $P_{1}$ y $P_{2}$ estar ${displaystyle {x=15}}$ y ${displaystyle {{texttt {true}}}}$ , respectivamente, para fortalecer nuevamente la condición previa. Informalmente, el efecto de la regla de la consecuencia es "olvidar" que ${displaystyle {x=15}}$ se conoce en la entrada de la más parte, desde la regla de asignación utilizada para más parte no necesita esa información.

Regla mientras

{displaystyle {dfrac {{Pwedge B}S{P}}{{P}{texttt {while}} B {texttt {do}} S {texttt {done}}{neg Bwedge P}}}}

Aquí. $P$ es el bucle invariante, que debe ser preservado por el cuerpo del bucle $S$ . Después de terminar el bucle, este invariante $P$ aún permanece, y además $neg B$ Debe haber causado que el bucle termine. Como en la regla condicional, $B$ no debe tener efectos secundarios.

Por ejemplo, una prueba de

<math alttext="{displaystyle {xleq 10}{texttt {while}} x<10 {texttt {do}} x:=x+1 {texttt {done}}{neg x{}x≤ ≤ 10}mientrasx.10dox:=x+1hecho{}¬ ¬ x.10∧ ∧ x≤ ≤ 10}{displaystyle {xleq 10}{texttt { while}} x 10\textttt {} x:=x+1 {fneg x 10\neg x 10h}}}\\fnegtttt {\\\\\fng}}}}}}}\\\displaystyledisplaystyle\\\\\\cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc<img alt="{displaystyle {xleq 10}{texttt {while}} x<10 {texttt {do}} x:=x+1 {texttt {done}}{neg x

por la regla while requiere probar

<math alttext="{displaystyle {xleq 10wedge x{}x\leq \leq 10\land \land x.10}x:=x+1{}x\leq \leq 10}{displaystyle {xleq 10wedge x 10}x:=x+1{xleq 10} <img alt="{displaystyle {xleq 10wedge x

, o simplificado

<math alttext="{displaystyle {x{}x.10}x:=x+1{}x\leq \leq 10}{displaystyle {x 0}x:=x+1{xleq 10} <img alt="{displaystyle {x

que se obtiene fácilmente por la regla de asignación. Por último, la condición previa $<math alttext="{displaystyle {neg x{}\neg \neg x.10\land \land x\leq \leq 10}{displaystyle {neg x 10wedge xleq 10} <img alt="{displaystyle {neg x$ se puede simplificar ${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 $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}} xcdot xneq a {texttt {do}} {texttt {skip}} {texttt {done}}{xcdot x=awedge {texttt {true}}}}

Después de aplicar la regla while con $P$ siendo true, permanece probar

{displaystyle {{texttt {true}}wedge xcdot xneq a}{texttt {skip}}{{texttt {true}}}}

que se deriva de la regla de omisión y la regla de consecuencia.

De hecho, el programa extraño es parcialmente correcto: si terminó, 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 para la corrección total

Si la regla while ordinaria anterior se reemplaza por la siguiente, el cálculo de Hoare también se puede usar para probar la corrección total, es decir, la terminación y la corrección parcial. Comúnmente, aquí se usan corchetes en lugar de llaves para indicar la noción diferente de la corrección del programa.

<math alttext="{displaystyle {dfrac {< {text{is a well-founded ordering on the set}} Dquadquad [Pwedge Bwedge tin Dwedge t=z]S[Pwedge tin Dwedge t.es una orden bien fundada en el conjuntoD,[P∧ ∧ B∧ ∧ t▪ ▪ D∧ ∧ t=z]S[P∧ ∧ t▪ ▪ D∧ ∧ t.z][P∧ ∧ t▪ ▪ D]mientrasBdoShecho[¬ ¬ B∧ ∧ P∧ ∧ t▪ ▪ D]{displaystyle {dfrac {cHFF} {fnMicrosoftware {fnMicrosoft Sans Serif} Dquadquad [Pwedge Bwedge tin Dwedge t=z]S[Pwedge tin Dwedge t madez]}{[[ Pwedge tin D]{textttt {Mientras} B {texttt { do} S {texttt {done}[neg Bwedge Pwedge tin D]}<img alt="{displaystyle {dfrac {< {text{is a well-founded ordering on the set}} Dquadquad [Pwedge Bwedge tin Dwedge t=z]S[Pwedge tin Dwedge t

En esta regla, además de mantener el bucle invariante, también se prueba la terminación por medio de una expresión $t$ , llamada la 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. Desde $.$ es bien fundada, una cadena estrictamente decreciente de miembros de $D$ puede tener sólo longitud finita, así $t$ no puede seguir disminuyendo para siempre. (Por ejemplo, el orden habitual $.$ está bien fundada en números enteros positivos $mathbb {N}$ , pero no en los enteros $mathbb {Z}$ ni en números reales positivos $mathbb {R} ^{+}$ ; todos estos conjuntos están destinados en la matemática, no en el sentido de la computación, todos son infinitos en particular.)

Dada la invariante de bucle $P$ , la condición $B$ debe implicar que $t$ no es un elemento mínimo del estilo $D$ , de lo contrario, el cuerpo $S$ no podría disminuir $t$ más allá, es decir, la premisa de la regla sería falsa. (Esta es una de varias notaciones para la corrección total).

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

<math alttext="{displaystyle [xleq 10]{texttt {while}} x<10 {texttt {do}} x:=x+1 {texttt {done}}[neg x[x\leq \leq 10]mientrasx.10dox:=x+1hecho[\neg \neg x.10\land \land x\leq \leq 10]{displaystyle [xleq 10]{texttt { while}} x 0texttt {} x:=x+1 {texttt {do}}[neg x 10wedge xleq 10]} <img alt="{displaystyle [xleq 10]{texttt {while}} x<10 {texttt {do}} x:=x+1 {texttt {done}}[neg x

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

<math alttext="{displaystyle [xleq 10wedge x<10wedge 10-xgeq 0wedge 10-x=z]x:=x+1[xleq 10wedge 10-xgeq 0wedge 10-x[x\leq \leq 10\land \land x.10\land \land 10- - x\geq \geq 0\land \land 10- - x=z]x:=x+1[x\leq \leq 10\land \land 10- - x\geq \geq 0\land \land 10- - x.z]{displaystyle [xleq 10wedge x 10wedge 10-xgeq 0wedge 10-x=z]x:=x+1[xleq 10wedge 10-xgeq 0wedge 10-x=z] <img alt="{displaystyle [xleq 10wedge x<10wedge 10-xgeq 0wedge 10-x=z]x:=x+1[xleq 10wedge 10-xgeq 0wedge 10-x

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

El objetivo de prueba anterior se puede simplificar a

<math alttext="{displaystyle [x<10wedge 10-x=z]x:=x+1[xleq 10wedge 10-x[x.10\land \land 10- - x=z]x:=x+1[x\leq \leq 10\land \land 10- - x.z]{displaystyle [x 10wedge 10-x=z]x:=x+1[xleq 10wedge 10-x didz]} <img alt="{displaystyle [x<10wedge 10-x=z]x:=x+1[xleq 10wedge 10-x

que se puede demostrar de la siguiente manera:

<math alttext="{displaystyle [x+1leq 10wedge 10-x-1<z]x:=x+1[xleq 10wedge 10-x[x+1\leq \leq 10\land \land 10- - x- - 1.z]x:=x+1[x\leq \leq 10\land \land 10- - x.z]{displaystyle [x+1leq 10wedge 10-x-1 segn]x:=x+1[xleq 10wedge 10-x se hizo realidad]} <img alt="{displaystyle [x+1leq 10wedge 10-x-1<z]x:=x+1[xleq 10wedge 10-x

se obtiene por la regla de asignación, y

<math alttext="{displaystyle [x+1leq 10wedge 10-x-1[x+1\leq \leq 10\land \land 10- - x- - 1.z]{displaystyle [x+1leq 10wedge 10-x-1traducidos]} <img alt="{displaystyle [x+1leq 10wedge 10-x-1

puede fortalecerse

<math alttext="{displaystyle [x[x.10\land \land 10- - x=z]{displaystyle [x 10wedge 10-x=z] <img alt="{displaystyle [x

por la regla de consecuencia.

Para el segundo ejemplo de la sección anterior, por supuesto no se puede encontrar ninguna expresión $t$ que disminuya por el ciclo vacío cuerpo, por lo que no se puede probar la terminación.

Contenido relacionado

Más resultados...