Verificación formal de la lógica de Hoare en Isabelle/HOL

Trabajo Fin de Máster Verificación formal de la lógica de Hoare en Isabelle/HOL Presentado por: Natividad González Blanco Tutora: Dra. María José Hidalgo Doblado, Universidad de Sevilla Septiembre de 2016 Abstract Hoare logic is a formal system developed by C.A.R. Hoare. This logic was introduced to verify formally imperative programs. That is, with the Hoare logic we can ensure and prove that a particular program performs exactly the actions for which it has been designed. An advantage to do it through a proof assistant is that in this way errors can be detected that in the handmade proofs could go unnoticed. In this dissertation, we will describe briefly the interactive theorem prover Isabelle/HOL. Then, we will present in detail the Hoare logic with examples. The major goal consists of an implementation of this logic in the proof assistant Isabelle/HOL. According as the size of a system grows, the costs of formal verification increase disproportionately. So some people think that formal verification isn’t very profitable but there are some situations in which this is vitally important such as braking systems of cars and aircraft piloting by electronic controls. 5 Índice general Índice general 7 1. Introducción 9 2. Introducción a Isabelle/HOL 13 2.1. Programación funcional en Isabelle/HOL . . . . . . . . . . . . . . . . 13 2.1.1. Números naturales, enteros y booleanos . . . . . . . . . . . . . 13 2.1.2. Definiciones no recursivas . . . . . . . . . . . . . . . . . . . . 14 2.1.3. Definiciones locales . . . . . . . . . . . . . . . . . . . . . . . . 15 2.1.4. Pares................................ 15 2.1.5. Listas ............................... 16 2.1.6. Funciones anónimas . . . . . . . . . . . . . . . . . . . . . . . . 16 2.1.7. Condicionales........................... 16 2.1.8. Definiciones recursivas . . . . . . . . . . . . . . . . . . . . . . 17 2.2. Razonamiento sobre programas en Isabelle/HOL . . . . . . . . . . . . 17 2.2.1. Razonamiento ecuacional . . . . . . . . . . . . . . . . . . . . . 17 2.2.2. Razonamiento por inducción sobre los naturales . . . . . . . . 19 2.2.3. Razonamiento por inducción sobre listas . . . . . . . . . . . . 22 2.2.4. Inducción correspondiente a la definición recursiva . . . . . . . 24 2.2.5. Razonamiento por distinción de casos . . . . . . . . . . . . . . 25 2.2.6. Heurística de generalización para la inducción . . . . . . . . . 28 2.2.7. Recursión mutua e inducción . . . . . . . . . . . . . . . . . . 29 2.3. Definiciones inductivas en Isabelle/HOL . . . . . . . . . . . . . . . . 32 2.3.1. El conjunto de los números pares . . . . . . . . . . . . . . . . 32 2.3.2. Clausura reflexiva transitiva . . . . . . . . . . . . . . . . . . . 38 3. Lógica de Hoare 43 3.1. Especificaciones.............................. 43 3.1.1. Un pequeño lenguaje de programación . . . . . . . . . . . . . 43 3.1.2. Notación de Hoare . . . . . . . . . . . . . . . . . . . . . . . . 50 3.1.3. Algunos ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.2. LógicadeHoare.............................. 53 3.2.1. Axiomas y reglas de la lógica de Hoare . . . . . . . . . . . . . 54 3.2.2. Ejemplos de ternas demostrables: corrección parcial . . . . . . 60 3.2.3. Adecuación y completitud para la corrección parcial . . . . . . 68 3.2.4. Correccióntotal.......................... 70 3.2.5. Ejemplos de ternas demostrables: corrección total . . . . . . . 73 7 4. Lógica de Hoare en Isabelle/HOL 77 4.1. Expresiones aritméticas . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.1.1. Simplificación de constantes . . . . . . . . . . . . . . . . . . . 79 4.2. Expresiones booleanas . . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.2.1. Simplificación de constantes . . . . . . . . . . . . . . . . . . . 83 4.3. Sintaxis del lenguaje imperativo simple IMP . . . . . . . . . . . . . . 85 4.4. Semántica operacional del lenguaje imperativo simple IMP . . . . . . 86 4.4.1. Semántica de paso largo . . . . . . . . . . . . . . . . . . . . . 86 4.4.2. Regla de inversión . . . . . . . . . . . . . . . . . . . . . . . . 90 4.4.3. Equivalencia de instrucciones . . . . . . . . . . . . . . . . . . 92 4.4.4. IMP es determinista . . . . . . . . . . . . . . . . . . . . . . . 95 4.4.5. Ejemplos de funciones sobre programas . . . . . . . . . . . . . 96 4.5. Lógica de Hoare en Isabelle/HOL . . . . . . . . . . . . . . . . . . . . 100 4.5.1. Corrección parcial . . . . . . . . . . . . . . . . . . . . . . . . . 100 4.5.2. Ejemplos..............................104 4.5.3. Adecuación y completitud para la corrección parcial . . . . . . 110 4.5.4. Corrección total . . . . . . . . . . . . . . . . . . . . . . . . . . 114 4.5.5. Ejemplos..............................116 4.5.6. Adecuación y completitud para la corrección total . . . . . . . 117 Bibliografía 123 8 Introducción Capítulo 1 Introducción La lógica de Hoare es un sistema formal desarrollado por el científico C.A.R. Hoare en 1969. En esta publicación, Hoare mencionó la ayuda de algunos de los trabajos anteriores de Robert Floyd. La lógica de Hoare se introdujo para poder verificar formalmente programas imperativos, es decir, para razonar sobre la corrección de tales programas. De otra forma, sirve para comprobar y demostrar que realmente un programa realiza las acciones para las que ha sido diseñado. En algunas situaciones esto es de vital importancia, como es el caso de los sistemas de frenado de coches y el pilotaje de aviones por mandos electrónicos. Este propósito lógico especial se obtiene introduciendo un lenguaje que contiene comandos básicos con el que se construyen los programas, el lenguaje determinista IMP, y una formulación con la que poder expresar el comportamiento de los programas. Además, es necesario un conjunto de reglas de cálculo para simplificar expresiones o deducir otras. Nuestro lenguaje estará formado por los siguiente comandos: asignaciones a variables numéricas enteras, condicionales, bucles tipo WHILE y composición secuencial de comandos. El sistema de la lógica de Hoare consiste en un lenguaje formado por ternas de la forma {P}C{Q}, donde Ces un programa, Pes una precondición y Qes una postcondición (ambas escritas en el lenguaje de la lógica matemática). Esta expresión corresponde a la correción parcial del programa Cbajo la precondición Py la postcondición Q. Se dirá que una terna de este tipo es verdadera si se cumple que: si ejecutamos el programa Ca partir de un estado inicial que cumple la precondición P, y, además, el programa Cpara dicho estado inicial termina, entonces, el estado final tras la ejecución de Csatisface la postcondición Q. En estas condiciones si una terna {P}C{Q} es verdadera lo que se puede asegurar acerca del programa es que bajo los estados iniciales para los que se haya ejecutado (que cumplan la precondición), en caso de que termine devuelve el cálculo deseado. Por lo tanto, para asegurarse de que el programa siempre que termine devuelve tal cálculo, habría que computar uno a uno todos los posibles estados que admite la precondición. Puede suceder que el conjunto de estados que cumplan la precondición no sea finito. Es por eso que surge la noción de demostrabilidad. Se construye un sistema deductivo que permite demostrar ternas de Hoare. Una terna de Hoare se dirá demostrable si existe una prueba en la lógica de Hoare de dicha terna. De esta forma queda 9 Introducción a Isabelle/HOL 2.1.5. Listas Una lista se representa escribiendo los elementos entre corchetes y separados por comas. La lista vacía se representa por [] oNil. Además, todos los elementos de una lista tienen que ser del mismo tipo. Una lista de elementos de tipo ’a es la lista Vacía o se obtiene añadiendo, con Cons, un elemento de tipo ’a a una lista de elementos de tipo ’a. El tipo de las listas de elementos del tipo ’a es ’a list. datatype ’a Lista = Vacia | Cons ’a "’a Lista" El término (x#xs) representa la lista obtenida añadiendo el elemento xal principio de la lista xs. Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista vacía los elementos c,byaes [a,b,c]. Dos funciones de descomposición de listas son: (hd xs) es el primer elemento de la lista xs. (tl xs) es el resto de la lista xs. Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es ay el resto de xs es [b,c]. value "let xs = [a,b,c] in hd xs = a ∧tl xs = [b,c]" -- "= True" Otra función de listas es (length xs), que representa la longitud de la lista xs. En “What’s in Main” (página 8) se encuentran más definiciones y propiedades de las listas. 2.1.6. Funciones anónimas En Isabelle pueden definirse funciones anónimas mediante expresiones lambda. Por ejemplo, el valor de la función que a un número le asigna su doble aplicada a 1 es 2. value "(λx. x + x) 1::int" -- "= 2" 2.1.7. Condicionales Isabelle/HOL también es compatible con algunos constructores básicos de la programación funcional, como las expresiones condicionales. Estas expresiones se pueden utilizar para definir funciones. Presentan una de las dos estructuras siguientes: if bthen t1else t2. Aquí bes de tipo bool yt1yt2son del mismo tipo. Veamos un ejemplo: El valor absoluto del entero xes xsi x≥0y es −xen caso contrario. 16 Introducción a Isabelle/HOL definition absoluto :: "int ⇒int" where "absoluto x ≡(if x ≥0 then x else -x)" (case eof c1⇒e1 |c2⇒e2 . . . |cn⇒en) Se evalúa eisi ees de la forma ci. Veamos un ejemplo: Un número natural nes un sucesor si es de la forma (Suc m). definition es_sucesor :: "nat ⇒bool" where "es_sucesor n ≡(case n of 0⇒False | Suc m ⇒True)" 2.1.8. Definiciones recursivas Generalmente, definir una función recursiva es tan simple como en los otros casos. La sintaxis es bastante autoexplicativa: se componen de un conjunto de ecuaciones recursivas. Por ejemplo, la sucesión de Fibonacci: fun fib :: "nat ⇒nat " where "fib 0 = 1" |"fib (Suc 0) = 1" |"fib (Suc(Suc n)) = fib n + fib (Suc n)" 2.2. Razonamiento sobre programas en Isabelle/HOL En esta sección se explica cómo demostrar con Isabelle las propiedades de los programas funcionales mediante algunos ejemplos. 2.2.1. Razonamiento ecuacional Se define la función intercambia tal que (intercambia p) es el par obtenido intercambiando las componentes del par p. fun intercambia :: "’a ×’b ⇒’b ×’a" where "intercambia (x,y) = (y,x)" Se puede probar el siguiente resultado. Proposición 2.2.1 Si se aplica dos veces la función intercambia al par pno se produce ningún cambio. Es decir, intercambia (intercambia (x,y)) = (x,y). 17 Introducción a Isabelle/HOL •La demostración detallada es: lemma "intercambia (intercambia (x,y)) = (x,y)" proof - have "intercambia (intercambia (x,y)) = intercambia (y,x)" by (simp only: intercambia.simps) also have "... = (x,y)" by (simp only: intercambia.simps) finally show "intercambia (intercambia (x,y)) = (x,y)" by simp qed En cuanto al lenguaje empleado en la demostración anterior se puede decir que se utiliza proof para iniciar la prueba, -(después de proof) para no usar el método por defecto, have para establecer un paso, by (simp only: intercambia.simps) para indicar que sólo se usa como regla de escritura la correspondiente a la definición de intercambia, also para encadenar pasos ecuacionales, ... para representar la igualdad anterior en un razonamiento ecuacional, finally para indicar el último paso de un razonamiento ecuacional, show para establecer la conclusión. by simp para indicar el método de demostración por simplificación y qed para terminar la prueba. La definición de la función intercambia genera una regla de simplificación. Si escribimos en Isabelle thm intercambia.simps se puede ver que dicha regla es intercambia.simps: intercambia (x,y) = (y,x). Cada lema, también se puede demostrar de forma estructurada, sin explicar cada paso. •La demostración estructurada en este caso es: lemma "intercambia (intercambia (x,y)) = (x,y)" proof - have "intercambia (intercambia (x,y)) = intercambia (y,x)" by simp also have "... = (x,y)" by simp finally show "intercambia (intercambia (x,y)) = (x,y)" by simp qed 18 Introducción a Isabelle/HOL La diferencia entre las dos demostraciones es que en los dos primeros pasos de la segunda no se explicita la regla de simplificación. Por último, las proposiciones también se pueden demostrar automáticamente, sin explicar ninguno de los pasos que se lleve a cabo en la demostración. •La demostración automática de la proposición 2.2.1 es: lemma "intercambia (intercambia (x,y)) = (x,y)" by simp 2.2.2. Razonamiento por inducción sobre los naturales Teorema 2.2.1 (Principio de inducción sobre los naturales) Para demostrar que una determinada propiedad Pes cierta para todos los números naturales basta probar que el 0satisface la propiedad y que si es cierta para n, entonces también lo es para n+1. En Isabelle el principio de inducción sobre los naturales está formalizado en el teorema nat.induct y puede verse con thm nat.induct: JP 0; Vn. P n =⇒P (Suc n)K=⇒P m Veamos un ejemplo de demostración por inducción sobre los naturales. Para ello, primero se define la función suma_impares tal que (suma_impares n) es la suma de los nprimeros números impares. fun suma_impares :: "nat ⇒nat" where "suma_impares 0 = 0" | "suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n" Proposición 2.2.2 La suma de los nprimeros números impares es n2. Es decir, 1 + 3 + ... + (2n−1) = n2 •Demostración de la proposición anterior por inducción y razonamiento ecuacional: lemma "suma_impares n = n * n" proof (induct n) show "suma_impares 0 = 0 * 0" by simp next fix n assume HI: "suma_impares n = n * n" have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp also have ". . . = (2 * (Suc n) - 1) + n * n" using HI by simp also have ". . . = n * n + 2 * n + 1" by simp finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" by simp qed 19 Introducción a Isabelle/HOL •Demostración de la proposición anterior con patrones y razonamiento ecuacional: lemma "suma_impares n = n * n" (is "?P n") proof (induct n) show "?P 0" by simp next fix n assume HI: "?P n" have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp also have ". . . = (2 * (Suc n) - 1) + n * n" using HI by simp also have ". . . = n * n + 2 * n + 1" by simp finally show "?P (Suc n)" by simp qed Comentarios sobre la demostración anterior: Con la expresión "suma_impares n = n * n"(is " ?P n") se abrevia "suma_impares n =n * n" como " ?P n". Por tanto, " ?P 0" es una abreviatura de "suma_impares 0 =0 * 0" y, " ?P (Suc n)" es una abreviatura de "suma_impares (Suc n) =(Suc n) * (Suc n)" En general, cualquier fórmula seguida de (is patrón) equipara el patrón con la fórmula. •La demostración usando patrones es: lemma "suma_impares n = n * n" (is "?P n") proof (induct n) show "?P 0" by simp next fix n assume "?P n" then show "?P (Suc n)" by simp qed •La demostración automática es: lemma "suma_impares n = n * n" by (induct n) auto El método auto es un poco más fuerte que simp. Este método combina el razonamiento clásico con el de simplificación. La diferencia entre auto y los demás es que intenta llevar a cabo todos los subobjetivos de la demostración, por lo que, desafortunadamente, puede producir un gran número de nuevos subobjetivos. 20 Introducción a Isabelle/HOL Veamos ahora, un ejemplo de definición con cuantificadores o existenciales. Podemos decir, que un número natural nes par si existe un natural mtal que n=m+m. Por lo tanto, definir la función par tal que (par n) devuelve, en caso de existir, la mitad de n. definition par :: "nat ⇒bool" where "par n ≡ ∃m. n=m+m" Esta definición puede verse con thm par_def. La siguiente proposición se demuestra mediante inducción y existenciales: Proposición 2.2.3 Para todo número natural n, se verifica que n(n+ 1) es par. •Demostración detallada por inducción: lemma fixes n :: "nat" shows "par (n*(n+1))" proof (induct n) show "par (0*(0+1))" by (simp add: par_def) next fix n assume "par (n*(n+1))" then have "∃m. n*(n+1) = m+m" by (simp add:par_def) then obtain m where m: "n*(n+1) = m+m" .. then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto then have "∃m. (Suc n)*((Suc n)+1) = m+m" .. then show "par ((Suc n)*((Suc n)+1))" by (simp add:par_def) qed Comentarios sobre la demostración: La declaración (fixes n :: "nat") es una abreviatura de “sea n un número natural”. En Isabelle puede demostrarse de manera más simple un lema equivalente usando en lugar de la función par la función even definida en la teoría Parity por even x ←→ x mod 2 = 0 lemma fixes n :: "nat" shows "even (n*(n+1))" by auto 21 Introducción a Isabelle/HOL Comentarios sobre la demostración anterior: Para poder usar la función even de la librería Parity es necesario importar dicha librería. Por ello, antes del inicio de la teoría aparece imports Main Parity. Para completar la demostración basta demostrar la equivalencia de las funciones par yeven. lemma fixes n :: "nat" shows "par n = even n" proof - have "par n = (∃m. n = m+m)" by (simp add:par_def) then show "par n = even n" by presburger qed Comentarios sobre la demostración anterior: by presburger indica que se use como método de demostración el algoritmo de decisión de la aritmética de Presburger, implementado en Isabelle. 2.2.3. Razonamiento por inducción sobre listas En Isabelle puede hacerse inducción estructural sobre cualquier tipo recursivo. La inducción matemática es la inducción sobre los naturales. Este apartado se centra en la inducción sobre listas. Para demostrar una propiedad para todas las listas basta demostrar que la lista vacía tiene la propiedad y que al añadir un elemento a una lista que tiene la propiedad se obtiene otra lista que también tiene la propiedad. En Isabelle el principio de inducción sobre listas está formalizado mediante el teorema list.induct JP []; Vx xs. P xs =⇒P (x#xs)K=⇒P xs A continuación se muestra un ejemplo. Se define la función conc tal que (conc xs ys) es la concatención de las listas xs eys. fun conc :: "’a list ⇒’a list ⇒’a list" where "conc [] ys = ys" | "conc (x#xs) ys = x # (conc xs ys)" A partir de la definición anterior se puede demostrar la proposición siguiente. 22 Introducción a Isabelle/HOL Proposición 2.2.4 Dadas dos listas cualesquiera, xs eys, siempre se verifica que conc xs (conc ys zs) =(conc xs ys) zs. •La demostración estructurada es: lemma "conc xs (conc ys zs) = conc (conc xs ys) zs" proof (induct xs) show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp next fix x xs assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp also have "... = x # (conc (conc xs ys) zs)" using HI by simp also have "... = conc (conc (x # xs) ys) zs" by simp finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" by simp qed Comentarios sobre la demostración anterior: (induct xs) genera dos subobjetivos: 1. conc [] (conc ys zs) =conc (conc [] ys) zs 2. Va xs. conc xs (conc ys zs) =conc (conc xs ys) zs =⇒conc (a#xs) (conc ys zs) =conc (conc (a#xs) ys) zs •La demostración automática de 2.2.4 es: lemma "conc xs (conc ys zs) = conc (conc xs ys) zs" by (induct xs) auto En Isabelle también se pueden refutar resultados, generándose un contraejemplo mediante Quickcheck oNitpick. En este caso, en relación con la función conc se puede refutar que conc xs ys =conc ys xs. lemma "conc xs ys = conc ys xs" quickcheck oops El contraejemplo que Isabelle encuentra es xs = [a2] ys = [a1] 23 Introducción a Isabelle/HOL 2.2.4. Inducción correspondiente a la definición recursiva Se define la función coge tal que (coge n xs) es la lista de los nprimeros elementos de xs. fun coge :: "nat ⇒’a list ⇒’a list" where "coge n [] = []" | "coge 0 xs = []" | "coge (Suc n) (x#xs) = x # (coge n xs)" Por otro lado, se define la función elimina tal que (elimina n xs) es la lista obtenida eliminando los nprimeros elementos de xs. fun elimina :: "nat ⇒’a list ⇒’a list" where "elimina n [] = []" | "elimina 0 xs = xs" | "elimina (Suc n) (x#xs) = elimina n xs" La definición coge genera de forma automática el esquema de inducción coge.induct: JVn. P n []; Vx xs. P 0 (x#xs); Vn x xs. P n xs =⇒P (Suc n) (x#xs)K =⇒P n x Este esquema puede verse usando thm coge.induct. Proposición 2.2.5 Dada una lista cualquiera xs, siempre se verifica que conc (coge n xs) (elimina n xs) = xs. •La demostración estructurada es lemma "conc (coge n xs) (elimina n xs) = xs" proof (induct rule: coge.induct) fix n show "conc (coge n []) (elimina n []) = []" by simp next fix x xs show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" by simp next fix n x xs assume HI: "conc (coge n xs) (elimina n xs) = xs" have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = conc (x#(coge n xs)) (elimina n xs)" by simp also have "... = x#(conc (coge n xs) (elimina n xs))" by simp also have "... = x#xs" using HI by simp finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs" by simp qed 24 Introducción a Isabelle/HOL Comentarios sobre la demostración anterior: (induct rule: coge.induct) indica que el método de demostración es por el esquema de inducción correspondiente a la definición de la función coge. Se generan 3subobjetivos: 1. Vn. conc (coge n []) (elimina n []) =[] 2. Vx xs. conc (coge 0(x#xs)) (elimina 0(x#xs)) =x#xs 3. Vn x xs.conc (coge n xs) (elimina n xs) =xs =⇒ conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) =x#xs •La demostración automática es lemma "conc (coge n xs) (elimina n xs) = xs" by (induct rule: coge.induct) auto 2.2.5. Razonamiento por distinción de casos Distinción de casos booleanos Ejemplo de demostración por distinción de casos booleanos: Demostrar ¬A∨A. •La demostración estructurada es lemma "¬A∨A" proof cases assume "A" then show "¬A∨A" .. next assume "¬A" then show "¬A∨A" .. qed Comentarios de la demostración anterior: proof cases indica que el método de demostración será por distinción de casos. Se generan 2casos: 1. ?P =⇒ ¬ A∨A 2. ¬?P =⇒ ¬ A∨A donde ?P es una variable sobre las fórmulas. (assume " A") indica que se está usando Aen lugar de la variable ?P. 25 Introducción a Isabelle/HOL 4. =⇒arbol bosque. Japlana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol); aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)K =⇒aplana_bosque (map_bosque (ConsB arbol bosque) h) = map h (aplana_bosque (ConsB arbol bosque)) •La demostración automática es lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" by (induct_tac a and b) auto 2.3. Definiciones inductivas en Isabelle/HOL 2.3.1. El conjunto de los números pares El conjunto de los números pares se puede definir inductivamente como el menor conjunto que contiene al 0y es cerrado por la operación +2. El conjunto de los números pares también puede definirse como los naturales divisibles por 2. Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo se demuestra su equivalencia. Definición inductiva del conjuntos de los pares Mediante el comando inductive_set se declara la constante par como un conjunto de números naturales con unas determinadas propiedades deseadas. Una definición inductiva está formada por reglas de introducción. inductive_set par :: "nat set" where cero [intro!]: "0 ∈par" | paso [intro!]: "n ∈par =⇒(Suc (Suc n)) ∈par" Esta definición inductiva genera varios teoremas. Estos teoremas incluyen las reglas de introducción especificadas en la declaración, una regla de eliminación para el análisis por casos y una regla de inducción. Reglas de introducción par.cero: 0∈par par.paso: n∈par =⇒Suc (Suc n) ∈par par.simps: (a ∈par) =(a =0∨(∃n. a =Suc (Suc n) ∧n∈par)) Regla de eliminación (reglas que pueden usarse como reglas de eliminación) 32 Introducción a Isabelle/HOL ?a ∈par =⇒(?a = 0 =⇒?P) =⇒ (Vn. ?a = Suc (Suc n) =⇒n∈par =⇒?P) =⇒?P Regla de inducción par.induct: Jx∈par; P 0; Vn. Jn∈par; P nK=⇒P (Suc (Suc n))K =⇒P x Uso de las reglas de introducción Este primer lema afirma que los números de la forma 2k, siendo k∈N, son pares. Proposición 2.3.1 Los números de la forma 2kson pares. •La demostración estructurada es lemma dobles_son_pares_2: "2*k ∈par" proof (induct k) show "2 * 0 ∈par" by auto next show "Vk. 2 * k ∈par =⇒2 * Suc k ∈par" by auto qed •La demostración automática es lemma dobles_son_pares [intro!]: "2*k ∈par" by (induct k) auto Nuestro objetivo es demostrar la equivalencia de la definición anterior y la definición mediante divisibilidad. Uno de los sentidos de esta equivalencia es inmediato por el lema que se acaba de probar, ya que el comando intro! asegura que el lema se aplica automáticamente. Proposición 2.3.2 Si nes divisible por 2, entonces es par. thm dvd_def lemma dvd_imp_par: "2 dvd n =⇒n∈par" by (auto simp add: dvd_def) 33 Introducción a Isabelle/HOL Regla de inducción Entre las reglas generadas por la definión par está la regla de inducción siguiente: par.induct: Jx∈par; P 0; Vn. Jn∈par; P nK=⇒P (Suc (Suc n))K =⇒P x Una propiedad Pse cumple para todos los números pares siempre que el 0tenga la propiedad y sea cerrada para la operación Suc (Suc ·). De esta forma, Pes cerrada bajo las reglas de introducción de par, que es el menor conjunto cerrado bajo estas reglas. A este razonamiento inductivo se le llama regla de inducción. La inducción es una forma habitual de demostrar que todos los elementos de un conjunto satisfacen una determinada propiedad. A continuación, se prueba por inducción la otra implicación de la equivalencia anterior, es decir, que todos los números pares son múltiplos de 2. Proposición 2.3.3 Los números pares son divisibles por 2. •La demostración detallada es: lemma par_imp_dvd: "n ∈par =⇒2 dvd n" proof (induction rule: par.induct) show "2 dvd (0::nat)" by simp (*(simp add: dvd_def)*) next fix n::nat assume H1: "n ∈par" and H2: "2 dvd n" have "∃k. n = 2*k" using H2 by (simp add: dvd_def) then obtain k where "n = 2*k" .. hence "Suc (Suc n) = 2*(k+1)" by arith hence "∃k. Suc (Suc n) = 2*k" .. thus "2 dvd Suc (Suc n)" by (simp add: dvd_def) qed El método arith trata de probar el primer subobjetivo siempre y cuando sea una fórmula aritmética lineal. Dichas fórmulas pueden incluir los conectores lógicos habituales (¬,∧,∨,−→,∃,∀), las relaciones, =,≤, y <, y las operaciones +,−,min ymax. •La demostración con arith es: lemma par_imp_dvd_2: "n ∈par =⇒2 dvd n" proof (induction rule: par.induct) show "2 dvd (0::nat)" by simp (* (simp_all add: dvd_def)*) next 34 Introducción a Isabelle/HOL fix n::nat assume H1: "n ∈par" and H2: "2 dvd n" thus "2 dvd Suc (Suc n)" by (auto simp add: dvd_def, arith) qed •La demostración automática es: lemma par_imp_dvd_3: "n ∈par =⇒2 dvd n" by (induction rule:par.induct) (auto simp add: dvd_def, arith) Si se combinan las dos proposiciones previas, se demuestra la equivalencia deseada: Proposición 2.3.4 Un número nes par ⇔es divisible por 2. theorem par_iff_dvd: "(n ∈par) = (2 dvd n)" by (auto simp add: dvd_imp_par par_imp_dvd) o bien by (blast intro: dvd_imp_par par_imp_dvd) El método blast es la herramienta principal que tiene Isabelle para probar teoremas de forma automática, además de ser el más rápido. Este método es aún más fuerte que auto. También es efectivo para teoría de conjuntos. Mientras que el método blast podría simplemente fallar, el método clarify nos muestra un subobjetivo que nos puede ayudar a entender porqué no se puede continuar con la prueba. Uso de la regla de eliminación Antes de aplicar inducción con frecuencia es conveniente generalizar la fórmula a probar. Vamos a ilustrar el principio anterior en el caso de los conjuntos inductivamente definidos, con el siguiente ejemplo: Proposición 2.3.5 Si n+ 2 es par, entonces ntambién lo es. El siguiente intento falla: lemma "Suc (Suc n) ∈par =⇒n∈par" apply (erule par.induct) oops En el intento anterior, los subobjetivos generados son: 1. n∈par, 35 Introducción a Isabelle/HOL 2. Vna. Jna ∈par; n ∈parK=⇒n∈par, que no se pueden demostrar. Se ha perdido la información sobre Suc (Suc n). En ese caso, se reformula el lema a demostrar. En el ejemplo que estamos tratando, la reformulación es: Proposición 2.3.6 Si nes par, entonces n−2también lo es. •La demostración estructurada es: lemma par_imp_par_menos_2: "n ∈par =⇒n - 2 ∈par" proof (induction rule:par.induct) show "0 - 2 ∈par" by auto next show "Vn. Jn∈par; n - 2 ∈parK=⇒Suc (Suc n) - 2 ∈par" by simp qed •La demostración automática es: lemma par_imp_par_menos_2: "n ∈par =⇒n - 2 ∈par" by (induction rule:par.induct) auto Utilizando este último lema se puede demostrar el lema original 2.3.5. •La demostración estructurada es: lemma assumes "Suc (Suc n) ∈par" shows "n ∈par" proof - have "Suc (Suc n) - 2 ∈par" using assms by (rule par_imp_par_menos_2) thus "n ∈par" by simp qed •La demostración aplicativa, usando el lema 2.3.6 como regla de destrucción para razonar hacia delante, es: lemma "Suc (Suc n) ∈par =⇒n∈par" apply (drule par_imp_par_menos_2) (* o bien con frule *) apply (simp) done •La demostración automática es: lemma Suc_Suc_par_imp_par: "Suc (Suc n) ∈par =⇒n∈par" by (drule par_imp_par_menos_2, simp) 36 Introducción a Isabelle/HOL A partir de los dos lemas 2.3.5 y 2.3.6, se puede demostrar la equivalencia siguiente. Proposición 2.3.7 Un número natural nes par ⇔n+ 2 es par. lemma [iff]: "((Suc (Suc n)) ∈par) = (n ∈par)" by (auto simp add: Suc_Suc_par_imp_par) o bien by (auto dest: Suc_Suc_par_imp_par) o con blast. Comentario sobre la demostración anterior: Se usa el atributo iff porque sirve como regla de simplificación. Definiciones mutuamente inductivas Existen conjuntos definidos mediante inducción mutua. Por ejemplo, la definición cruzada de los conjuntos inductivos de los pares y de los impares es: inductive_set Pares :: "nat set" and Impares :: "nat set" where ceroP: "0 ∈Pares" | ParesI: "n ∈Impares =⇒Suc n ∈Pares" | ImparesI: "n ∈Pares =⇒Suc n ∈Impares" El esquema de inducción generado por la definición anterior es Pares_Impares.induct: JP1 0; Vn. Jn∈Impares; P2 nK=⇒P1 (Suc n); Vn. Jn∈Pares; P1 nK=⇒P2 (Suc n)K =⇒(x1 ∈Pares −→ P1 x1) ∧(x2 ∈Impares −→ P2 x2) Ejemplo de demostración usando el esquema anterior. lemma "(m ∈Pares −→ 2 dvd m) ∧(n ∈Impares −→ 2 dvd (Suc n))" proof (induction rule:Pares_Impares.induct) show "2 dvd (0::nat)" by simp next fix n :: "nat" assume H1: "n ∈Impares" and H2: "2 dvd Suc n" show "2 dvd Suc n" using H2 by simp next fix n :: "nat" 37 Introducción a Isabelle/HOL assume H1: "n ∈Pares" and H2: "2 dvd n" have "∃k. n = 2*k" using H2 by (simp add: dvd_def) then obtain k where "n = 2*k" .. hence "Suc (Suc n) = 2*(k+1)" by simp hence "∃k. Suc (Suc n) = 2*k" .. thus "2 dvd Suc (Suc n)" by (simp add: dvd_def) qed Definición inductiva de predicados En lugar de definir un conjunto de números con unas determinadas propiedades también se puede construir un predicado sobre los naturales. Definición inductiva del predicado es_par tal que (es_par n) se verifica si nes par. inductive es_par :: "nat ⇒bool" where "es_par 0" | "es_par n =⇒es_par(Suc(Suc n))" Heurística para elegir entre definir conjuntos o predicados: si se va a combinar con operaciones conjuntistas, definir conjunto; en caso contrario, definir predicado. 2.3.2. Clausura reflexiva transitiva Isabelle admite la definición de funciones de orden superior, es decir, cuyos argumentos sean otras funciones o predicados. Definición 2.3.1 La clausura reflexiva y transitiva de una relación res la menor relación reflexiva y transitiva que contiene a r. Se representa por r∗. Esta relación r∗se puede definir inductivamente, como conjunto: (x, x)∈r∗ Si (x, y)∈re(y, z)∈r∗, entonces (x, z)∈r∗. La definición inductiva, como conjunto, se puede expresar en Isabelle/HOL como sigue: inductive_set crt :: "(’a ×’a) set ⇒(’a ×’a) set" ("_*" [1000] 999) for r :: "(’a ×’a) set" where crt_refl [iff]: "(x,x) ∈r*" | crt_paso: "J(x,y) ∈r; (y,z) ∈r* K=⇒(x,z) ∈r*" 38 Introducción a Isabelle/HOL Comentarios sobre la definición anterior: La sintaxis concreta permite escribir r* en lugar de crt r. La definición consta de dos reglas. A la regla reflexiva se le añade el atributo iff para aumentar la automatización. A la regla del paso no se le añade ningún atributo, porque r* ocurre en la izquierda. En el resto de esta sección se demuestra que esta definición coincide con la menor relación reflexiva y transitiva que contiene a r. Teoremas que se han generado sólamente con la definición, cuando se ha construido: thm crt.induct thm crt_paso thm crt_refl thm crt.intros thm crt.induct hay que estudiarlo en detalle porque es el que luego se utiliza para demostraciones. Proposición 2.3.8 La relación r∗es reflexiva. lemma "(x,x) ∈r*" by simp (* o con "by (rule crt_refl)"*) Proposición 2.3.9 La relación r∗contiene a r. lemma [intro]: "(x,y) ∈r=⇒(x,y) ∈r*" by (blast intro: crt_paso) (*o bien con "auto"*) Comentarios sobre la demostración anterior: La ventaja del lema es que se puede declarar como regla de introducción, porque r* ocurre sólo en la derecha. Con la declaración, algunas demostraciones que usan crt_paso se hacen de manera automática. El esquema de inducción de la clausura reflexiva transitiva es crt.induct: J(x1, x2) ∈r*; Vx. P x x; Vx y z. J(x,y) ∈r; (y,z) ∈r*; P y zK=⇒P x zK =⇒P x1 x2 Proposición 2.3.10 La relación r∗es transitiva. 39 Introducción a Isabelle/HOL •La demostración automática es: lemma crt_trans_auto: "J(x,y) ∈r*; (y,z) ∈r* K=⇒(x,z) ∈r*" by (induction rule:crt.induct) (auto simp add:crt_paso) •La demostración aplicativa es: lemma crt_trans_apply: "J(x,y) ∈r*; (y,z) ∈r* K=⇒(x,z) ∈r*" apply (induction rule:crt.induct) apply (auto simp add:crt_paso) done La relación r∗está contenida en cualquier relación reflexiva y transitiva que contenga a r. Mediante crt2 r se define la menor relación reflexiva y transitiva que contiene ar. inductive_set crt2 :: "(’a ×’a)set ⇒(’a ×’a)set" for r :: "(’a ×’a)set" where "(x,y) ∈r=⇒(x,y) ∈crt2 r" (* contiene a r *) | "(x,x) ∈crt2 r" (* reflexiva *) | "J(x,y) ∈crt2 r; (y,z) ∈crt2 r K=⇒(x,z) ∈crt2 r" (* transitiva *) A continuación probamos que r* coincide con crt2 r. Proposición 2.3.11 La relación crt2 r está contenida en r*. lemma "(x,y) ∈crt2 r =⇒(x,y) ∈r*" proof (induction rule: crt2.induct) fix x y assume "(x,y) ∈r" thus "(x,y) ∈r*" by blast next fix x show "(x,x) ∈r*" by blast next fix x y z assume H1: "(x,y) ∈crt2 r" and H2: "(x,y) ∈r*" and H3: "(y,z) ∈crt2 r" and H4: "(y,z) ∈r*" show "(x,z) ∈r*" using H2 H4 by (rule crt_trans) qed 40 Introducción a Isabelle/HOL Proposición 2.3.12 La relación r* está contenida en crt2 r. lemma "(x,y) ∈r* =⇒(x,y) ∈crt2 r" proof (induction rule:crt.induct) fix x show "(x,x) ∈crt2 r" by (rule crt2.intros(2)) next fix x y z assume H1: "(x,y) ∈r" and H2: "(y,z) ∈r*" and H3: "(y,z) ∈crt2 r" have "(x,y) ∈crt2 r" using H1 by (rule crt2.intros(1)) thus "(x,z) ∈crt2 r" using H3 by (rule crt2.intros(3)) qed 41 Lógica de Hoare A continuación se muestran ejemplos de programas completos. Dichos ejemplos ponen de manifiesto la potencia del lenguaje de programación descrito a pesar de su aparente simplicidad. De hecho, puede demostrarse que el lenguaje WHILE aquí descrito constituye un modelo de computación universal, tan potente como el modelo de las máquinas de Turing o cualquier otro modelo de computación clásico. Ejemplo 1: C1=   Y:=1; R:=0; WHILE R6=X DO (R:=R+1; Y:=Y*R) Computación del programa C1a partir del estado inicial {X=3}. Paso 0. {X=3,Y=y,R=r} Paso 1. {X=3,Y=1,R=r} Paso 2. {X=3,Y=1,R=0} Paso 3. {X=3,Y=1,R=1} Paso 4. {X=3,Y=1,R=1} Paso 5. {X=3,Y=1,R=2} Paso 6. {X=3,Y=2,R=2} Paso 7. {X=3,Y=2,R=3} Paso 8. {X=3,Y=6,R=3} El programa anterior calcula el factorial de X, en caso de que sea un entero no negativo, en la variable de salida Y. Si el valor inicial de Xes negativo, el programa anterior no para. Ejemplo 2: C2=   R:=X; Q:=0; WHILE Y ≤R DO (R:=R-Y; Q:=Q+1) Computación del programa C2a partir del estado inicial {X=7,Y=2}. Paso 0. {X=7,Y=2,R=r,Q=q} Paso 1. {X=7,Y=2,R=7,Q=q} 48 Lógica de Hoare Paso 2. {X=7,Y=2,R=7,Q=0} Paso 3. {X=7,Y=2,R=5,Q=0} Paso 4. {X=7,Y=2,R=5,Q=1} Paso 5. {X=7,Y=2,R=3,Q=1} Paso 6. {X=7,Y=2,R=3,Q=2} Paso 7. {X=7,Y=2,R=1,Q=2} Paso 8. {X=7,Y=2,R=1,Q=3} Este programa calcula la división euclídea entre XeY, números enteros positivos, siendo QyRel cociente y el resto, respectivamente. Ejemplo 3: C3=       Y:=X; Z:=1; R:=1; WHILE 1<Y DO (R:=R+Z; Z:=R-Z; Y:=Y-1) Computación de C3a partir del estado inicial {X=3}. Paso 0. {X=3,Y=y,Z=z,R=r} Paso 1. {X=3,Y=3,Z=z,R=r} Paso 2. {X=3,Y=3,Z=1,R=r} Paso 3. {X=3,Y=3,Z=1,R=1} Paso 4. {X=3,Y=3,Z=1,R=2} Paso 5. {X=3,Y=3,Z=1,R=2} Paso 6. {X=3,Y=2,Z=1,R=2} Paso 7. {X=3,Y=2,Z=1,R=3} Paso 8. {X=3,Y=2,Z=2,R=3} Paso 9. {X=3,Y=1,Z=2,R=3} 49 Lógica de Hoare Este programa calcula el valor del número que está en la posición X-ésima en la sucesión de Fibonacci, y lo devuelve en la variable Z. 3.1.2. Notación de Hoare C.A.R. Hoare introdujo la siguiente notación para describir formalmente el comportamiento esperado de un programa {P}C{Q} donde: Pes una condición que se denomina precondición. Qes una condición que se denomina postcondición. Ces un programa imperativo cuyo lenguaje se ha descrito anteriormente. Diremos que la terna de Hoare {P}C{Q}es verdadera, y lo denotaremos por |={P}C{Q}, cuando se cumple que: si ejecutamos el programa Ca partir de un estado inicial que cumple la precondición P, y, además, el programa Cpara dicho estado inicial termina, entonces, el estado final tras la ejecución de Csatisface la postcondición Q. La expresión {P}C{Q}corresponde a la corrección parcial del programa ya que si el programa para, ha de cumplirse la postcondición Q; si no para, no hay nada que comprobar ni refutar. La corrección total es otro tipo de corrección más fuerte que la parcial. Se denota por [P]C[Q] Diremos que dicha terna es verdadera, y lo escribiremos como |=[P]C[Q], si se cumple que: si ejecutamos el programa Ca partir de un estado inicial que cumple la precondición P, entonces el programa Ctermina para dicho estado inicial y, además, el estado final tras la ejecución de Csatisface la postcondición Q. 50 Lógica de Hoare La relación que existe entre ambos tipos de corrección se puede expresar informalmente por la ecuación Corrección total =Corrección parcial +Terminación Para demostrar la corrección total de un programa se suele probar de forma separada, por una parte, la corrección parcial y, por otra, la terminación. La corrección total es lo que nos interesa en definitiva. La terminación es, normalmente, fácil de establecer, aunque existen algunos casos en los que no, como la conjetura de Collatz. 3.1.3. Algunos ejemplos A continuación se muestran algunos ejemplos de ternas verdaderas y falsas, con respecto a la corrección parcial o total. •{P}C{T} Es verdadera para cualquier precondición Py cualquier programa C, ya que la postcondición {T} es, por definición, siempre verdadera. •{T} C{T} Esta terna es verdadera trivialmente, es un caso particular del ejemplo anterior tomando P=T. •[T] C[T] Esta terna es verdadera siempre que la computación de Ctermine a partir de cualquier estado inicial. •{X=1} X:=X+1 {X=2}. Esta terna es verdadera, ya que si se toma el estado inicial {X=1} que cumple la precondición y se ejecuta el programa, se obtiene el estado final {X=2}, como indica la postcondición. •{X=x,Y=y} X:=Y; Y:=X {X=y,Y=x}. Paso 0. {X=x,Y=y} Paso 1. {X=y,Y=y} Paso 2. {X=y,Y=y} 51 Lógica de Hoare Esta terna es falsa (a menos que x=y), pues las variables XeYno intercambian sus valores, como se muestra en la computación anterior. •{X=x,Y=y} R:=X; X:=Y; Y:=R {X=y,Y=x}. Paso 0. {X=x,Y=y,R:=r} Paso 1. {X=x,Y=y,R:=x} Paso 2. {X=y,Y=y,R:=x} Paso 3. {X=y,Y=x,R:=x} Esta terna de Hoare es verdadera, las variables XeYintercambian sus valores. •{X=1} WHILE X6=0 DO X:=X {1=2} Esta terna es verdadera a pesar de que la postcondición es contradictoria, pues se trata de corrección parcial y el programa sobre {X=1} no para. •[X=1] WHILE X6=0 DO X:=X [1=2] Esta terna de Hoare falsa, porque el programa sobre {X=1} no para y ahora estamos considerando corrección total en lugar de parcial. •{T} WHILE X6=0 DO X:=X {F} Esta terna de Hoare es falsa, porque el programa termina para el estado inicial {X=0} que satisface trivialmente la precondición y la postcondición es, por definición, siempre falsa. •Sea la siguiente terna de Hoare {T} C4=   R:=X; Q:=0; WHILE Y ≤R DO (R=R-Y; Q=Q+1) {R<Y ∧X=R+(Y*Q)}. Dicha terna será verdadera si, para cualesquiera valores iniciales de XeY, si la ejecución del programa C4termina, entonces Qguarda el cociente de dividir Xentre YyRguarda el resto. 52 Lógica de Hoare •Sea la terna de Hoare [0≤X∧0<Y] C4[R<Y ∧X=R+(Y*Q)], donde C4es el programa del ejemplo anterior. Puesto que ahora estamos usando correción total, esta terna será verdadera si, para cualesquiera valores iniciales X≥0eY > 0, podemos asegurar que el programa C4para y, además, en el estado final se cumple que la variable Qguarda el cociente de dividir Xentre YyRguarda el resto. •Sea la terna de Hoare {T} C5=   Y:=1; R:=0; WHILE R6=X DO (R:=R+1; Y:=Y*R) {Y=fact(X)} La terna anterior es verdadera, ya que en caso de que C5termine se satisface la postcondición. Ahora bien, si en el estado inicial la variable Xcontiene un valor entero negativo, el programa anterior no para. Por tanto, la terna [T] C5[Y=fact(X)] es, en cambio, falsa. 3.2. Lógica de Hoare En la sección anterior se introdujeron tres tipos de expresiones que podían ser verdaderas o falsas: 1. Corrección parcial de una terna de Hoare. 2. Corrección total de una terna de Hoare. 3. Declaraciones matemáticas, esto es, fórmulas de un lenguaje de primer orden. Es bien conocido que las declaraciones matemáticas pueden demostrarse mediante axiomas yreglas de inferencia usando un cálculo de tipo Hilbert para la lógica de primer orden. Una prueba en dicho cálculo es una sucesión finita de fórmulas en la cual cada fórmula o bien es un axioma o bien puede deducirse de fórmulas anteriores en la sucesión aplicando una regla de inferencia. La última línea muestra la conclusión de la prueba, la declaración que se quería obtener. Esto es, una fórmula Pse dirá demostrable si existe una prueba tal que la última fórmula de la prueba es, precisamente, P. 53 Lógica de Hoare El objetivo de esta sección es presentar un cálculo similar que permita establecer la correción parcial de un programa imperativo. Para ello será necesario presentar una serie de axiomas y reglas de inferencia que traten tanto con declaraciones matemáticas (fórmulas de primer orden) como con ternas de Hoare. Dichos axiomas y reglas vendrán proporcionados por el sistema lógico conocido como la lógica de Hoare o lógica de Floyd-Hoare (la formulación del sistema deductivo de debe a Hoare, aunque algunas de las ideas subyacentes pertenecen a Floyd). De manera análoga al caso de la lógica de primer orden, una demostración o una prueba en la lógica de Hoare será una sucesión finita, donde pueden aparecer tanto ternas de Hoare como fórmulas de primer orden, y tal que cada elemento de la sucesión o bien es un axioma de la lógica de Hoare o bien puede obtenerse a partir de elementos anteriores de la sucesión mediante la aplicación de reglas de inferencia. Una terna de Hoare {P}C{Q}se dirá demostrable, y lo escribiremos ` {P}C{Q}, si existe una prueba en la lógica de Hoare cuyo último elemento es, precisamente, dicha terna. La lógica de Hoare proporciona un marco teórico para desarrollar la verificación formal de programas imperativos. Las pruebas de corrección sobre programas suelen ser complejas y normalmente se necesitan métodos formales para asegurar que son válidas. Por ello es importante que se muestren explícitamente los principios de razonamiento que se utilicen, con el fin de que se pueda analizar la robustez. Nótese que en algunas situaciones la corrección de un sistema informático es muy importante o incluso crítica. Considérese el caso, por ejemplo, de los sistemas de los que depende la vida humana, como los controladores de reactores nucleares, los sistemas de frenado de coches, pilotaje de aviones por mandos electrónicos o equipos médicos controlados por software. A continuación, se explica y se muestra con ejemplos el sistema deductivo de Hoare para el razonamiento sobre programas imperativos. 3.2.1. Axiomas y reglas de la lógica de Hoare En este apartado, se describen los axiomas y reglas de inferencia de la lógica de Hoare. Expresaremos dichas reglas mediante el siguiente esquema `S1,...,`Sn `S Esto es, a partir de las hipótesis `S1,...,`Snse deduce la conclusión `S. Estas hipótesis pueden ser ternas de Hoare o una mezcla entre ternas de Hoare y declaraciones matemáticas (esto es, fórmulas de primer orden). 54 Lógica de Hoare Axiomas del dominio En primer lugar, es necesario disponer de un conjunto de axiomas que capturen las propiedades matemáticas del dominio subyacente sobre el cual interpretaremos nuestros programas imperativos. En nuestro caso, fijaremos un lenguaje de primer orden con igualdad adecuado para expresar propiedades de los números enteros y que contenga, al menos, la suma y el producto como operaciones básicas; y añadiremos como un axioma de la lógica de Hoare cada propiedad de primer orden que sea verdadera en la estructura estándar de los números enteros (Z,+,×, . . . ). Axiomas del dominio `P para cualquier fórmula Pverdadera en la estructura Z. Cuando en una prueba en la lógica de Hoare empleemos un axioma del dominio, usualmente escribiremos como justificación de dicho paso de la prueba por lógica o por aritmética. Axioma de asignación El axioma de asignación representa el hecho de que el valor de una variable V después de ejecutar el comando de asignación V:= Ees igual al valor de la expresión Een el estado antes de ejecutarlo. Por tanto, cualquier propiedad Pque se verificara antes de la asignación para la expresión Etambién ha de verificarse después de la asignación para la variable V. Formalmente, escribimos P[E/V ]para expresar el resultado de reemplazar todas las ocurrencias de la variable Ven la fórmula Ppor la expresión E. Axioma de asignación ` {P[E/V ]}V:= E{P} donde Ves una variable, Ees una expresión, Pes una condición y la notación P[E/V ]denota el resultado de sustituir todas las ocurrencias de Vpor el término Een P. Ejemplos: Las siguientes ternas de Hoare son demostrables por ser una instancia de un axioma de asignación. `{X+1=n+1} X:=X+1 {X=n+1}. 55 Lógica de Hoare `{X+1=2} X:=X+1 {X=2}. `{Y=2} X:=2 {Y=X}. `{E=E} X:=E {X=E}. Puede llamar la atención que la aplicación del axioma de asignación sea hacia atrás. Sin embargo, la intuición nos puede llevar a cometer alguno de los dos errores siguientes en cuanto a la expresión de este axioma si intentamos aplicar el axioma hacia adelante. 1. ` {P}V:= E{P[V/E]}. Donde la notación P[V/E]denota el resultado de sustituir Epor Ven P. Esta formulación del axioma nos llevaría a obtener incongruencias. Por ejemplo, tomemos P=(x=0),V=x, y E= 1. Entonces, se obtendría `{x=0} x:=1 {x=0}, que claramente se trata de una terna de Hoare falsa. Nótese que (x=0)[x/1] es igual a (x=0), ya que 1no ocurre en (x=0). 2. ` {P}V:= E{P[E/V ]}. Esta formulación de axioma también nos llevaría a conclusiones erróneas. Por ejemplo, tomemos de nuevo P=(x=0),V=x, y E= 1. Entonces se obtendría `{x=0} x:=1 {1=0}, que claramente se trata de una terna de Hoare falsa. Reforzamiento de la precondición Reforzamiento de la precondición `P⇒P0,` {P0}C{Q} ` {P}C{Q} Si a partir de la condición Pse tiene P0, y la terna de Hoare {P0}C{Q} es demostrable, se tiene que esta otra {P}C{Q} también es demostrable, cuya precondición Pes más restrictiva que la de la terna anterior. Ejemplo: Probar `{X=n} X:=X+1 {X=n+1}. Paso 0. `{X+1=n+1} X:=X+1 {X=n+1}. (Axioma de asignación) Paso 1. `X=n ⇒X+1=n+1. (Aritmética) Paso 2. `{X=n} X:=X+1 {X=n+1}. (Reforzamiento de la precondición 0,1)  56 Lógica de Hoare Debilitamiento de la postcondición Debilitamiento de la postcondición ` {P}C{Q0},`Q0⇒Q ` {P}C{Q} Esto es, si la terna de Hoare {P}C{Q0} es demostrable y a partir de su postcondición Q0se deduce Q; entonces la terna {P}C{Q} también es demostrable (pues su postcondición Qes más general que la de la terna anterior). Ejemplo: Probar `{R=X} Q:=0 {R=X+(Y*Q)}. Paso 0. `{R=X ∧0=0} Q:=0 {R=X ∧Q=0}. (Axioma de asignación) Paso 1. `R=X ⇒R=X ∧0=0. (Lógica) Paso 2. `{R=X} Q:=0 {R=X ∧Q=0}. (Reforzamiento de la precondición 0,1) Paso 3. `R=X ∧Q=0 ⇒R=X+(Y*Q). (Aritmética) Paso 4. `{R=X} Q:=0 {R=X+(Y*Q)}. (Debilitamiento de la postcondición 2,3)  Las dos reglas anteriores se pueden condensar en una sola, como se explica a continuación. Regla de la consecuencia Regla de la consecuencia `P⇒P0,` {P0}C{Q0},`Q0⇒Q ` {P}C{Q} Si a partir de la condición Pse tiene la condición P0, la terna de Hoare {P0}C{Q0} es demostrable y, además, de su postcondición Q0se deduce Q; entonces se puede concluir que la terna {P}C{Q}también es demostrable. 57 Lógica de Hoare Paso 6. `(R2≤X∧(R+1)2=T ∧ ¬(T≤X)) ⇒(R2≤X∧X<(R+1)2). (Aritmética) Paso 7. `{R2≤X∧(R+1)2=T} WHILE T≤X DO (R:=R+1; T:=T+(2*R+1)) {R2≤X∧X<(R+1)2}. (Debilitamiento de la postcondición 5,6) Paso 8. `{R2≤X∧(R+1)2=1} T:=1 {R2≤X∧(R+1)2=T}. (Axioma de asignación) Paso 9. `{0≤X∧1=1} R:=0 {R2≤X∧(R+1)2=1}. (Axioma de asignación + Aritmética + Reforzamiento de la precondición) Paso 10. `{0≤X∧1=1} C8{R2≤X∧(R+1)2<T}. (Regla de secuenciación 7,8,9) Paso 11. `0≤X⇒0≤X∧1=1. (Lógica) Paso 12. `{0≤X} C8{R2≤X∧(R+1)2<T}. (Reforzamiento de la precondición 10,11)  Ejemplo 4: Probaremos que la siguiente terna de Hoare para C9es demostrable. El programa C9calcula en la variable Tla diferencia entre YyX. {X=m ∧Y=n ∧0≤m} C9=   R:=m; T:=n; WHILE 0<R DO (R:=R-1; T:=T-1) {T=n-m}. Se propone como invariante: Invariante P≡“m+T=n+R∧0≤R∧R≤m” Veamos que Pes un invariante. Es decir, veamos que se cumple que: `{P ∧0<R} R:=R-1; T:=T-1 {P} Paso 0. `{m+T-1=n+R ∧0≤R∧R≤m} T:=T-1 {m+T=n+R ∧0≤R∧R≤m}. (Axioma de asignación) 64 Lógica de Hoare Paso 1. `{m+T-1=n+R-1 ∧0≤R-1 ∧R-1≤m} R:=R-1 {m+T-1=n+R ∧0≤R∧R≤m}. (Axioma de asignación) Paso 2. `{m+T-1=n+R-1 ∧0≤R-1 ∧R-1≤m} R:=R-1; T:=T-1 {m+T=n+R ∧0≤R∧R≤m}. (Regla de secuenciación 0,1) Paso 3. `(m+T=n+R ∧0≤R∧R≤m∧0<R) ⇒(m+T-1=n+R-1 ∧0≤R-1 ∧R-1≤m). (Aritmética) Paso 4. `{m+T=n+R ∧0≤R∧R≤m∧0<R} R:=R-1; T:=T-1 {m+T=n+R ∧0≤R∧R≤m}. (Reforzamiento de la precondición 2,3) XEs invariante. Paso 5. `{m+T=n+R ∧0≤R∧R≤m} WHILE 0<R DO (R:=R-1; T:=T-1) {m+T=n+R ∧0≤R∧R≤m∧ ¬(0<R)}. (Regla While para el invariante anterior) Paso 6. `(m+T=n+R ∧0≤R∧R≤m∧ ¬(0<R)) ⇒T=n-m. (Aritmética) Paso 7. `{m+T=n+R ∧0≤R∧R≤m} WHILE 0<R DO (R:=R-1; T:=T-1) {T=n-m}. (Debilitamiento de la postcondición 5,6) Paso 8. `{m+n=n+R ∧0≤R∧R≤m} T:=n {m+T=n+R ∧0≤R∧R≤m}. (Axioma de asignación) Paso 9. `{m+n=n+m ∧0≤m∧m≤m} R:=m {m+n=n+R ∧0≤R∧R≤m}. (Axioma de asignación) Paso 10. `{m+n=n+m ∧0≤m∧m≤m} C9{T=n-m}. (Regla de secuenciación 7,8,9) Paso 11. `(X=m ∧Y=n ∧0≤m) ⇒(m+n=n+m ∧0≤m∧m≤m). (Aritmética) Paso 12. `{X=m ∧Y=n ∧0≤m} C9{T=n-m}. (Reforzamiento de la precondición 10,11)  Ejemplo 5: Probaremos que la siguiente terna de Hoare para C10 es demostrable, donde tras la ejecución del programa C10 se obtiene la potencia de Xen base 2. Esta operación se ha expresado con la notación de función pot2(X)=2X. {X=n ∧0≤n} 65 Lógica de Hoare C10 =   R:=0; T:=1; WHILE R6=n DO (R:=R+1; T:=2*T) {T=pot2(n)}. Primeramente, se demuestra que se tiene un invariante: Invariante P≡“T=pot2(R)∧0≤R∧R≤n” Veamos que se cumple que: `{P ∧R6=n} R:=R+1; T:=2*T {P} Paso 0. `{2*T=pot2(R) ∧0≤R∧R≤n} T:=2*T {T=pot2(R) ∧0≤R∧R≤n}. (Axioma de asignación) Paso 1. `{2*T=pot2(R+1) ∧0≤R+1 ∧R+1≤n} R:=R+1 {2*T=pot2(R) ∧0≤R∧R≤n}. (Axioma de asignación) Paso 2. `{2*T=pot2(R+1) ∧0≤R+1 ∧R+1≤n} R:=R+1; T:=2T {T=pot2(R) ∧0≤R∧R≤n}. (Regla de secuenciación 0,1) Paso 3. `(T=pot2(R) ∧0≤R∧R≤n∧R6=n) ⇒ (2*T=pot2(R+1) ∧0≤R+1 ∧R+1≤n). (Aritmética) Paso 4. `{T=pot2(R) ∧0≤R∧R≤n∧R6=n} R:=R+1; T:=2*T {T=pot2(R) ∧0≤R∧R≤n}. (Reforzamiento de la precondición 2,3) XEs invariante. Paso 5. `{T=pot2(R) ∧0≤R∧R≤n} WHILE R6=n DO (R:=R+1; T=2*T) {T=pot2(R) ∧0≤R∧R≤n∧ ¬(R6=n)}. (Regla While para el invariante anterior) Paso 6. `(T=pot2(R) ∧0≤R∧R≤n∧ ¬(R6=n)) ⇒T=pot2(n). (Lógica) Paso 7. `{T=pot2(R) ∧0≤R∧R≤n} WHILE R6=n DO (R:=R+1; T=2*T) {T=pot2(n)}. (Debilitamiento de la postcondición 5,6) Paso 8. `{1=pot2(R) ∧0≤R∧R≤n} T:=1 {T=pot2(R) ∧0≤R∧R≤n}. (Axioma de asignación) Paso 9. `{1=pot2(0) ∧0≤0∧0≤n} R:=0 {1=pot2(R) ∧0≤R∧R≤n}. (Axioma de asignación) 66 Lógica de Hoare Paso 10. `{1=pot2(0) ∧0≤0∧0≤n} C10 {T=pot2(n)}. (Regla de secuenciación 7,8,9) Paso 11. `(X=n ∧0≤n) ⇒(1=pot2(0) ∧0≤0∧0≤n). (Aritmética) Paso 12. `{X=n ∧0≤n} C10 {T=pot2(n)}. (Reforzamiento de la precondición 10,11)  Ejemplo 6: Probaremos que la siguiente terna de Hoare para C11 es demostrable. El programa C11 calcula el cociente y el resto de la división euclídea de Xentre Y. {X=a ∧Y=b ∧0≤a∧0<b} C11 =   C:=0; R:=a; WHILE b≤R DO (C:=C+1; R:=R-b) {a=b*C+R ∧R<b}. Primeramente, consideramos el siguiente invariante para el bucle: Invariante P≡“a=b∗C+R∧0≤R” Veamos que, de hecho, es invariante. Es decir, veamos que se cumple que: `{P ∧b≤R} C:=C+1; R:=R-b {P} Paso 0. `{a=b*C+(R-b) ∧0≤R-b} R:=R-b {a=b*C+R ∧0≤R}. (Axioma de asignación) Paso 1. `{a=b*(C+1)+(R-b) ∧0≤R-b} C:=C+1 {a=b*C+(R-b) ∧0≤R-b}. (Axioma de asignación) Paso 2. `{a=b*(C+1)+(R-b) ∧0≤R-b} C:=C+1; R:=R-b {a=b*C+R ∧0≤R}. (Regla de secuenciación 0,1) Paso 3. `(a=b*C+R ∧0≤R∧b≤R) ⇒(a=b*(C+1)+(R-b) ∧0≤R-b). (Aritmética) Paso 4. `{a=b*C+R ∧0≤R∧b≤R} C:=C+1; R:=R-b {a=b*C+R ∧0≤R}. (Reforzamiento de la precondición 2,3) 67 Lógica de Hoare XEs invariante. Paso 5. `{a=b*C+R ∧0≤R} WHILE b≤R DO (C:=C+1; R:=R-b) {a=b*C+R ∧0≤R∧ ¬(b≤R)}. (Regla While para el invariante anterior) Paso 6. `(a=b*C+R ∧0≤R∧ ¬(b≤R)) ⇒(a=b*C+R ∧R<b). (Aritmética) Paso 7. `{a=b*C+R ∧0≤R} WHILE b≤R DO (C:=C+1; R:=R-b) {a=b*C+R ∧R<b}. (Debilitamiento de la postcondición 5,6) Paso 8. `{a=b*C+a ∧0≤a} R:=a {a=b*C+R ∧0≤R}. (Axioma de asignación) Paso 9. `{a=a ∧0≤a} C:=0 {a=b*C+a ∧0≤a}. (Axioma de asignación + Aritmética + Reforzamiento de la precondición) Paso 10. `{a=a ∧0≤a} C11 {a=b*C+R ∧R<b}. (Regla de secuenciación 7,8,9) Paso 11. `(X=a ∧Y=b ∧0≤a∧0<b) ⇒(a=a ∧0≤a). (Aritmética) Paso 12. `{X=a ∧Y=b ∧0≤a∧0<b} C11 {a=b*C+R ∧R<b}. (Reforzamiento de la precondición 10,11)  3.2.3. Adecuación y completitud para la corrección parcial Un sistema lógico se dirá adecuado si toda expresión demostrable en él es verdadera. Un sistema lógico se dirá completo si toda expresión verdadera escrita en su lenguaje es demostrable en el sistema. La lógica de Hoare para la corrección parcial que hemos estudiado en las secciones anteriores es tanto adecuada como completa. Teorema 3.2.1 (Adecuación) ` {P}C{Q}=⇒ |={P}C{Q}. Prueba: (Idea) Basta comprobar que cada axioma y cada regla de la lógica de Hoare son adecuados y razonar por inducción sobre la longitud de una prueba en la lógica de Hoare. Teorema 3.2.2 (Completitud) |={P}C{Q}=⇒ ` {P}C{Q}. La prueba de la completitud de la lógica de Hoare es más elaborada y descansa en el concepto de precondición más débil que describimos a continuación. Para motivar la definición, consideremos, por ejemplo, la asignación X=:2*Y+1. Una terna de Hoare verdadera para dicho comando es: {Y≤3} X:=2*Y+1 {(X≤7)∧(Y≤3)}. 68 Lógica de Hoare Pero Y≤3no es la única precondición que hace la postcondición cierta. Otra tal precondición podría ser: {Y=1 ∨Y=3} X:=2*Y+1 {(X≤7)∧(Y≤3)}. Ahora bien, la segunda precondición Y=1 ∨Y=3 es menos interesante que la primera Y≤3, pues la segunda no caracteriza todos los estados iniciales desde los cuales la computación del programa alcanzará un estado satisfaciendo la postcondición. Queremos pues elegir la precondición menos restrictiva que haga cierta una terna de Hoare. Ello lo conseguiremos mediante el concepto de precondición más débil. Definición 3.2.1 Diremos que una condición Pes más débil que una condición Q si la fórmula de primer orden Q⇒Pes verdadera en Z. Definición 3.2.1 Dados un programa Cy una condición Q, la precondición más débil para CyQ, que denotaremos por wp(C, Q), es la condición Pmás débil tal que la terna de Hoare {P}C{Q}es verdadera. Por ejemplo, wp(X:=2*Y+1,X≤7) = Y≤3. De la propia definición se sigue que: Lema 3.2.1 La terna de Hoare {P}C{Q}es verdadera si, y sólo si, la fórmula P⇒wp(C, Q)es verdadera. Una propiedad esencial para la prueba del teorema de completitud es que la condición wp(C, Q)es, de hecho, expresable en el lenguaje de primer orden subyacente a la lógica de Hoare. Es por ello que hemos supuesto que nuestro lenguaje de primer orden contiene, al menos, a la suma y al producto como operaciones básicas, pues para expresar en la lógica de primer orden la precondición más débil correspondiente a un comando tipo WHILE es necesario usar la función βde Gödel (u otra de similar naturaleza) para codificar convenientemente sucesiones finitas. Usando que la condición wp(C, Q)es expresable y razonando por inducción estructural, se prueba que: Lema 3.2.2 Para todo CyQ, se tiene que ` {wp(C, Q)}C{Q}. Podemos ahora dar un esquema de la prueba del teorema de completitud para la lógica de Hoare: |={P}C{Q}=⇒ |=P⇒wp(C, Q)(Lema 3.2.1) =⇒ ` P⇒wp(C, Q)(Axioma del dominio) =⇒ ` {wp(C, Q)}C{Q}(Lema 3.2.2) =⇒ ` {P}C{Q}(Reforzamiento de la precondición) 69 Lógica de Hoare 3.2.4. Corrección total Los axiomas de la lógica de Hoare, ya descritos en la sección (3.2.1), sirven para probar que un programa es correcto parcialmente. No obstante, el sistema de la lógica de Hoare se puede ampliar para probar que tales programas son totalmente correctos, en el caso que corresponda. Es decir, para que se pueda demostrar que su ejecución termina. 1 Como se dijo anteriormente, para demostrar la corrección total se suele probar de forma separada la corrección parcial y la terminación. Corrección total =Corrección parcial +Terminación De esta forma, si una terna de Hoare es correcta totalmente entonces también lo es parcialmente. Esto es, se tiene que: `[P]C[Q] ` {P}C{Q} Dicha relación ya no es cierta, en general, en sentido inverso. Ahora bien, si nos restringimos a programas en los que no interviene el comando WHILE, entonces dichos programas siempre terminan. Todos los comandos estudiados, a excepción del comando WHILE, terminan para cualquier estado inicial a partir del cual se ejecuten. En consecuencia, la formulación de sus axiomas será la misma que en el caso de la correción parcial, reemplazando "{ }"por "[ ]". Esto es, para todos los comandos excepto el comando WHILE se cumple que: ` {P}C{Q} `[P]C[Q] Por tanto, todo el esfuerzo para obtener la versión de la lógica de Hoare para la corrección total se centrará en proponer una nueva formulación para la regla del comando WHILE. A continuación se muestran las reglas y los axiomas de la lógica de Hoare para la corrección total. La única diferencia importante respecto al sistema deductivo descrito en la sección (3.2.1) radica en la nueva regla para el comando WHILE descrita al final de la presente sección. 1En cuanto a la terminación de los programas imperativos introducidos, como en [7], supondremos que los errores del tipo 1/0 o fact(−1) no causan problemas en el lenguaje. Por tanto, la única causa que puede provocar que un programa no pare será la ejecución infinita de un bucle WHILE. 70 Lógica de Hoare Axiomas del dominio para la corrección total Axiomas del dominio `P para cualquier fórmula Pverdadera en la estructura Z. Axioma de asignación para la corrección total Axioma de asignación `[P[E/V ]] V:= E[P] donde Ves una variable, Ees una expresión, Pes una condición y la notación P[E/V ]denota el resultado de sustituir todas las ocurrencias de Vpor el término Een P. Reforzamiento de la precondición para la corrección total Reforzamiento de la precondición `P⇒P0,`[P0]C[Q] `[P]C[Q] Debilitamiento de la postcondición para la corrección total Debilitamiento de la postcondición `[P]C[Q0],`Q0⇒Q `[P]C[Q] Las dos reglas anteriores se pueden condensar en una sola, como se muestra a continuación. 71 Lógica de Hoare Regla de la consecuencia para la corrección total Regla de la consecuencia `P⇒P0,`[P0]C[Q0],`Q0⇒Q `[P]C[Q] Regla de secuenciación para la corrección total Regla de secuenciación `[P]C1[Q],`[Q]C2[R] `[P]C1;C2[R] Regla del condicional para la corrección total Regla del condicional `[P∧S]C1[Q],`[P∧ ¬S]C2[Q] `[P]IF STHEN C1ELSE C2[Q] Regla While para la corrección total En el caso de la corrección parcial, este axioma se presentó como “el más interesante de la lógica de Hoare”, por razones ya explicadas. Este comentario es, si cabe, aún más apropiado en el caso de la corrección total. Este comando es el único de nuestro pequeño lenguaje imperativo que no presenta una terminación inmediata, que podría no terminar para ciertos estados iniciales. Considérese por ejemplo el comando WHILE X6= 0 DO X:=X-1 que sólo termina para estados iniciales en los que Xtenga un valor no negativo; o bien el comando WHILE X=X DO X:=X-1 que no termina para ningún estado inicial. ¿Cómo podemos pues demostrar formalmente que un bucle tipo WHILE termina en caso de que así sea? La idea consiste en encontrar alguna “cantidad” numérica 72 Lógica de Hoare entera, ya sea alguna de las variables que intervenga en el programa o ya sea alguna expresión aritmética entera construida a partir de ellas, que tome solamente valores enteros no negativos y que decrezca con cada iteración del bucle WHILE. Diremos entonces que dicha cantidad o variable es una variante del comando WHILE correspondiente, y la denotaremos por E. Puesto que el conjunto de los enteros no negativos no posee cadenas infinitas en orden descendiente (Nes un conjunto bien ordenado), la existencia de una tal variante para el bucle WHILE garantiza su terminación. En la formulación de la regla While, debemos hacer explícito que la variante E toma simpre valores no negativos y usaremos una variable auxiliar npara expresar que la variante Edecrece. Por otra parte, incorporamos también el concepto de invariante del bucle para expresar la semántica de la instrucción, tal y como se hizo en la regla While para la corrección parcial. Por tanto, la formulación de la regla While queda ahora como sigue: Regla WHILE `[P∧S∧(E=n)] C[P∧(E < n)],`P∧S⇒0≤E `[P]WHILE SDO C[P∧ ¬S] donde la condición Pse dirá un invariante del bucle, la expresión Ese dirá una variante del bucle, y nes una variable auxiliar. 3.2.5. Ejemplos de ternas demostrables: corrección total A modo de ejemplo, daremos una prueba en la lógica de Hoare de la corrección total del programa C5(descrito al final de la sección (3.1.3)) para calcular el factorial de un entero no negativo X, Es decir, probaremos que: 1) la ejecución del programa C5termina para cualquier estado inicial que satisfaga X≥0, y 2) para dichos estados iniciales C5calcula en su variable de salida Yel factorial de X. Esto es, daremos una prueba de la siguiente terna de Hoare: [0 ≤X] C5=   Y:=1; R:=0; WHILE R6=X DO (R:=R+1; Y:=Y*R) [Y=fact(X)] Proponemos como invariante del bucle la condición 73 Lógica de Hoare en Isabelle/HOL fun asimp_const :: "aexp ⇒aexp" where "asimp_const (N n) = N n" | "asimp_const (V x) = V x" | "asimp_const (Plus a1 a2) = (case (asimp_const a1, asimp_const a2) of (N n1, N n2) ⇒N(n1+n2) | (b1,b2) ⇒Plus b1 b2)" Lema 4.1.2 La simplificación es correcta. Es decir, no cambia el valor de la expresión aritmética. •La demostración aplicativa es: theorem aval_asimp_const: "aval (asimp_const a) s = aval a s" apply(induction a) apply (auto split: aexp.split) done Comentarios sobre la demostración anterior: La prueba se realiza por inducción en la expresión a. Si aes un número o una variable, es trivial. Y, si aes de la forma Plus a1 a2, se distiguen dos casos, según que a1 ya2 sean o no expresiones numéricas. •En la prueba automática: split proporciona la ayuda para que se realice la distinción de casos cuando una expresión case se aplica sobre un dato aexp. Segunda simplificación: Eliminación de los ceros en las sumas. Para ello, definimos la función plus fun plus :: "aexp ⇒aexp ⇒aexp" where "plus (N i1) (N i2) = N(i1+i2)" | "plus (N i) a = (if i=0 then a else Plus (N i) a)" | "plus a (N i) = (if i=0 then a else Plus a (N i))" | "plus a1 a2 = Plus a1 a2" Lema 4.1.3 La función plus se comporta como el constructor de tipo Plus mediante la evaluación. •La demostración aplicativa es: lemma aval_plus[simp]: "aval (plus a1 a2) s = aval a1 s + aval a2 s" apply(induction a1 a2 rule: plus.induct) apply simp_all done 80 Lógica de Hoare en Isabelle/HOL •La demostración automática es: lemma "aval (plus a1 a2) s = aval a1 s + aval a2 s" by (induct a1 a2 rule: plus.induct) simp_all Simplificación total: La función asimp simplifica una expresión aritmética, eliminando los ceros de las sumas y efectuando las sumas de las subexpresiones numéricas. fun asimp :: "aexp ⇒aexp" where "asimp (N n) = N n" | "asimp (V x) = V x" | "asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)" Por ejemplo, value "asimp (Plus (V ’’x’’) (Plus (Plus (N 3) (N 1)) (Plus (V ’’y’’) (N 0))))" queda de la forma "Plus (V ’’x’’) (Plus (N 4) (V ’’y’’))" Lema 4.1.4 La función asimp es correcta: el valor de la expresión aritmética no varía. •La demostración aplicativa es: theorem aval_asimp[simp]: "aval (asimp a) s = aval a s" apply(induction a) apply simp_all done •La demostración automática es: theorem "aval (asimp a) s = aval a s" by (induct a) simp_all Comentarios sobre la demostración anterior: La demostración es por inducción estructurada en la expresión a. 81 Lógica de Hoare en Isabelle/HOL 4.2. Expresiones booleanas Definición 4.2.1 Una expresión booleana es: una constante booleana, la negación de una expresión booleana, la conjunción de dos expresiones booleanas, o la comparación de dos expresiones aritméticas. Una expresión booleana se representa mediante el tipo bexp, definido por datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp En cuanto a la semántica, el valor de una expresión booleana en un estado se define: fun bval :: "bexp ⇒state ⇒bool" where "bval (Bc v) s = v" | "bval (Not b) s = (¬bval b s)" | "bval (And b1 b2) s = (bval b1 s ∧bval b2 s)" | "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" Veamos un par de ejemplos: value "bval (Less (V ’’x’’) (Plus (N 3) (V ’’y’’))) <’’x’’ := 3, ’’y’’ := 1>" value "bval (Less (V ’’x’’) (Plus (N 3) (V ’’y’’))) <’’x’’ := 5, ’’y’’ := 1>" Las reglas de simplificación introducidas por la definición se observan con thm bval.simps. Se quiere eliminar la tercera regla y definirla de otra forma más eficiente computacionalmente. Establecemos el siguiente lema como regla de simplificación de las expresiones condicionales, con objeto de mejorar los procesos automáticos de demostración: lemma bval_And_if[simp]: "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" by(simp) Para eliminar la tercera regla de simplificación del proceso automático hay que ordenar declare bval.simps(3)[simp del]. Esto no significa que ya no se pueda utilizar, basta con escribir bval.simps(3) para volver a hacer uso de ella. Como en el caso de las expresiones aritméticas, aquí también es conveniente realizar algunas optimizaciones. 82 Lógica de Hoare en Isabelle/HOL 4.2.1. Simplificación de constantes Primera simplificación: La función less simplificará las expresiones de la forma "Less (N n1) (N n2)" a "Bc (n1 < n2)". fun less :: "aexp ⇒aexp ⇒bexp" where "less (N n1) (N n2) = Bc(n1 < n2)" | "less a1 a2 = Less a1 a2" Lema 4.2.1 La función less es correcta. El valor de la expresión less a1 a2 en un estado scoincide con el valor de aval a1 s <aval a2 s. •La demostración aplicativa es: lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)" apply(induction a1 a2 rule: less.induct) apply simp_all done Segunda simplificación: Definimos una función and que simplificará las expresiones booleanas conjuntivas, una de cuyas componentes sea una constante booleana. fun "and" :: "bexp ⇒bexp ⇒bexp" where "and (Bc True) b = b" | "and b (Bc True) = b" | "and (Bc False) b = Bc False" | "and b (Bc False) = Bc False" | "and b1 b2 = And b1 b2" Lema 4.2.2 La función and es correcta. •La demostración aplicativa es: lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s ∧bval b2 s)" apply(induction b1 b2 rule: and.induct) apply simp_all done Tercera simplificación: Definimos una función not que simplificará las expresiones booleanas negativas de constantes booleanas. 83 Lógica de Hoare en Isabelle/HOL fun not :: "bexp ⇒bexp" where "not (Bc True) = Bc False" | "not (Bc False) = Bc True" | "not b = Not b" Lema 4.2.3 La función not es correcta. •La demostración aplicativa es: lemma bval_not[simp]: "bval (not b) s = (¬bval b s)" apply(induction b rule: not.induct) apply simp_all done Simplificación total: La función bsimp simplifica las expresiones booleanas, mediante las funciones previas. fun bsimp :: "bexp ⇒bexp" where "bsimp (Bc v) = Bc v" | "bsimp (Not b) = not (bsimp b)" | "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" | "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" Lema 4.2.4 La función bsimp es correcta: el valor de la expresión booleana simplificada coincide con el valor de la expresión inicial, en cualquier estado. •La demostración aplicativa es: theorem "bval (bsimp b) s = bval b s" apply(induction b) apply simp_all done A continuación se muestra un par de ejemplos value "bsimp (And (Less (N 0) (N 1)) b)" se reemplaza por "bsimp b", value "bsimp (And (Less (N 1) (N 0)) (Bc True))" se reemplaza por "Bc False". 84 Lógica de Hoare en Isabelle/HOL 4.3. Sintaxis del lenguaje imperativo simple IMP En la sección (3.1.1) se describen cuáles son los comandos que forman el lenguaje. Se muestra qué notación se utiliza (sintaxis) y qué significado se le da a esta notación (semántica), es decir, explicaciones teóricas que se pueden deducir o intuir. En Isabelle/HOL es necesario precisar dicha sintaxis y semántica. Para la sintaxis se define un nuevo tipo de dato, que se explica a continuación, y para la semántica se construye un predicado ternario, como se muestra más adelante. En cuanto a la sintaxis, para especificar la notación elegida definimos un lenguaje imperativo con las instrucciones básicas del lenguaje: asignación, composición secuencial, condicional, WHILE ySKIP (para representar una instrucción sin ninguna acción a realizar). Instrucciones del lenguaje: Assign x e: asignar la expresión aritmética ea la variable x. Seq c1 c2: realizar la instrucción c1 y, a continuación, c2. If b c1 c2: si la expresión booleana bes verdadera, realizar c1; en caso contrario, realizar c2. While b c: mientras la expresión booleana bsea verdadera, realizar c. SKIP: no hacer nada. Representamos el lenguaje mediante el siguiente tipo de dato: datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;;/ _" [60, 61] 60) | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) Comentarios acerca de las instrucciones: Escribiremos Assign x a como x ::= e. Escribiremos Seq c1 c2 como c1 ;; c2. Escribiremos If b c1 c2 como IF b THEN c1 ELSE c2. Escribiremos While b c como WHILE b DO c. La instrucción ;; asocia por la izquierda. Es decir, c1 ;; c2 ;; c3 es (c1 ;; c2) ;; c3 Las instrucciones IF yWHILE tienen prelación sobre ;;. Es decir, WHILE b DO c1 ;; c2 es (WHILE b DO c1) ;; c2. 85 Lógica de Hoare en Isabelle/HOL 4.4. Semántica operacional del lenguaje imperativo simple IMP En esta sección se define una semántica operacional para dar una interpretación a cada instrucción del lenguaje IMP. Esto es, el significado exacto que tendrá cada comando de la sección (3.1.1). La idea es que la semántica describa el proceso de ejecución de un programa, en lugar de centrarse en los resultados. Se ha elegido una semántica operacional natural ode paso largo, así se simplifica la notación y se ocultan los detalles, dándose un paso más grande en la computación. 4.4.1. Semántica de paso largo La semántica de paso largo establece una relación entre el programa, el estado inicial y el estado final. Los estados intermedios no se tienen en cuenta en dicha relación. Aunque a través de las reglas inductivas que van a definir la semántica se puede ver cómo es la ejecución del programa, la relación propiamente dicha sólo muestra como si el programa se ejecutara en un único paso, paso largo. Formalizamos la semántica mediante un predicado ternario big_step, tal que big_step c s t significa que la ejecución de la instrucción c, empezando en el estado s, termina en el estado t. Nota: Usaremos la notación (c,s) ⇒t, en vez de big_step c s t. Semántica del lenguaje: inductive big_step :: "com ×state ⇒state ⇒bool" (infix "⇒" 55) where Skip: "(SKIP,s) ⇒s" | Assign: "(x ::= a,s) ⇒s(x := aval a s)" | Seq: "J(c1,s1) ⇒s2; (c2,s2) ⇒s3 K=⇒(c1;;c2, s1) ⇒s3" | IfTrue: "Jbval b s; (c1,s) ⇒tK=⇒ (IF b THEN c1 ELSE c2, s) ⇒t" | IfFalse: "J¬bval b s; (c2,s) ⇒tK=⇒ (IF b THEN c1 ELSE c2, s) ⇒t" | WhileFalse: "¬bval b s =⇒(WHILE b DO c,s) ⇒s" | WhileTrue: "Jbval b s1; (c,s1) ⇒s2; (WHILE b DO c, s2) ⇒s3 K =⇒(WHILE b DO c, s1) ⇒s3" Descripción de la semántica de cada instrucción: Si la instrucción es SKIP, el estado inicial y el final han de ser el mismo. Si la instrucción es x::= a y el estado inicial es s, entonces el estado final es el estado sen el que el valor de la variable xes el valor de aen s. 86 Lógica de Hoare en Isabelle/HOL Si la instrucción es c1;;c2 y el estado inicial es s1, entonces el estado final es s3 si existe un estado intermedio s2 tal que c1 termina en s2, empezando en s1, y c2 termina en s3, empezando en s2. La instrucción condicional If b c1 c2 se corresponde con la descrita en (3.2.1). Para darle significado en Isabelle se ha dividido en dos reglas, dependiendo del valor de ben el estado inicial s: •Si es True, entonces el estado final es el estado final de ejecutar c1 empezando en s. •Si es False, entonces el estado final es el estado final de ejecutar c2 empezando en s. La instrucción While b c se corresponde con la descrita en (3.2.1). Igual que en el caso previo, esta instrucción también se ha dividido en dos reglas, dependiendo del valor de ben el estado inicial s: •Si es False, entonces el estado final es s. •Si es True en un estado inicial s1, entonces el estado final será un estado s3 si existe un estado intermedio s2 tal que: ◦la instrucción ctermina en s2 empezando en s1, y ◦el bucle While b c termina en s3, empezando en s2. Ejemplo. Sea el programa P: P = ’’x’’::= N 5 ;; ’’y::= V ’’x’’. Si ejecutamos Pen un estado inicial s, el estado final será el mismo estado sen el que xeyvalen 5. Veamos cómo usar Isabelle para seguir la ejecución del programa. schematic_lemma ex: "(’’x’’ ::= N 5;; ’’y’’ ::= V ’’x’’, s) ⇒?t" apply(rule Seq) apply(rule Assign) apply simp apply(rule Assign) done Una vez finalizada la prueba, Isabelle instancia el lema con el comando thm ex[simplified] y, después de simplificarlo, se obtiene (’’x’’ ::= N 5;; ’’y’’ ::= V ’’x’’, ?s) ⇒?s(’’x’’ := 5, ’’y’’ := 5) Otra forma mejor de ejecutar simbólicamente los programas IMP es usando el generador de código de Isabelle code_pred, y usando el comando values, análogo avalue pero que se puede aplicar a definiciones inductivas. 87 Lógica de Hoare en Isabelle/HOL code_pred big_step . values "{t. (SKIP, λ_. 0) ⇒t}" El código generado se puede ver mediante el comando thm big_step.equation. En los siguientes ejemplos, se calcula el valor de una lista de variables en el estado final de la ejecución de un programa. values "{map t [’’x’’] |t. (SKIP, <’’x’’ := 42>) ⇒t}" values "{map t [’’x’’] |t. (’’x’’ ::= N 2, <’’x’’ := 42>) ⇒t}" values "{map t [’’x’’,’’y’’] |t. (WHILE Less (V ’’x’’) (V ’’y’’) DO (’’x’’ ::= Plus (V ’’x’’) (N 5)), <’’x’’ := 0, ’’y’’ := 13>) ⇒t}" Automatización de las demostraciones: Con el comando declare big_step.intros [intro] declaramos las reglas big_step.intros como reglas de introducción, con objeto de automatizar la ejecución de programas pequeños. Nota: Como la definición de big_step es inductiva, las demostraciones suelen hacerse por inducción en la estructura de la definición. Si escribimos thm big_step.induct podemos observar tal esquema de inducción. ?x1.0 ⇒?x2.0 =⇒ (Vs. ?P (SKIP, s) s) =⇒ (Vx a s. ?P (x ::= a, s) (s(x := aval a s))) =⇒ (Vc1 s1 s2 c2 s3. (c1, s1) ⇒s2 =⇒ ?P (c1, s1) s2 =⇒ (c2, s2) ⇒s3 =⇒?P (c2, s2) s3 =⇒?P (c1;; c2, s1) s3) =⇒ (Vb s c1 t c2. bval b s =⇒(c1, s) ⇒t=⇒?P (c1, s) t =⇒ ?P (IF b THEN c1 ELSE c2, s) t) =⇒ (Vb s c2 t c1. ¬bval b s =⇒(c2, s) ⇒t=⇒?P (c2, s) t =⇒ ?P (IF b THEN c1 ELSE c2, s) t) =⇒ (Vb s c. ¬bval b s =⇒?P (WHILE b DO c, s) s) =⇒ 88 Lógica de Hoare en Isabelle/HOL (Vb s1 c s2 s3. bval b s1 =⇒ (c, s1) ⇒s2 =⇒ ?P (c, s1) s2 =⇒ (WHILE b DO c, s2) ⇒s3 =⇒ ?P (WHILE b DO c, s2) s3 =⇒?P (WHILE b DO c, s1) s3)=⇒ ?P ?x1.0 ?x2.0 Comentarios: El esquema de inducción tiene dos variables, ?x1.0 para representar la instrucción y ?x2.0 para el estado inicial, en vez de las tres que aparecerán en las pruebas: s,cyt. Con objeto de modificar la forma del esquema de inducción, introducimos el siguiente lema: lemmas big_step_induct = big_step.induct[split_format(complete)] Y observamos la nueva forma del esquema de inducción, ahora con las tres variables, que representan la instrucción, el estado inicial y el estado final. Si escribimos thm big_step_induct podremos observar tal esquema: (?x1a, ?x1b) ⇒?x2a =⇒ (Vs. ?P SKIP s s) =⇒ (Vx a s. ?P (x ::= a) s (s(x := aval a s))) =⇒ (Vc1 s1 s2 c2 s3. (c1, s1) ⇒s2 =⇒ ?P c1 s1 s2 =⇒(c2, s2) ⇒s3 =⇒?P c2 s2 s3 =⇒ ?P (c1;; c2) s1 s3) =⇒ (Vb s c1 t c2. bval b s =⇒(c1, s) ⇒t=⇒?P c1 s t =⇒ ?P (IF b THEN c1 ELSE c2) s t) =⇒ (Vb s c2 t c1. ¬bval b s =⇒(c2, s) ⇒t=⇒?P c2 s t =⇒ ?P (IF b THEN c1 ELSE c2) s t) =⇒ (Vb s c. ¬bval b s =⇒?P (WHILE b DO c) s s) =⇒ (Vb s1 c s2 s3. bval b s1 =⇒ (c, s1) ⇒s2 =⇒ 89 Lógica de Hoare en Isabelle/HOL theorem big_step_determ: "J(c,s) ⇒t; (c,s) ⇒t’ K=⇒t’ = t" by (induction arbitrary: t’ rule: big_step.induct) blast+ •En la siguiente demostración, sólo detallamos los casos significativos, dejando los demás de forma automática. theorem "(c,s) ⇒t=⇒(c,s) ⇒t’ =⇒t’ = t" proof (induction arbitrary: t’ rule: big_step.induct) -- "el único caso interesante es WhileTrue:" fix b c s s1 t t’ -- "las hipótesis de la regla:" assume "bval b s" and "(c,s) ⇒s1" and "(WHILE b DO c,s1) ⇒t" -- {* H.I.: nótese Vpor el uso de arbitrary: *} assume IHc: "Vt’. (c,s) ⇒t’ =⇒t’ = s1" assume IHw: "Vt’. (WHILE b DO c,s1) ⇒t’ =⇒t’ = t" -- "premisa de la implicación:" assume "(WHILE b DO c,s) ⇒t’" with ‘bval b s‘ obtain s1’ where c: "(c,s) ⇒s1’" and w: "(WHILE b DO c,s1’) ⇒t’" by auto from c IHc have "s1’ = s1" by blast with w IHw show "t’ = t" by blast qed blast+ -- "el resto se prueba de forma automática" 4.4.5. Ejemplos de funciones sobre programas En este apartado se muestran ejemplos de funciones sobre programas, así como algunas propiedades de las mismas. Ejemplo 1 Se define la función assigned, que obtiene el conjunto de las variables asignadas en un programa c. fun assigned :: "com ⇒vname set" where "assigned (SKIP) = {}"| "assigned (Assign v a) = {v}"| "assigned (Seq c1 c2) = (assigned c1)∪(assigned c2)"| "assigned (If a c1 c2) = (assigned c1)∪(assigned c2)"| "assigned (While b c) = (assigned c)" Lema 4.4.3 Si una variable no está asignada en un programa c, dicha variable nunca se modifica mediante c. •Demostración aplicativa: 96 Lógica de Hoare en Isabelle/HOL lemma "J(c, s) ⇒t; x /∈assigned c K=⇒s x = t x" apply(induction rule: big_step_induct) apply auto done Ejemplo 2 La función skip comprueba si el programa crealiza lo mismo que la instrucción SKIP. fun skip :: "com ⇒bool" where "skip (SKIP) = True"| "skip (Assign x a) = (∀s. (x ::= a,s) ⇒s)"| "skip (Seq c1 c2) = conj(skip c1)(skip c2)"| "skip (If a c1 c2) = conj(skip c1)(skip c2)"| "skip (While b c) = (∀s. (¬bval b s) )" Lema 4.4.4 La función skip es correcta. •Demostración estructurada para la cuál se han necesitado dos lemas auxiliares: lemma skip_1: "skip c =⇒(∀s.(c,s) ⇒s)" by (induct) auto lemma skip_2 : "(∀s t. (SKIP,s) ⇒t←→ s = t)" by auto lemma "skip c =⇒c∼SKIP" proof (induction c) case SKIP thus ?case by simp next case Assign thus ?case using skip_2 by auto next case (Seq a b) hence "a ∼SKIP" and "b ∼SKIP" by auto moreover hence "(a;; b) ∼(SKIP;; SKIP)" by blast moreover hence "(SKIP;; SKIP) ∼SKIP" by auto ultimately show ?case by auto next case (If a b c) hence "b ∼SKIP" and "c ∼SKIP" by auto thus ?case by blast next case While thus ?case by auto qed 97 Lógica de Hoare en Isabelle/HOL Ejemplo 3 La función deskip elimina de un programa ctodas las instruciones SKIP posibles. fun deskip :: "com ⇒com" where "deskip SKIP = SKIP"| "deskip (Assign x a) = Assign x a"| "deskip (Seq c1 c2) = (if(deskip c1)=SKIP then deskip c2 else if (deskip c2)=SKIP then deskip c1 else Seq (deskip c1) (deskip c2))" | "deskip (If b c1 c2) = ( If b (deskip c1)(deskip c2))"| "deskip (While b c) = (While b (deskip c))" Lema 4.4.5 La función deskip es correcta. Es decir, c∼(deskip c). •Demostración detallada: lemma "deskip c ∼c" proof (induction c) case SKIP show ?case by simp next case Assign show ?case by simp next case (Seq a b) hence "a;; b ∼deskip a;; deskip b" by auto moreover have "deskip (a;; b) ∼deskip a;; deskip b" by auto ultimately show ?case by auto next case If thus ?case by auto next case While thus ?case by (simp add: sim_while_cong) qed Ejemplo 4 Se define una nueva instrucción Or como sigue definition Or :: "bexp ⇒bexp ⇒bexp" where "Or b1 b2 = Not (And (Not b1) (Not b2))" Probar los siguientes lemas: ◦Lema 1: lemma While_end: "(WHILE b DO c, s) ⇒t=⇒ ¬bval b t" proof(induction "WHILE b DO c" s t rule: big_step_induct) case WhileFalse thus ?case . next case WhileTrue show ?case by fact qed 98 Lógica de Hoare en Isabelle/HOL ◦Lema 2: lemma "WHILE Or b1 b2 DO c ∼ WHILE Or b1 b2 DO c;; WHILE b1 DO c" proof - { fix s assume "¬bval (Or b1 b2) s" hence "¬bval b1 s" by (auto simp add: Or_def) } then show ?thesis by (blast intro!: While_end) qed Ejemplo 5 La siguiente función Do define la nueva instrucción DO c WHILE b, tal que la instrucción cse ejecuta una vez antes de comprobar si la expresión bes cierta en un estado. fun Do :: "com ⇒bexp ⇒com" ("DO _ WHILE _" [0, 61] 61) where "Do c b = Seq c (While b c)" Ejemplo 6 La función dewhile realiza una traducción de las instrucciones, reemplazando las instrucciones de la forma WHILE b DO c por instrucciones de la forma DO c WHILE b, manteniendo la semántica. fun dewhile :: "com ⇒com" where "dewhile SKIP = SKIP" | "dewhile (a ::= b) = a ::= b" | "dewhile (a;; b) = dewhile a;; dewhile b" | "dewhile (IF a THEN b ELSE c) = IF a THEN dewhile b ELSE dewhile c" | "dewhile (WHILE a DO b) = If a (Do b a) SKIP" Lema 4.4.6 La traducción conserva la semántica. lemma "dewhile c ∼c" proof (induction c) case SKIP thus ?case by simp next case Assign thus ?case by simp next case Seq thus ?case by auto next case If thus ?case by auto next case (While b c) hence "WHILE b DO c ∼WHILE b DO dewhile c" using sim_while_cong by simp thus ?case using Do_def while_unfold by auto qed 99 Lógica de Hoare en Isabelle/HOL 4.5. Lógica de Hoare en Isabelle/HOL Como se explicó en el capítulo (3), la lógica de Hoare es una lógica para probar propiedades de programas imperativos. Las fórmulas de esta lógica son ternas de la forma {P}C{Q}. El significado es el siguiente: si la fórmula Pes cierta antes de ejecutar la instrucción C, entonces la fórmula Qes cierta después de ejecutar C. 4.5.1. Corrección parcial Recordatorio: Sección (3.1.2). Las pre y postcondiciones de una terna de Hoare, también denominadas asertos, se pueden representar bien como objetos sintácticos concretos (como las expresiones booleanas), o bien como predicados sobre estados. Elegimos esta segunda representación porque es más adecuada para el razonamiento automático. Formalizamos los asertos (assn) como predicados sobre estados. type_synonym assn = "state ⇒bool" Veracidad de una terna: Como se explicó en el capítulo anterior, si la terna {P}C{Q}es verdadera escribiremos |={P}C{Q}. Definimos la veracidad de una terna formalmente. definition hoare_valid :: "assn ⇒com ⇒assn ⇒bool" ("|={(1_)}/ (_)/ {(1_)}" 50) where "|={P}c{Q} = (∀s t. P s ∧(c,s) ⇒t−→ Q t)" Notación: El estado sen el que el valor de la variable xes el valor de la expresión aen s, s(x := aval a s). En el capítulo anterior denotamos esto como s[a/x]. Formalizamos en Isabelle/HOL esta simplificación. abbreviation state_subst :: "state ⇒aexp ⇒vname ⇒state" ("_[_’/_]" [1000,0,0] 999) where "s[a/x] == s(x := aval a s)" 100 Lógica de Hoare en Isabelle/HOL Sistema deductivo: Hemos definido cuando una terna de Hoare es verdadera. Ahora presentamos el conjunto de reglas de inferencia o sistema deductivo que se utiliza para obtener o demostrar ternas de Hoare, que se corresponde con los axiomas (3.2.1), (3.2.1), (3.2.1), (3.2.1) y (3.2.1). inductive hoare :: "assn ⇒com ⇒assn ⇒bool" ("`({(1_)}/ (_)/ {(1_)})" 50) where Skip: "`{P} SKIP {P}" | Assign: "`{λs. P(s[a/x])} x::=a {P}" | Seq: "J`{P} c1 {Q}; `{Q} c2 {R} K =⇒ ` {P} c1;;c2 {R}" | If: "J`{λs. P s ∧bval b s} c1 {Q}; `{λs. P s ∧ ¬ bval b s} c2 {Q} K =⇒ ` {P} IF b THEN c1 ELSE c2 {Q}" | While: "`{λs. P s ∧bval b s} c {P} =⇒ `{P} WHILE b DO c {λs. P s ∧ ¬ bval b s}" | conseq: "J∀s. P’ s −→ P s; `{P} c {Q}; ∀s. Q s −→ Q’ s K =⇒ ` {P’} c {Q’}" Para añadir reglas de simplificación asociadas a la definición se declaran los siguientes lemas. lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq hoare.If lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If Recordatorio: Es importante no confundir las nociones de terna verdadera y terna demostrable. Validez (|={P}C{Q}), basada en la semántica operacional. Demostrabilidad (` {P}C{Q}), basada en el conjunto de reglas. Posteriormente, (4.5.3), probaremos que ambos conceptos son equivalentes: |={P}C{Q}si y sólo si ` {P}C{Q} Algunas de las reglas que forman parte del sistema deductivo, Skip,Assign o While, no son fáciles de manejar, pues sólo se pueden aplicar hacia atrás si la precondición o la postcondición tienen una forma exacta. Por ello, establecemos las reglas 101 Lógica de Hoare en Isabelle/HOL siguientes, que se prueban usando la regla de consecuencia. Reforzamiento de la precondición: lemma strengthen_pre: "J∀s. P’ s −→ P s; `{P} c {Q} K=⇒ ` {P’} c {Q}" by (blast intro: conseq) Debilitamiento de la postcondición: lemma weaken_post: "J`{P} c {Q}; ∀s. Q s −→ Q’ s K=⇒ ` {P} c {Q’}" by (blast intro: conseq) lemma Assign’: "∀s. P s −→ Q(s[a/x]) =⇒ ` {P} x ::= a {Q}" by (simp add: strengthen_pre[OF _ Assign]) lemma While’: assumes "`{λs. P s ∧bval b s} c {P}" and "∀s. P s ∧ ¬ bval b s −→ Q s" shows "`{P} WHILE b DO c {Q}" by(rule weaken_post[OF While[OF assms(1)] assms(2)]) Observación: En las deducciones en la lógica de Hoare es útil realizar razonamiento hacia atrás con la regla Seq, modificando el orden de los subobjetivos generados. Para hacerlo en un sólo paso, establecemos el lema Seq_bwd. lemmas Seq_bwd = Seq[rotated] Ejemplo a) Consideremos el programa que suma en ylos números de 1 a x: y := 0; WHILE 0 < x DO (y := y + x; x := x-1) Formalmente, el programa en el lenguaje IMP es la sucesión de la asignación y:=0 y el siguiente bucle abbreviation "wsum == WHILE Less (N 0) (V ’’x’’) DO (’’y’’ ::= Plus (V ’’y’’) (V ’’x’’);; ’’x’’ ::= Plus (V ’’x’’) (N -1))" Para probar que, efectivamente, el programa realiza la suma de los números de 1 a x, definimos la función sum, tal que sum i calcula la suma de los números de 1 ai. 102 Lógica de Hoare en Isabelle/HOL fun sum :: "int ⇒int" where "sum i = (if i ≤0 then 0 else sum (i - 1) + i)" Con el comando declare sum.simps[simp del] eliminamos las reglas de simplificación que generadas por la definición, y se establecen las siguientes: lemma sum_simps[simp]: "0 < i =⇒sum i = sum (i - 1) + i" "i ≤0=⇒sum i = 0" by(simp_all) El comportamiento del bucle WHILE con respecto a la función sum es: Si tes el estado que resulta de aplicar wsum al estado inicial s, entonces el valor de yen tes el valor inicial de yen smás la suma de los números desde 1 hasta el valor de xen s. Se trata de probar, usando las reglas de inferencia, que el programa realmente guarda en ydicha suma, es decir, que la terna de Hoare {x=n} y := 0; WHILE 0 <x DO (y := y + x; x := x-1) {y=sum(n)}. es demostrable. La prueba es la siguiente. lemma "`{λs. s ’’x’’ = n} ’’y’’ ::= N 0;; wsum {λs. s ’’y’’ = sum n}" apply(rule Seq) -- "Se generan dos subobjetivos: " -- "1. `{λs. s ’’x’’ = n} ’’y’’ ::= N 0 {?Q}" -- "2. `{?Q} wsum {λs. s ’’y’’ = sum n}" prefer 2 -- "Intercambiamos el orden en el que decidimos probarlos." -- "Como es un bucle, aplicamos la regla While’, instanciando" -- "P con el invariante del bucle" apply(rule While’ [where P = "λs. (s ’’y’’ = sum n - sum(s ’’x’’))"]) -- "En el primer subobjetivo hay que probar que P es un" -- "invariante del bucle. Como la instrucción es una composición," -- "aplicamos la regla Seq:" apply(rule Seq) prefer 2 apply(rule Assign) apply(rule Assign’) apply simp apply simp apply(rule Assign’) apply simp done Queda probado que, efectivamente, el programa guarda en ydicha suma. 103 Lógica de Hoare en Isabelle/HOL Ejemplo b) Sea la terna de Hoare {λ_. True} MAX {λs. s ’’c’’ = max (s ’’a’’) (s ’’b’’)} El programa MAX es análogo al del ejemplo expuesto para la regla del condicional en el capítulo anterior, (3.2.1). En este caso, MAX hace referencia al programa en sí, que calcula el máximo de dos números y lo almacena en c. definition MAX :: com where "MAX == IF (Less (V ’’a’’) (V ’’b’’)) THEN ’’c’’ ::= V ’’b’’ ELSE ’’c’’ ::= V ’’a’’" A continuación probamos que la terna anterior es demostrable. lemma "`{λ_. True} MAX {λs. s ’’c’’ = max (s ’’a’’) (s ’’b’’)}" unfolding MAX_def apply (rule If) apply (rule Assign’) apply simp apply arith apply (rule Assign’) apply simp apply arith done 4.5.2. Ejemplos En este apartado se resuelven de forma aplicativa, y detalladamente, ejemplos similares a los dos anteriores. Se trata de algunas de las ternas que se demostraron en la sección (3.2.2) del capítulo (3). La mayoría de estos ejemplos pertenecen al capítulo 12 del libro ([8]). Ejemplo 1 Probamos que la terna de Hoare del ejemplo 3 de la sección (3.2.2) es demostrable. Es decir, demostramos el siguiente lema. lemma "`{λs. 0 ≤s ’’x’’ } ’’r’’ ::= N 0;; ’’t’’ ::= N 1;; WHILE (Not (Less (V ’’x’’) (V ’’t’’))) 104 Lógica de Hoare en Isabelle/HOL DO (’’r’’ ::= Plus (V ’’r’’) (N 1);; ’’t’’ ::= Plus (V ’’t’’) (Plus (Plus (V ’’r’’) (V ’’r’’)) (N 1))) {λs. (s ’’r’’)^2 ≤s ’’x’’ ∧s ’’x’’ < (s ’’r’’ + 1)^2}" El programa calcula una aproximación entera de la raíz cuadrada de x. Nota: Usaremos las reglas de simplificación algebra_simps ypower2_eq_square. lemma "`{λs. 0 ≤s ’’x’’ } ’’r’’ ::= N 0;; ’’t’’ ::= N 1;; WHILE (Not (Less (V ’’x’’) (V ’’t’’))) DO (’’r’’ ::= Plus (V ’’r’’) (N 1);; ’’t’’ ::= Plus (V ’’t’’) (Plus (Plus (V ’’r’’) (V ’’r’’)) (N 1))) {λs. (s ’’r’’)^2 ≤s ’’x’’ ∧s ’’x’’ < (s ’’r’’ + 1)^2}" apply (rule Seq) prefer 2 apply (rule While’[where P = "λs. (s ’’r’’)^2 ≤(s ’’x’’) ∧ (s ’’t’’) = (s ’’r’’ + 1)^2"]) -- "Observamos que se pueden simplificar los subobjetivos" -- "mediante reglas algebraicas" apply (simp add:algebra_simps) apply (rule Seq) prefer 2 apply (rule Assign) apply (rule Assign’) apply (simp add:algebra_simps) -- "Se simplifican los subobjetivos mediante -- "la regla de simplificación power2_eq_square" apply (auto simp add:power2_eq_square) prefer 2 apply (rule Assign’) apply (simp add:power2_eq_square) apply (simp add:algebra_simps) done Ejemplo 2 Probemos la demostrabilidad de la terna del ejemplo 4 de la sección (3.2.2). Es decir, lemma "`{λs. s ’’x’’ = m ∧s ’’y’’ = n ∧0≤m} 105 Lógica de Hoare en Isabelle/HOL bval b s1, (c,s1) ⇒s2 (c = WHILE b DO c =⇒P s1 =⇒P s2 ∧ ¬ bval b s2) (WHILE b DO c, s2_) ⇒s3 P s2 =⇒P s3 ∧ ¬ bval b s3 P s1 hay que probar P s3 ∧ ¬ bval b s3. Teniendo P s1,bval b s1,(c,s1) ⇒s2 , aplicamos la hipótesis de inducción externa y se obtiene P s2. Luego, aplicando la hipótesis de inducción externa, tenemos P s3 ∧ ¬ bval b s3. Veamos ahora el teorema de completitud, también tratado en el capítulo anterior. Teorema 4.5.2 (Teorema de completitud de la lógica de Hoare con respecto a la semántica operacional) Si una terna {P}C{Q}es verdadera, entonces es demostrable. Esto es, |={P}C{Q}=⇒ ` {P}C{Q}. Ya sabemos que esta demostracion es más elaborada y que se basa en el concepto de precondición más débil. La precondición más débil de una instrucción Cy una postcondición Q, es el aserto más débil que, siendo cierto antes de la ejecución de C, garantiza que Qes cierto después. Formalizamos ahora en Isabelle/HOL la definición (3.2.1). definition wp :: "com ⇒assn ⇒assn" where "wp c Q = (λs. ∀t. (c,s) ⇒t−→ Q t)" Observación: La precondición más debil de CyQes un aserto, es decir un predicado sobre estados, que está definido mediante su λexpresión: aplicado a un estado scumple que, para cualquier estado ten el que finalice la ejecución de C, que ha empezado en s, se verifique Q t. El concepto de precondición más débil es central en la lógica de Hoare, pues hace posible la construcción de las pruebas de la lógica, obteniendo las precondiciones hacia atrás, de forma sucesiva. A partir de esta última definición y de los comandos que aquí se tratan se tienen las siguientes propiedades. 112 Lógica de Hoare en Isabelle/HOL lemma wp_SKIP[simp]: "wp SKIP Q = Q" apply (rule ext) -- "aplicamos extensionalidad: dos funciones son" -- "iguales si lo son en todos sus argumentos" apply (auto simp: wp_def) done lemma wp_Ass[simp]: "wp (x::=a) Q = (λs. Q(s[a/x]))" by (rule ext) (auto simp: wp_def) lemma wp_Seq[simp]: "wp (c1;;c2) Q = wp c1 (wp c2 Q)" by (rule ext) (auto simp: wp_def) lemma wp_If[simp]: "wp (IF b THEN c1 ELSE c2) Q = (λs. if bval b s then wp c1 Q s else wp c2 Q s)" by (rule ext) (auto simp: wp_def) lemma wp_While_If: -- "no se almacena como regla de simplificación" "wp (WHILE b DO c) Q s = wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s" by (metis while_unfold wp_def) -- "usando Sledgehammer" lemma wp_While_True[simp]: "bval b s =⇒ wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s" apply (simp add: wp_While_If) done lemma wp_While_False[simp]: "¬bval b s =⇒wp (WHILE b DO c) Q s = Q s" by(simp add: wp_While_If) En la prueba de completitud es clave la propiedad esencial de la precondición más débil de CyQ: también es una precondición con respecto a la noción de demostrabilidad. Esto es, el lema (3.2.2), que se prueba a continuación. lemma wp_is_pre: "`{wp c Q} c {Q}" proof(induction c arbitrary: Q) case If thus ?case by(auto intro: conseq) next case (While b c) let ?w = "WHILE b DO c" show "`{wp ?w Q} ?w {Q}" 113 Lógica de Hoare en Isabelle/HOL proof(rule While’) show "`{λs. wp ?w Q s ∧bval b s} c {wp ?w Q}" proof(rule strengthen_pre[OF _ While.IH]) show "∀s. wp ?w Q s ∧bval b s −→ wp c (wp ?w Q) s" by auto qed show "∀s. wp ?w Q s ∧ ¬ bval b s −→ Q s" by auto qed qed auto Por lo tanto, se muestra a continuación la prueba del teorema de completitud en Isabelle/HOL. theorem hoare_complete: assumes "|={P}c{Q}" shows "`{P}c{Q}" proof(rule strengthen_pre) show "∀s. P s −→ wp c Q s" using assms by (auto simp: hoare_valid_def wp_def) show "`{wp c Q} c {Q}" by(rule wp_is_pre) qed De estos dos teoremas se sigue el siguiente corolario. corollary hoare_sound_complete: "`{P}c{Q} ←→ |={P}c{Q}" by (metis hoare_complete hoare_sound) 4.5.4. Corrección total Veracidad de una terna: La noción informal de corrección total de una terna {P}C{Q}es la siguiente, tal y como se explica en (3.2.4): si Pes cierta antes de la ejecución de C, entonces Ctermina y Qes cierta después. Es ese caso escribimos |=[P]C[Q]. Definimos la veracidad de una terna formalmente. definition hoare_tvalid :: "assn ⇒com ⇒assn ⇒bool" ("|=t {(1_)}/ (_)/ {(1_)}" 50) where "|=t {P}c{Q} ←→ (∀s. P s −→ (∃t. (c,s) ⇒t∧Q t))" Nota: Observar que esta definición necesita que la ejecución sea determinista, que es nuestro caso. Sistema deductivo para la corrección total: Presentamos un conjunto de reglas de inferencia que son análogas a las presentadas para la corrección parcial, excepto para la instrucción While. En este caso, añadimos un predicado 114 Lógica de Hoare en Isabelle/HOL T:: state ⇒nat ⇒bool para garantizar la terminación del bucle. Esto es, la formalización de los axiomas y las reglas (3.2.4), (3.2.4), (3.2.4)y (3.2.4). También se formaliza la demostrabilidad de una terna correcta totalmente en cuanto al comando SKIP, aunque teóricamente se pueda considar como un caso particular del comando de asignación. inductive hoaret :: "assn ⇒com ⇒assn ⇒bool" ("`t ({(1_)}/ (_)/ {(1_)})" 50) where Skip: "`t {P} SKIP {P}" | Assign: "`t {λs. P(s[a/x])} x::=a {P}" | Seq: "J`t {P1} c1 {P2}; `t {P2} c2 {P3} K=⇒ `t {P1} c1;;c2 {P3}" | If: "J`t {λs. P s ∧bval b s} c1 {Q}; `t {λs. P s ∧ ¬ bval b s} c2 {Q} K =⇒ `t {P} IF b THEN c1 ELSE c2 {Q}" | While: "(Vn::nat. `t {λs. P s ∧bval b s ∧T s n} c {λs. P s ∧(∃n’<n. T s n’)}) =⇒ `t {λs. P s ∧(∃n. T s n)} WHILE b DO c {λs. P s ∧ ¬bval b s}" | conseq: "J∀s. P’ s −→ P s; `t {P}c{Q}; ∀s. Q s −→ Q’ s K=⇒ `t {P’}c{Q’}" Observación: En la regla While, la relación Tes una medida que necesariamente tiene que decrecer en cada paso del bucle. Modificamos la regla y obtenemos una versión funcional más intuitiva y útil para el razonamiento. thm While [where T="λs n. n = f s"] thm While [where T="λs n. n = f s", simplified] lemma While_fun: "JVn::nat. `t {λs. P s ∧bval b s ∧n = f s} c {λs. P s ∧f s < n}K =⇒ `t {P} WHILE b DO c {λs. P s ∧ ¬bval b s}" by (rule While [where T="λs n. n = f s", simplified]) 115 Lógica de Hoare en Isabelle/HOL Igual que en el caso de la corrección parcial, las reglas Skip,Assign yWhile no son fáciles de manejar tal y como están definidas. Por ello, se construyen estas otras reglas, que se prueban usando la regla de consecuencia. lemma strengthen_pre: "J∀s. P’ s −→ P s; `t {P} c {Q} K=⇒ `t {P’} c {Q}" by (blast intro: conseq) lemma weaken_post: "J`t {P} c {Q}; ∀s. Q s −→ Q’ s K=⇒ `t {P} c {Q’}" by (metis hoaret.conseq) -- "usando Sledgehammer" lemma Assign’: "∀s. P s −→ Q(s[a/x]) =⇒ `t {P} x ::= a {Q}" by (simp add: strengthen_pre[OF _ Assign]) lemma While_fun’: assumes "Vn::nat. `t {λs. P s ∧bval b s ∧n = f s} c {λs. P s ∧f s < n}" and "∀s. P s ∧ ¬ bval b s −→ Q s" shows "`t {P} WHILE b DO c {Q}" by(blast intro: assms(1) weaken_post[OF While_fun assms(2)]) 4.5.5. Ejemplos En este apartado se resuelve de forma aplicativa, y detalladamente, un ejemplo de terna demostrable con respecto a la correccón total. Se trata del Ejemplo a), (4.5.1), que se expuso al final de la sección (3.2.4). Tras la ejecución del programa se obtiene en yla suma de los números de 1 a x. lemma "`t {λs. s ’’x’’ = i} ’’y’’ ::= N 0;; wsum {λs. s ’’y’’ = sum i}" -- "aplicamos la regla Seq" apply(rule Seq) prefer 2 -- "cambiamos el orden de los subobjetivos" -- "Se trata de un bucle." -- "Aplicamos la regla While_fun’, instanciando el invariante" -- "y la función de medida" apply(rule While_fun’ [where P = "λs. (s ’’y’’ = sum i - sum(s ’’x’’))" and f = "λs. nat(s ’’x’’)"]) -- "En el primer subobjetivo hay que probar -- "que la variante elegida decrece." -- "Como la instrucción en una composición," -- "aplicamos la regla Seq:" apply(rule Seq) 116 Lógica de Hoare en Isabelle/HOL prefer 2 apply(rule Assign) apply(rule Assign’) apply simp apply(simp) apply(rule Assign’) apply simp done 4.5.6. Adecuación y completitud para la corrección total Teorema 4.5.3 (Teorema de adecuación de la lógica de Hoare para la corrección total) Si una terna [P]C[Q]es demostrable, entonces es verdadera. `t[P]C[Q]=⇒ |=t[P]C[Q]. En este caso, la demostración también es por inducción según la regla hoaret.induct. Hay que probar que cada regla de esta lógica conserva la validez. Todos los casos se demuestran de forma automática, excepto para la regla While. La prueba es la siguiente: theorem hoaret_sound: "`t {P}c{Q} =⇒ |=t {P}c{Q}" proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) -- "todos los casos son automáticos, excepto While" case (While P b T c) { fix s n have "JP s; T s n K=⇒ ∃t. (WHILE b DO c, s) ⇒ t∧P t ∧ ¬ bval b t" proof(induction "n" arbitrary: s rule: less_induct) case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue) qed } thus ?case by auto next case If thus ?case by auto blast qed fastforce+ Comentarios sobre la demostración anterior: Para el caso de la regla While el subobjetivo que se genera es: VP b T c. (Vn. `t {λs. P s ∧bval b s ∧T s n} c {λs. P s ∧(∃n’<n. T s n’)}) =⇒(Vn. ∀s. P s ∧bval b s ∧T s n −→ (∃t. (c, s) ⇒ t∧P t ∧(∃n’<n. T t n’))) =⇒ ∀s. P s ∧Ex (T s) −→ (∃t. (WHILE b DO c, s) ⇒t∧P t ∧ ¬ bval b t) 117 Lógica de Hoare en Isabelle/HOL Para este subobjetivo basta probar que para todo sytse tiene que ∃t. (WHILE b DO c, s) ⇒t∧P t ∧ ¬ bval b t" La prueba es por inducción fuerte en n, con sarbitrario (ver thm less_induct). Con esto y, usando las hipótesis de inducción, se tiene el resultado. Veamos ahora el teorema de completitud. Teorema 4.5.4 (Teorema de completitud de la lógica de Hoare para la corrección total) Si una terna [P]C[Q]es demostrable, entonces es verdadera. `t[P]C[Q]=⇒ |=t[P]C[Q]. La prueba de completitud es análoga a la prueba realizada para la completitud de la corrección parcial. En primer lugar, definimos una noción más fuerte de la precondición más débil, que tiene en cuenta la terminación: es un predicado tal que, aplicado a un estado s cumple que, existe un estado ttal que la ejecución de C, empezando en s, termina en ty se verifica Q. Formalizamos en Isabelle/HOL la idea de precondición más debil para el caso de la corrección total. definition wpt :: "com ⇒assn ⇒assn" ("wpt") where "wpt c Q = (λs. ∃t. (c,s) ⇒t∧Q t)" De esta última definición se siguen las siguientes propiedades. lemma [simp]: "wpt SKIP Q = Q" apply (rule ext) apply (auto simp: wpt_def) done lemma [simp]: "wpt (x ::= e) Q = (λs. Q(s(x := aval e s)))" by(auto intro: ext simp: wpt_def) lemma [simp]: "wpt (c1;;c2) Q = wpt c1 (wpt c2 Q)" unfolding wpt_def apply(rule ext) apply auto done 118 Lógica de Hoare en Isabelle/HOL lemma [simp]: "wpt (IF b THEN c1 ELSE c2) Q = (λs. wpt (if bval b s then c1 else c2) Q s)" apply(unfold wpt_def) apply(rule ext) apply auto done Definimos el número de iteraciones necesarias para que el bucle WHILE b DO c termine si empieza en el estado s. Como es, en realidad, una función parcial, lo definimos mediante inductive, con dos reglas: Si bno es cierta en s⇒el número de iteraciones es 0. Si bes cierta en s,(c,s) ⇒s’ y el número de iteraciones para que el bucle termine si empieza en s’ es n, entonces el número de iteraciones para que el bucle termine si empieza en ses n+1. inductive Its :: "bexp ⇒com ⇒state ⇒nat ⇒bool" where Its_0: "¬bval b s =⇒Its b c s 0" | Its_Suc: "Jbval b s; (c,s) ⇒s’; Its b c s’ n K=⇒Its b c s (Suc n)" El comando thm Its.cases muestra un conjunto de reglas que pueden usarse como reglas de eliminación. Lema 4.5.1 La relación Its es funcional. lemma Its_fun: "Its b c s n =⇒Its b c s n’ =⇒n=n’" proof(induction arbitrary: n’ rule:Its.induct) case Its_0 thus ?case by (metis Its.cases) -- "Sledgehammer" next case Its_Suc thus ?case by(metis Its.simps big_step_determ) -- "Sledgehammer" qed Lema 4.5.2 Si el bucle WHILE b DO c termina, entonces el número de iteraciones nverifica Its b c s n. lemma WHILE_Its: "(WHILE b DO c,s) ⇒t=⇒ ∃n. Its b c s n" proof(induction "WHILE b DO c" s t rule: big_step_induct) case WhileFalse thus ?case by (metis Its_0) -- "Sledgehammer" next case WhileTrue thus ?case by (metis Its_Suc) -- "Sledgehammer" qed Lema 4.5.3 La precondición total más débil también es una precondición con respecto a la noción de demostrabilidad total. 119 Lógica de Hoare en Isabelle/HOL lemma wpt_is_pre: "`t {wpt c Q} c {Q}" proof (induction c arbitrary: Q) case SKIP show ?case by (auto simp:hoaret.Skip) next case Assign show ?case by (auto intro:hoaret.Assign) next case Seq thus ?case by (auto intro:hoaret.Seq) next case If thus ?case by (auto intro:hoaret.If hoaret.conseq) next case (While b c) let ?w = "WHILE b DO c" let ?T = "Its b c" have "∀s. wpt ?w Q s −→ wpt ?w Q s ∧(∃n. Its b c s n)" by (metis WHILE_Its wpt_def) -- "Sledgehammer" (* unfolding wpt_def by (metis WHILE_Its) *) moreover { fix n let ?R = "λs’. wpt ?w Q s’ ∧(∃n’<n. ?T s’ n’)" { fix s t assume "bval b s" and "?T s n" and "(?w, s) ⇒t" and "Q t" from ‘bval b s‘ and ‘(?w, s) ⇒t‘ obtain s’ where "(c,s) ⇒s’" "(?w,s’) ⇒t" by auto from ‘(?w, s’) ⇒t‘ obtain n’ where "?T s’ n’" by (blast dest: WHILE_Its) with ‘bval b s‘ and ‘(c, s) ⇒s’‘ have "?T s (Suc n’)" by (rule Its_Suc) with ‘?T s n‘ have "n = Suc n’" by (rule Its_fun) with ‘(c,s) ⇒s’‘ and ‘(?w,s’) ⇒t‘ and ‘Q t‘ and ‘?T s’ n’‘ have "wpt c ?R s" by (auto simp: wpt_def) } hence "∀s. wpt ?w Q s ∧bval b s ∧?T s n −→ wpt c ?R s" by (auto simp:wpt_def) note strengthen_pre[OF this While.IH] } note hoaret.While[OF this] moreover have "∀s. wpt ?w Q s ∧ ¬ bval b s −→ Q s" by (auto simp add:wpt_def) ultimately show ?case by (rule conseq) qed Comentarios sobre la demostración anterior: Observar que en el caso While, se usa Its como argumento para la terminación. Por lo tanto, se muestra en Isabelle/HOL el teorema de completitud para la corrección total. theorem hoaret_complete: "|=t {P}c{Q} =⇒ `t {P}c{Q}" 120 Lógica de Hoare en Isabelle/HOL apply(rule strengthen_pre[OF _ wpt_is_pre]) apply(auto simp: hoare_tvalid_def wpt_def) done De estos dos teoremas clave se sigue el siguiente resultado. corollary hoaret_sound_complete: "`t {P}c{Q} ←→ |=t {P}c{Q}" by (metis hoaret_sound hoaret_complete) 121