summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Expr_Compiler.thy

author | hoelzl |

Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) | |

changeset 51526 | 155263089e7b |

parent 46582 | dcc312f22ee8 |

child 55640 | abc140f21caa |

permissions | -rw-r--r-- |

move SEQ.thy and Lim.thy to Limits.thy

1 (* Title: HOL/Isar_Examples/Expr_Compiler.thy

2 Author: Markus Wenzel, TU Muenchen

4 Correctness of a simple expression/stack-machine compiler.

5 *)

7 header {* Correctness of a simple expression compiler *}

9 theory Expr_Compiler

10 imports Main

11 begin

13 text {* This is a (rather trivial) example of program verification.

14 We model a compiler for translating expressions to stack machine

15 instructions, and prove its correctness wrt.\ some evaluation

16 semantics. *}

19 subsection {* Binary operations *}

21 text {* Binary operations are just functions over some type of values.

22 This is both for abstract syntax and semantics, i.e.\ we use a

23 ``shallow embedding'' here. *}

25 type_synonym 'val binop = "'val => 'val => 'val"

28 subsection {* Expressions *}

30 text {* The language of expressions is defined as an inductive type,

31 consisting of variables, constants, and binary operations on

32 expressions. *}

34 datatype ('adr, 'val) expr =

35 Variable 'adr

36 | Constant 'val

37 | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"

39 text {* Evaluation (wrt.\ some environment of variable assignments) is

40 defined by primitive recursion over the structure of expressions. *}

42 primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"

43 where

44 "eval (Variable x) env = env x"

45 | "eval (Constant c) env = c"

46 | "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"

49 subsection {* Machine *}

51 text {* Next we model a simple stack machine, with three

52 instructions. *}

54 datatype ('adr, 'val) instr =

55 Const 'val

56 | Load 'adr

57 | Apply "'val binop"

59 text {* Execution of a list of stack machine instructions is easily

60 defined as follows. *}

62 primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"

63 where

64 "exec [] stack env = stack"

65 | "exec (instr # instrs) stack env =

66 (case instr of

67 Const c => exec instrs (c # stack) env

68 | Load x => exec instrs (env x # stack) env

69 | Apply f => exec instrs (f (hd stack) (hd (tl stack))

70 # (tl (tl stack))) env)"

72 definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"

73 where "execute instrs env = hd (exec instrs [] env)"

76 subsection {* Compiler *}

78 text {* We are ready to define the compilation function of expressions

79 to lists of stack machine instructions. *}

81 primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"

82 where

83 "compile (Variable x) = [Load x]"

84 | "compile (Constant c) = [Const c]"

85 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"

88 text {* The main result of this development is the correctness theorem

89 for @{text compile}. We first establish a lemma about @{text exec}

90 and list append. *}

92 lemma exec_append:

93 "exec (xs @ ys) stack env =

94 exec ys (exec xs stack env) env"

95 proof (induct xs arbitrary: stack)

96 case Nil

97 show ?case by simp

98 next

99 case (Cons x xs)

100 show ?case

101 proof (induct x)

102 case Const

103 from Cons show ?case by simp

104 next

105 case Load

106 from Cons show ?case by simp

107 next

108 case Apply

109 from Cons show ?case by simp

110 qed

111 qed

113 theorem correctness: "execute (compile e) env = eval e env"

114 proof -

115 have "\<And>stack. exec (compile e) stack env = eval e env # stack"

116 proof (induct e)

117 case Variable show ?case by simp

118 next

119 case Constant show ?case by simp

120 next

121 case Binop then show ?case by (simp add: exec_append)

122 qed

123 then show ?thesis by (simp add: execute_def)

124 qed

127 text {* \bigskip In the proofs above, the @{text simp} method does

128 quite a lot of work behind the scenes (mostly ``functional program

129 execution''). Subsequently, the same reasoning is elaborated in

130 detail --- at most one recursive function definition is used at a

131 time. Thus we get a better idea of what is actually going on. *}

133 lemma exec_append':

134 "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"

135 proof (induct xs arbitrary: stack)

136 case (Nil s)

137 have "exec ([] @ ys) s env = exec ys s env" by simp

138 also have "... = exec ys (exec [] s env) env" by simp

139 finally show ?case .

140 next

141 case (Cons x xs s)

142 show ?case

143 proof (induct x)

144 case (Const val)

145 have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"

146 by simp

147 also have "... = exec (xs @ ys) (val # s) env" by simp

148 also from Cons have "... = exec ys (exec xs (val # s) env) env" .

149 also have "... = exec ys (exec (Const val # xs) s env) env" by simp

150 finally show ?case .

151 next

152 case (Load adr)

153 from Cons show ?case by simp -- {* same as above *}

154 next

155 case (Apply fn)

156 have "exec ((Apply fn # xs) @ ys) s env =

157 exec (Apply fn # xs @ ys) s env" by simp

158 also have "... =

159 exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp

160 also from Cons have "... =

161 exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .

162 also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp

163 finally show ?case .

164 qed

165 qed

167 theorem correctness': "execute (compile e) env = eval e env"

168 proof -

169 have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"

170 proof (induct e)

171 case (Variable adr s)

172 have "exec (compile (Variable adr)) s env = exec [Load adr] s env"

173 by simp

174 also have "... = env adr # s" by simp

175 also have "env adr = eval (Variable adr) env" by simp

176 finally show ?case .

177 next

178 case (Constant val s)

179 show ?case by simp -- {* same as above *}

180 next

181 case (Binop fn e1 e2 s)

182 have "exec (compile (Binop fn e1 e2)) s env =

183 exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp

184 also have "... = exec [Apply fn]

185 (exec (compile e1) (exec (compile e2) s env) env) env"

186 by (simp only: exec_append)

187 also have "exec (compile e2) s env = eval e2 env # s" by fact

188 also have "exec (compile e1) ... env = eval e1 env # ..." by fact

189 also have "exec [Apply fn] ... env =

190 fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp

191 also have "... = fn (eval e1 env) (eval e2 env) # s" by simp

192 also have "fn (eval e1 env) (eval e2 env) =

193 eval (Binop fn e1 e2) env"

194 by simp

195 finally show ?case .

196 qed

198 have "execute (compile e) env = hd (exec (compile e) [] env)"

199 by (simp add: execute_def)

200 also from exec_compile have "exec (compile e) [] env = [eval e env]" .

201 also have "hd ... = eval e env" by simp

202 finally show ?thesis .

203 qed

205 end