RA2013: Demostración en Isabelle de la corrección de un compilador
En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.
La clase se ha basado en la siguiente teoría Isabelle
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 |
header {* Tema 8: Caso de estudio: Compilación de expresiones *} theory T8 imports Main begin text {* El objetivo de este tema es contruir un compilador de expresiones genéricas (construidas con variables, constantes y operaciones binarias) a una máquina de pila y demostrar su corrección. *} section {* Las expresiones y el intérprete *} text {* Definición. Las expresiones son las constantes, las variables (representadas por números naturales) y las aplicaciones de operadores binarios a dos expresiones. *} type_synonym 'v binop = "'v ⇒ 'v ⇒ 'v" datatype 'v expr = Const 'v | Var nat | App "'v binop" "'v expr" "'v expr" text {* Definición. [Intérprete] La función "valor" toma como argumentos una expresión y un entorno (i.e. una aplicación de las variables en elementos del lenguaje) y devuelve el valor de la expresión en el entorno. *} fun valor :: "'v expr ⇒ (nat ⇒ 'v) ⇒ 'v" where "valor (Const b) ent = b" | "valor (Var x) ent = ent x" | "valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))" text {* Ejemplo. A continuación mostramos algunos ejemplos de evaluación con el intérprete. *} lemma "valor (Const 3) id = 3 ∧ valor (Var 2) id = 2 ∧ valor (Var 2) (λx. x+1) = 3 ∧ valor (App (op +) (Const 3) (Var 2)) (λx. x+1) = 6 ∧ valor (App (op +) (Const 3) (Var 2)) (λx. x+4) = 9" by simp section {* La máquina de pila *} text {* Nota. La máquina de pila tiene tres clases de intrucciones: · cargar en la pila una constante, · cargar en la pila el contenido de una dirección y · aplicar un operador binario a los dos elementos superiores de la pila. *} datatype 'v instr = IConst 'v | ILoad nat | IApp "'v binop" text {* Definición. [Ejecución] La ejecución de la máquina de pila se modeliza mediante la función "ejec" que toma una lista de intrucciones, una memoria (representada como una función de las direcciones a los valores, análogamente a los entornos) y una pila (representada como una lista) y devuelve la pila al final de la ejecución. *} fun ejec :: "'v instr list ⇒ (nat⇒'v) ⇒ 'v list ⇒ 'v list" where "ejec [] ent vs = vs" | "ejec (i#is) ent vs = (case i of IConst v ⇒ ejec is ent (v#vs) | ILoad x ⇒ ejec is ent ((ent x)#vs) | IApp f ⇒ ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" text {* A continuación se muestran ejemplos de ejecución. *} lemma "ejec [IConst 3] id [7] = [3,7] ∧ ejec [ILoad 2, IConst 3] id [7] = [3,2,7] ∧ ejec [ILoad 2, IConst 3] (λx. x+4) [7] = [3,6,7] ∧ ejec [ILoad 2, IConst 3, IApp (op +)] (λx. x+4) [7] = [9,7]" by simp section {* El compilador *} text {* Definición. El compilador "comp" traduce una expresión en una lista de instrucciones. *} fun comp :: "'v expr ⇒ 'v instr list" where "comp (Const v) = [IConst v]" | "comp (Var x) = [ILoad x]" | "comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]" text {* A continuación se muestran ejemplos de compilación. *} lemma "comp (Const 3) = [IConst 3] ∧ comp (Var 2) = [ILoad 2] ∧ comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]" by simp section {* Corrección del compilador *} text {* Para demostrar que el compilador es correcto, probamos que el resultado de compilar una expresión y a continuación ejecutarla es lo mismo que interpretarla; es decir, *} theorem "ejec (comp e) ent [] = [valor e ent]" oops text {* El teorema anterior no puede demostrarse por inducción en e. Para demostrarlo, lo generalizamos a *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" oops text {* En la demostración del teorema anterior usaremos el siguiente lema. *} lemma ejec_append: "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume "?P xs" thus "?P (a#xs)" by (cases "a", auto) qed -- "La demostración detallada es" lemma ejec_append_1: "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume HI: "?P xs" thus "?P (a#xs)" proof (cases "a") case IConst thus ?thesis using HI by simp next case ILoad thus ?thesis using HI by simp next case IApp thus ?thesis using HI by simp qed qed text {* Una demostración más detallada del lema es la siguiente: *} lemma ejec_append_2: "∀vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs") proof (induct xs) show "?P []" by simp next fix a xs assume HI: "?P xs" thus "?P (a#xs)" proof (cases "a") fix v assume C1: "a=IConst v" show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs" using C1 by simp also have "… = ejec (xs@ys) ent (v#vs)" by simp also have "… = ejec ys ent (ejec xs ent (v#vs))" using HI by simp also have "… = ejec ys ent (ejec ((IConst v)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C1 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed next fix n assume C2: "a=ILoad n" show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs" using C2 by simp also have "… = ejec (xs@ys) ent ((ent n)#vs)" by simp also have "… = ejec ys ent (ejec xs ent ((ent n)#vs))" using HI by simp also have "… = ejec ys ent (ejec ((ILoad n)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C2 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed next fix f assume C3: "a=IApp f" show "∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" proof fix vs have "ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs" using C3 by simp also have "… = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))" by simp also have "… = ejec ys ent (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" using HI by simp also have "… = ejec ys ent (ejec ((IApp f)#xs) ent vs)" by simp also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C3 by simp finally show "ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)" . qed qed qed text {* La demostración automática del teorema es *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" by (induct e) (auto simp add:ejec_append) text {* La demostración estructurada del teorema es *} theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs" proof (induct e) fix v show "∀vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs" by simp next fix x show "∀vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs" by simp next fix f e1 e2 assume HI1: "∀vs. ejec (comp e1) ent vs = (valor e1 ent) # vs" and HI2: "∀vs. ejec (comp e2) ent vs = (valor e2 ent) # vs" show "∀vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" proof fix vs have "ejec (comp (App f e1 e2)) ent vs = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs" by simp also have "… = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)" using ejec_append by blast also have "… = ejec [IApp f] ent (ejec (comp e1) ent (ejec (comp e2) ent vs))" using ejec_append by blast also have "… = ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))" using HI2 by simp also have "… = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))" using HI1 by simp also have "… = (f (valor e1 ent) (valor e2 ent))#vs" by simp also have "… = (valor (App f e1 e2) ent) # vs" by simp finally show "ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" by blast qed qed end |
Como tarea se ha propuesto los ejercicios de la relación 12.