{"id":1890,"date":"2012-02-16T19:57:50","date_gmt":"2012-02-16T19:57:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1890"},"modified":"2013-03-08T05:48:55","modified_gmt":"2013-03-08T05:48:55","slug":"ra2011-demostraccion-en-isabelle-de-la-correccion-de-un-compilador","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2011-demostraccion-en-isabelle-de-la-correccion-de-un-compilador\/","title":{"rendered":"RA2011: Demostracci\u00f3n en Isabelle de la correcci\u00f3n de un compilador"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-11\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n d 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\">\r\nheader {* Tema 11: Caso de estudio: Compilaci\u00f3n de expresiones *}\r\n\r\ntheory Tema_11\r\nimports Main\r\nbegin\r\n\r\ntext {*\r\n  El objetivo de este tema es contruir un compilador de expresiones\r\n  gen\u00e9ricas (construidas con variables, constantes y operaciones\r\n  binarias) a una m\u00e1quina de pila y demostrar su correcci\u00f3n.\r\n*}\r\n\r\nsection {* Las expresiones y el int\u00e9rprete *}\r\n\r\ntext {*\r\n  Definici\u00f3n. Las expresiones son las constantes, las variables\r\n  (representadas por n\u00fameros naturales) y las aplicaciones de operadores\r\n  binarios a dos expresiones. \r\n*}\r\n\r\ntypes 'v binop = \"'v \u21d2 'v \u21d2 'v\"\r\ndatatype 'v expr = \r\n    Const 'v \r\n  | Var nat \r\n  | App \"'v binop\" \"'v expr\" \"'v expr\" \r\n\r\ntext {*\r\n  Definici\u00f3n. [Int\u00e9rprete] \r\n  La funci\u00f3n \"valor\" toma como argumentos una expresi\u00f3n y un entorno\r\n  (i.e. una aplicaci\u00f3n de las variables en elementos del lenguaje) y\r\n  devuelve el valor de la expresi\u00f3n en el entorno.\r\n*}\r\n\r\nprimrec valor :: \"'v expr \u21d2 (nat \u21d2 'v) \u21d2 'v\" where\r\n  \"valor (Const b) ent = b\"\r\n| \"valor (Var x) ent = ent x\"\r\n| \"valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))\"\r\n\r\ntext {*\r\n  Ejemplo. A continuaci\u00f3n mostramos algunos ejemplos de evaluaci\u00f3n con\r\n  el int\u00e9rprete. \r\n*}\r\n\r\nlemma \r\n  \"valor (Const 3) id = 3 \u2227\r\n  valor (Var 2) id = 2 \u2227\r\n  valor (Var 2) (\u03bbx. x+1) = 3 \u2227 \r\n  valor (App (op +) (Const 3) (Var 2)) (\u03bbx. x+1) = 6 \u2227\r\n  valor (App (op +) (Const 3) (Var 2)) (\u03bbx. x+4) = 9\" \r\nby simp\r\n\r\nsection {* La m\u00e1quina de pila *}\r\n\r\ntext {*\r\n  Nota. La m\u00e1quina de pila tiene tres clases de intrucciones:\r\n  \u00b7 cargar en la pila una constante,\r\n  \u00b7 cargar en la pila el contenido de una direcci\u00f3n y\r\n  \u00b7 aplicar un operador binario a los dos elementos superiores de la pila.\r\n*}\r\n\r\ndatatype 'v instr = \r\n    IConst 'v \r\n  | ILoad nat \r\n  | IApp \"'v binop\"\r\n\r\ntext {*\r\n  Definici\u00f3n. [Ejecuci\u00f3n]\r\n  La ejecuci\u00f3n de la m\u00e1quina de pila se modeliza mediante la funci\u00f3n\r\n  \"ejec\" que toma una lista de intrucciones, una memoria (representada\r\n  como una funci\u00f3n de las direcciones a los valores, an\u00e1logamente a los\r\n  entornos) y una pila (representada como una lista) y devuelve la pila al\r\n  final de la ejecuci\u00f3n.\r\n*}\r\n\r\nprimrec ejec :: \"'v instr list \u21d2 (nat\u21d2'v) \u21d2 'v list \u21d2 'v list\" where\r\n  \"ejec [] ent vs = vs\"\r\n| \"ejec (i#is) ent vs = \r\n     (case i of\r\n        IConst v \u21d2 ejec is ent (v#vs)\r\n      | ILoad x \u21d2 ejec is ent ((ent x)#vs)\r\n      | IApp f \u21d2 ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))\"\r\n\r\ntext {* \r\n  A continuaci\u00f3n se muestran ejemplos de ejecuci\u00f3n.\r\n*}\r\n\r\nlemma\r\n  \"ejec [IConst 3] id [7] = [3,7] \u2227\r\n  ejec [ILoad 2, IConst 3] id [7] = [3,2,7] \u2227\r\n  ejec [ILoad 2, IConst 3] (\u03bbx. x+4) [7] = [3,6,7] \u2227\r\n  ejec [ILoad 2, IConst 3, IApp (op +)] (\u03bbx. x+4) [7] = [9,7]\"\r\nby simp\r\n\r\nsection {* El compilador *}\r\n\r\ntext {*\r\n  Definici\u00f3n. El compilador \"comp\" traduce una expresi\u00f3n en una lista de\r\n  instrucciones. \r\n*}\r\n\r\nprimrec comp :: \"'v expr \u21d2 'v instr list\" where\r\n  \"comp (Const v) = [IConst v]\"\r\n| \"comp (Var x) = [ILoad x]\"\r\n| \"comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]\"\r\n\r\ntext {*\r\n  A continuaci\u00f3n se muestran ejemplos de compilaci\u00f3n.\r\n*}\r\n\r\nlemma\r\n  \"comp (Const 3) = [IConst 3] \u2227\r\n  comp (Var 2) = [ILoad 2] \u2227\r\n  comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]\"\r\nby simp\r\n\r\nsection {* Correcci\u00f3n del compilador *}\r\n\r\ntext {*\r\n  Para demostrar que el compilador es correcto, probamos que el resultado de\r\n  compilar una expresi\u00f3n y a continuaci\u00f3n ejecutarla es lo mismo que\r\n  interpretarla; es decir, \r\n*}\r\n\r\ntheorem \"ejec (comp e) ent [] = [valor e ent]\" \r\noops\r\n\r\ntext {*\r\n  El teorema anterior no puede demostrarse por inducci\u00f3n en e. Para\r\n  demostrarlo por inducci\u00f3n, lo generalizamos a\r\n*}\r\n\r\ntheorem \"\u2200vs. ejec (comp e) ent vs = (valor e ent)#vs\"\r\noops\r\n\r\ntext {*\r\n  En la demostraci\u00f3n del teorema anterior usaremos el siguiente lema.\r\n*}\r\n\r\nlemma ejec_append:\r\n  \"\u2200 vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" (is \"?P xs\")\r\nproof (induct xs)\r\n  show \"?P []\" by simp\r\nnext\r\n  fix a xs\r\n  assume HI: \"?P xs\"\r\n  thus \"?P (a#xs)\"\r\n  proof (cases \"a\")\r\n    case IConst thus ?thesis using HI by simp\r\n  next\r\n    case ILoad thus ?thesis using HI by simp\r\n  next\r\n    case IApp thus ?thesis using HI by simp\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  Una demostraci\u00f3n m\u00e1s detallada del lema es la siguiente:\r\n*}\r\n\r\nlemma ejec_append_2:\r\n  \"\u2200 vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)\" (is \"?P xs\")\r\nproof (induct xs)\r\n  show \"?P []\" by simp\r\nnext\r\n  fix a xs\r\n  assume HI: \"?P xs\"\r\n  thus \"?P (a#xs)\"\r\n  proof (cases \"a\")\r\n    fix v assume C1: \"a=IConst v\"\r\n    show \" \u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\r\n    proof\r\n      fix vs\r\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs\"\r\n        using C1 by simp\r\n      also have \"\u2026 = ejec (xs@ys) ent (v#vs)\" by simp\r\n      also have \"\u2026 = ejec ys ent (ejec xs ent (v#vs))\" using HI by simp\r\n      also have \"\u2026 = ejec ys ent (ejec ((IConst v)#xs) ent vs)\" by simp\r\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C1 by simp\r\n      finally show \"ejec ((a#xs)@ys) ent vs = \r\n                    ejec ys ent (ejec (a#xs) ent vs)\" .\r\n    qed\r\n  next\r\n    fix n assume C2: \"a=ILoad n\"\r\n    show \" \u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\r\n    proof\r\n      fix vs\r\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs\"\r\n        using C2 by simp\r\n      also have \"\u2026 = ejec (xs@ys) ent ((ent n)#vs)\" by simp\r\n      also have \"\u2026 = ejec ys ent (ejec xs ent ((ent n)#vs))\" using HI by simp\r\n      also have \"\u2026 = ejec ys ent (ejec ((ILoad n)#xs) ent vs)\" by simp\r\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C2 by simp\r\n      finally show \"ejec ((a#xs)@ys) ent vs = \r\n                    ejec ys ent (ejec (a#xs) ent vs)\" .\r\n    qed\r\n  next\r\n    fix f assume C3: \"a=IApp f\"\r\n    show \"\u2200vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)\"\r\n    proof\r\n      fix vs\r\n      have \"ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs\"\r\n        using C3 by simp\r\n      also have \"\u2026 = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))\" \r\n        by simp\r\n      also have \"\u2026 = ejec ys \r\n                          ent \r\n                          (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))\" \r\n        using HI by simp\r\n      also have \"\u2026 = ejec ys ent (ejec ((IApp f)#xs) ent vs)\" by simp\r\n      also have \"\u2026 = ejec ys ent (ejec (a#xs) ent vs)\" using C3 by simp\r\n      finally show \"ejec ((a#xs)@ys) ent vs = \r\n                    ejec ys ent (ejec (a#xs) ent vs)\" .\r\n    qed\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  La demostraci\u00f3n del teorema es la siguiente\r\n*}\r\n\r\ntheorem \"\u2200 vs. ejec (comp e) ent vs = (valor e ent)#vs\"\r\nproof (induct e)\r\n  fix v\r\n  show \"\u2200vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs\" by simp\r\nnext\r\n  fix x\r\n  show \"\u2200vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs\" by simp\r\nnext\r\n  fix f e1 e2\r\n  assume HI1: \"\u2200vs. ejec (comp e1) ent vs = (valor e1 ent) # vs\"\r\n    and HI2: \"\u2200vs. ejec (comp e2) ent vs = (valor e2 ent) # vs\"\r\n  show \"\u2200vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs\"\r\n  proof\r\n    fix vs\r\n    have \"ejec (comp (App f e1 e2)) ent vs\r\n          = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs\" by simp\r\n    also have \"\u2026 = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)\"\r\n      using ejec_append by blast\r\n    also have \"\u2026 = ejec [IApp f] \r\n                         ent \r\n                         (ejec (comp e1) ent (ejec (comp e2) ent vs))\" \r\n      using ejec_append by blast\r\n    also have \"\u2026 =  ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))\"\r\n      using HI2 by simp\r\n    also have \"\u2026 = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))\"\r\n      using HI1 by simp\r\n    also have \"\u2026 = (f (valor e1 ent) (valor e2 ent))#vs\" by simp\r\n    also have \"\u2026 = (valor (App f e1 e2) ent) # vs\" by simp\r\n    finally \r\n    show \"ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs\" \r\n      by blast\r\n  qed\r\nqed\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo demostrar en Isabelle la correcci\u00f3n d 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":"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":[187],"tags":[296],"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\/1890"}],"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=1890"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1890\/revisions"}],"predecessor-version":[{"id":2853,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1890\/revisions\/2853"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1890"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1890"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1890"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}