Menu Close

RA2018: Demostración en Isabelle de la corrección de un compilador

En la segunda parte de 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

chapter {* Tema 10: Caso de estudio: Compilación de expresiones *}
 
theory T10_Caso_de_estudio_Compilacion_de_expresiones
 
imports Main
begin
 
declare [[names_short]]
 
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 (+) (Const 3) (Var 2)) (λx. x+1) = 6 ∧
   valor (App (+) (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 (+)] (λ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 (+) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (+)]"
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]" 
  apply (induct e)
  apply auto
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"
  then show "?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"
  then show "?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"
  then show "?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
RA2018