{"id":7026,"date":"2020-02-13T17:22:54","date_gmt":"2020-02-13T16:22:54","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7026"},"modified":"2020-02-16T17:23:32","modified_gmt":"2020-02-16T16:23:32","slug":"ra2019-demostracion-en-isabelle-de-la-correccion-de-un-compilador","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-demostracion-en-isabelle-de-la-correccion-de-un-compilador\/","title":{"rendered":"RA2019: Demostraci\u00f3n en Isabelle de la correcci\u00f3n de un compilador"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">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<\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 10: Caso de estudio: Compilaci\u00f3n de expresiones\u203a\n\ntheory T10_Caso_de_estudio_Compilacion_de_expresiones\n\nimports Main\nbegin\n\ntext \u2039El 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.\u203a\n\nsection \u2039Las expresiones y el int\u00e9rprete\u203a\n\ntext \u2039Definici\u00f3n. Las expresiones son las constantes, las variables\n  (representadas por n\u00fameros naturales) y las aplicaciones de operadores\n  binarios a dos expresiones.\u203a\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 \u2039Definici\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.\u203a\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 \u2039Ejemplo. A continuaci\u00f3n mostramos algunos ejemplos de evaluaci\u00f3n \n  con el int\u00e9rprete.\u203a\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 (+) (Const 3) (Var 2)) (\u03bbx. x+1) = 6 \u2227\n   valor (App (+) (Const 3) (Var 2)) (\u03bbx. x+4) = 9\" \n  by simp\n\nsection \u2039La m\u00e1quina de pila\u203a\n\ntext \u2039Nota. 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 \n    pila.\u203a\n\ndatatype 'v instr = \n  IConst 'v \n| ILoad nat \n| IApp \"'v binop\"\n\ntext \u2039Definici\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.\u203a\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 \u2039  A continuaci\u00f3n se muestran ejemplos de ejecuci\u00f3n.\u203a\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 (+)] (\u03bbx. x+4) [7] = [9,7]\"\n  by simp\n\nsection \u2039El compilador\u203a\n\ntext \u2039Definici\u00f3n. El compilador \"comp\" traduce una expresi\u00f3n en una \n  lista de instrucciones.\u203a\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 \u2039A continuaci\u00f3n se muestran ejemplos de compilaci\u00f3n.\u203a\n\nlemma\n  \"comp (Const 3)                   = [IConst 3] \u2227\n   comp (Var 2)                     = [ILoad 2] \u2227\n   comp (App (+) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (+)]\"\n  by simp\n\nsection \u2039Correcci\u00f3n del compilador\u203a\n\ntext \u2039Para 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,\u203a\n\ntheorem \"ejec (comp e) ent [] = [valor e ent]\" \n  apply (induct e)\n    apply auto\n  oops\n\ntext \u2039El teorema anterior no puede demostrarse por inducci\u00f3n en e. Para\n  demostrarlo, lo generalizamos a\u203a\n\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\n  oops\n\ntext \u2039En la demostraci\u00f3n del teorema anterior usaremos el siguiente \n  lema.\u203a\n\nlemma\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  then show \"?P (a#xs)\" by (cases \"a\", auto)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a \nlemma \n  \"\u2200 vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" \nproof (induct xs)\n  case Nil\n  then show ?case \n    by simp\nnext\n  case (Cons a xs)\n  then show ?case \n    by (cases \"a\"; simp)\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a \nlemma \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  then show \"?P (a#xs)\"\n  proof (cases \"a\")\n    case (IConst x1)\n    then show ?thesis using HI by simp\n  next\n    case (ILoad x2)\n    then show ?thesis using HI by simp\n  next\n    case (IApp x3)\n    then show ?thesis using HI by simp\n  qed\nqed\n\n\u2015 \u2039Una demostraci\u00f3n m\u00e1s detallada del lema es la siguiente:\u203a\nlemma ejec_append:\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  then show \"?P (a#xs)\"\n  proof (cases \"a\")\n    fix v \n    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)\" \n        by simp\n      also have \"\u2026 = ejec ys ent (ejec xs ent (v#vs))\" \n        using HI by simp\n      also have \"\u2026 = ejec ys ent (ejec ((IConst v)#xs) ent vs)\" \n        by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C1 \n        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 \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)\" \n        by simp\n      also have \"\u2026 = ejec ys ent (ejec xs ent ((ent n)#vs))\" \n        using HI by simp\n      also have \"\u2026 = ejec ys ent (ejec ((ILoad n)#xs) ent vs)\" \n        by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" \n        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 \n    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)\" \n        by simp\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" \n        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 \u2039La demostraci\u00f3n autom\u00e1tica del teorema es\u203a\n\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\n  by (induct e) (auto simp add: ejec_append)\n\ntext \u2039La demostraci\u00f3n estructurada del teorema es\u203a\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\nproof (induct e)\n  case (Const x)\n  then show ?case by simp\nnext\n  case (Var x)\n  then show ?case by simp\nnext\n  case (App x1a e1 e2)\n  then show ?case by (simp add: ejec_append)\nqed\n\ntext \u2039La demostraci\u00f3n detallada del teorema es\u203a\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\" \n    by simp\nnext\n  fix x\n  show \"\u2200vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs\" \n    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 = \n             (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\" \n      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","protected":false},"excerpt":{"rendered":"<p>En la primera parte de 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 chapter \u2039Tema 10: Caso de estudio: Compilaci\u00f3n de expresiones\u203a theory T10_Caso_de_estudio_Compilacion_de_expresiones imports Main begin text \u2039El&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[333],"tags":[],"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\/7026"}],"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=7026"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7026\/revisions"}],"predecessor-version":[{"id":7028,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7026\/revisions\/7028"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7026"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7026"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7026"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}