Preuve de la correction du mini compilateur d'expression présenté dans l'épisode Program correctness de Computerphile.
theory MiniCompiler imports Main begin text‹ Proof of the correction of the mini compiler presented in https://www.youtube.com/watch?v=T_IINWzQhow › text‹ Simple expressions: integer constants and sums of expressions › datatype Expr = Val int | Add Expr Expr text‹ Value of an expression › primrec eval where ‹eval (Val n) = n› | ‹eval (Add x y) = eval x + eval y› text‹ Operations of the execution machine: ▪ push an integer on the stack ▪ pop two integers and push their sum › datatype Op = PUSH int | ADD text‹ Compile an expression into a list of operations of the execution machine › primrec comp where ‹comp (Val n) = [PUSH n]› | ‹comp (Add x y) = comp x @ comp y @ [ADD]› text‹ Execute a list of operations on a stack s › fun exec where ‹exec (PUSH n # p) s = exec p (n # s)› | ‹exec (ADD # p) (m # n # s) = exec p ((n + m) # s)› | ‹exec _ s = s› (* all other possibilities leave the stack unchanged *) text‹Examples› abbreviation ‹e1 ≡ Val 1› abbreviation ‹e2 ≡ Add (Val 2) (Val 3)› abbreviation ‹e3 ≡ Add e2 (Val 4)› value ‹eval e1› (* 1::int *) value ‹eval e2› (* 5::int *) value ‹eval e3› (* 9::int *) value ‹comp e1› (* [PUSH 1] :: Op list *) value ‹exec (comp e1) []› (* [1] :: int list *) value ‹comp e2› (* [PUSH 2, PUSH 3, ADD] :: Op list *) value ‹exec (comp e2) []› (* [5] :: int list *) value ‹comp e3› (* [PUSH 2, PUSH 3, ADD, PUSH 4, ADD]] :: Op list *) value ‹exec (comp e3) []› (* [9] :: int list *) text‹ The compilation of an expression is correct iff executing the generated list of operations starting with any stack yields an identical stack with only the value of the expression pushed onto it. › definition ‹correct ≡ (∀e::Expr. ∀ stack::int list. exec (comp e) stack = (eval e)#stack)› text‹ Because the compilation of an expression requires the compilation of its subexpressions we need to consider the execution of the code of an expression followed by other code for the induction to work well. We first show that executing a compiled expression followed by some program p amounts to executing after pushing the value off the expression on the stack. › lemma exec_val: ‹exec ((comp expr1)@p) s = exec p ((eval expr1)#s)› (* by (induction expr1 arbitrary: p s, simp_all) *) proof (induction expr1 arbitrary: p s) ― ‹"arbitrary: p s" makes the induction hypothesis stronger. You can check what it does by looking at Add.IH with and without the arbitrary option.› case (Val x) then show ?case by simp next case (Add expr11 expr12) thm Add.IH have ‹exec (comp (Add expr11 expr12) @ p) s = exec ((comp expr11) @ (comp expr12) @ [ADD] @ p) s› by simp also have ‹... = exec ((comp expr12) @ [ADD] @ p) ((eval expr11) # s)› using Add.IH(1) by simp also have ‹... = exec ([ADD] @ p) ((eval expr12) # (eval expr11) # s)› using Add.IH(2) by simp also have ‹... = exec (ADD # p) ((eval expr12) # (eval expr11) # s)› by simp also have ‹... = exec p (((eval expr11) + (eval expr12)) # s)› by simp also have ‹... = exec p ((eval (Add expr11 expr12)) # s)› by simp finally show ?case . qed text‹ We can now show that any expression is compiled correctly: our compiler is correct. › theorem ‹correct› unfolding correct_def using exec_val[where p=‹[]›] by simp end