{"id":4671,"date":"2014-12-04T22:35:21","date_gmt":"2014-12-04T21:35:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4671"},"modified":"2014-12-15T22:37:41","modified_gmt":"2014-12-15T21:37:41","slug":"ra2014-demostraccion-en-isabelle-de-la-correccion-de-un-compilador","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-demostraccion-en-isabelle-de-la-correccion-de-un-compilador\/","title":{"rendered":"RA2014: Demostracci\u00f3n en Isabelle de la correcci\u00f3n de un compilador"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-14\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n de un compilador de expresiones aritm\u00e9ticas.<\/p>\n<p>La clase se ha basado en la siguiente teor\u00eda Isabelle<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* Tema 6: Caso de estudio: Compilaci\u00f3n de expresiones *}\n\ntheory T6\nimports Main\nbegin\n\ntext {*\n  El objetivo de este tema es contruir un compilador de expresiones\n  gen\u00e9ricas (construidas con variables, constantes y operaciones\n  binarias) a una m\u00e1quina de pila y demostrar su correcci\u00f3n.\n*}\n\nsection {* Las expresiones y el int\u00e9rprete *}\n\ntext {*\n  Definici\u00f3n. Las expresiones son las constantes, las variables\n  (representadas por n\u00fameros naturales) y las aplicaciones de operadores\n  binarios a dos expresiones. \n*}\n\ntype_synonym 'v binop = \"'v \u21d2 'v \u21d2 'v\"\n\ndatatype 'v expr = \n  Const 'v \n| Var nat \n| App \"'v binop\" \"'v expr\" \"'v expr\" \n\ntext {*\n  Definici\u00f3n. [Int\u00e9rprete] \n  La funci\u00f3n \"valor\" toma como argumentos una expresi\u00f3n y un entorno\n  (i.e. una aplicaci\u00f3n de las variables en elementos del lenguaje) y\n  devuelve el valor de la expresi\u00f3n en el entorno.\n*}\n\nfun valor :: \"'v expr \u21d2 (nat \u21d2 'v) \u21d2 'v\" where\n  \"valor (Const b) ent = b\"\n| \"valor (Var x) ent = ent x\"\n| \"valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))\"\n\ntext {*\n  Ejemplo. A continuaci\u00f3n mostramos algunos ejemplos de evaluaci\u00f3n con\n  el int\u00e9rprete. \n*}\n\nlemma \n  \"valor (Const 3) id = 3 \u2227\n   valor (Var 2) id = 2 \u2227\n   valor (Var 2) (\u03bbx. x+1) = 3 \u2227 \n   valor (App (op +) (Const 3) (Var 2)) (\u03bbx. x+1) = 6 \u2227\n   valor (App (op +) (Const 3) (Var 2)) (\u03bbx. x+4) = 9\" \nby simp\n\nsection {* La m\u00e1quina de pila *}\n\ntext {*\n  Nota. La m\u00e1quina de pila tiene tres clases de intrucciones:\n  \u00b7 cargar en la pila una constante,\n  \u00b7 cargar en la pila el contenido de una direcci\u00f3n y\n  \u00b7 aplicar un operador binario a los dos elementos superiores de la pila.\n*}\n\ndatatype 'v instr = \n  IConst 'v \n| ILoad nat \n| IApp \"'v binop\"\n\ntext {*\n  Definici\u00f3n. [Ejecuci\u00f3n]\n  La ejecuci\u00f3n de la m\u00e1quina de pila se modeliza mediante la funci\u00f3n \n  \"ejec\" que toma una lista de intrucciones, una memoria (representada \n  como una funci\u00f3n de las direcciones a los valores, an\u00e1logamente a los \n  entornos) y una pila (representada como una lista) y devuelve la pila\n  al final de la ejecuci\u00f3n.\n*}\n\nfun ejec :: \"'v instr list \u21d2 (nat\u21d2'v) \u21d2 'v list \u21d2 'v list\" where\n  \"ejec [] ent vs = vs\"\n| \"ejec (i#is) ent vs = \n     (case i of\n        IConst v \u21d2 ejec is ent (v#vs)\n      | ILoad x \u21d2 ejec is ent ((ent x)#vs)\n      | IApp f \u21d2 ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))\"\n\ntext {* \n  A continuaci\u00f3n se muestran ejemplos de ejecuci\u00f3n.\n*}\n\nlemma\n  \"ejec [IConst 3] id [7] = [3,7] \u2227\n   ejec [ILoad 2, IConst 3] id [7] = [3,2,7] \u2227\n   ejec [ILoad 2, IConst 3] (\u03bbx. x+4) [7] = [3,6,7] \u2227\n   ejec [ILoad 2, IConst 3, IApp (op +)] (\u03bbx. x+4) [7] = [9,7]\"\nby simp\n\nsection {* El compilador *}\n\ntext {*\n  Definici\u00f3n. El compilador \"comp\" traduce una expresi\u00f3n en una lista de\n  instrucciones. \n*}\n\nfun comp :: \"'v expr \u21d2 'v instr list\" where\n  \"comp (Const v) = [IConst v]\"\n| \"comp (Var x) = [ILoad x]\"\n| \"comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]\"\n\ntext {*\n  A continuaci\u00f3n se muestran ejemplos de compilaci\u00f3n.\n*}\n\nlemma\n  \"comp (Const 3) = [IConst 3] \u2227\n   comp (Var 2) = [ILoad 2] \u2227\n   comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]\"\nby simp\n\nsection {* Correcci\u00f3n del compilador *}\n\ntext {*\n  Para demostrar que el compilador es correcto, probamos que el\n  resultado de compilar una expresi\u00f3n y a continuaci\u00f3n ejecutarla es lo\n  mismo que interpretarla; es decir, \n*}\n\ntheorem \"ejec (comp e) ent [] = [valor e ent]\" \noops\n\ntext {*\n  El teorema anterior no puede demostrarse por inducci\u00f3n en e. Para\n  demostrarlo, lo generalizamos a\n*}\n\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\noops\n\ntext {*\n  En la demostraci\u00f3n del teorema anterior usaremos el siguiente lema.\n*}\n\nlemma ejec_append:\n  \"\u2200 vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" (is \"?P xs\")\nproof (induct xs)\n  show \"?P []\" by simp\nnext\n  fix a xs\n  assume \"?P xs\"\n  thus \"?P (a#xs)\" by (cases \"a\", auto)\nqed\n\n-- \"La demostraci\u00f3n detallada es\" \nlemma ejec_append_1:\n  \"\u2200 vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" (is \"?P xs\")\nproof (induct xs)\n  show \"?P []\" by simp\nnext\n  fix a xs\n  assume HI: \"?P xs\"\n  thus \"?P (a#xs)\"\n  proof (cases \"a\")\n    case IConst thus ?thesis using HI by simp\n  next\n    case ILoad thus ?thesis using HI by simp\n  next\n    case IApp thus ?thesis using HI by simp\n  qed\nqed\n\ntext {*\n  Una demostraci\u00f3n m\u00e1s detallada del lema es la siguiente:\n*}\n\nlemma ejec_append_2:\n  \"\u2200vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" (is \"?P xs\")\nproof (induct xs)\n  show \"?P []\" by simp\nnext\n  fix a xs\n  assume HI: \"?P xs\"\n  thus \"?P (a#xs)\"\n  proof (cases \"a\")\n    fix v assume C1: \"a=IConst v\"\n    show \" \u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\n    proof\n      fix vs\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs\"\n        using C1 by simp\n      also have \"\u2026 = ejec (xs@ys) ent (v#vs)\" by simp\n      also have \"\u2026 = ejec ys ent (ejec xs ent (v#vs))\" using HI by simp\n      also have \"\u2026 = ejec ys ent (ejec ((IConst v)#xs) ent vs)\" by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C1 by simp\n      finally show \"ejec ((a#xs)@ys) ent vs = \n                    ejec ys ent (ejec (a#xs) ent vs)\" .\n    qed\n  next\n    fix n assume C2: \"a=ILoad n\"\n    show \" \u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\n    proof\n      fix vs\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs\"\n        using C2 by simp\n      also have \"\u2026 = ejec (xs@ys) ent ((ent n)#vs)\" by simp\n      also have \"\u2026 = ejec ys ent (ejec xs ent ((ent n)#vs))\" using HI by simp\n      also have \"\u2026 = ejec ys ent (ejec ((ILoad n)#xs) ent vs)\" by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C2 by simp\n      finally show \"ejec ((a#xs)@ys) ent vs = \n                    ejec ys ent (ejec (a#xs) ent vs)\" .\n    qed\n  next\n    fix f assume C3: \"a=IApp f\"\n    show \"\u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\n    proof\n      fix vs\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs\"\n        using C3 by simp\n      also have \"\u2026 = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))\" \n        by simp\n      also have \"\u2026 = ejec ys \n                          ent \n                          (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))\" \n        using HI by simp\n      also have \"\u2026 = ejec ys ent (ejec ((IApp f)#xs) ent vs)\" by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C3 by simp\n      finally show \"ejec ((a#xs)@ys) ent vs = \n                    ejec ys ent (ejec (a#xs) ent vs)\" .\n    qed\n  qed\nqed\n\ntext {*\n  La demostraci\u00f3n autom\u00e1tica del teorema es\n*}\n\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\nby (induct e) (auto simp add:ejec_append)\n\ntext {*\n  La demostraci\u00f3n estructurada del teorema es\n*}\n\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\nproof (induct e)\n  fix v\n  show \"\u2200vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs\" by simp\nnext\n  fix x\n  show \"\u2200vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs\" by simp\nnext\n  fix f e1 e2\n  assume HI1: \"\u2200vs. ejec (comp e1) ent vs = (valor e1 ent) # vs\"\n    and HI2: \"\u2200vs. ejec (comp e2) ent vs = (valor e2 ent) # vs\"\n  show \"\u2200vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs\"\n  proof\n    fix vs\n    have \"ejec (comp (App f e1 e2)) ent vs\n          = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs\" by simp\n    also have \"\u2026 = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)\"\n      using ejec_append by blast\n    also have \"\u2026 = ejec [IApp f] \n                         ent \n                         (ejec (comp e1) ent (ejec (comp e2) ent vs))\" \n      using ejec_append by blast\n    also have \"\u2026 =  ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))\"\n      using HI2 by simp\n    also have \"\u2026 = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))\"\n      using HI1 by simp\n    also have \"\u2026 = (f (valor e1 ent) (valor e2 ent))#vs\" by simp\n    also have \"\u2026 = (valor (App f e1 e2) ent) # vs\" by simp\n    finally \n    show \"ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs\" \n      by blast\n  qed\nqed\n\nend\n<\/pre>\n<p>Como tarea se ha propuesto los ejercicios de la <a href=\"http:\/\/bit.ly\/1yTutOq\">relaci\u00f3n 8<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n de un compilador de expresiones aritm\u00e9ticas. La clase se ha basado en la siguiente teor\u00eda Isabelle<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[240],"tags":[144,307],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4671"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4671"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4671\/revisions"}],"predecessor-version":[{"id":4672,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4671\/revisions\/4672"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4671"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4671"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4671"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}