39307
|
1 |
(* Title: HOL/Imperative_HOL/Overview.thy
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
(*<*)
|
|
6 |
theory Overview
|
|
7 |
imports Imperative_HOL LaTeXsugar
|
|
8 |
begin
|
|
9 |
|
|
10 |
(* type constraints with spacing *)
|
|
11 |
setup {*
|
|
12 |
let
|
|
13 |
val typ = Simple_Syntax.read_typ;
|
|
14 |
val typeT = Syntax.typeT;
|
|
15 |
val spropT = Syntax.spropT;
|
|
16 |
in
|
|
17 |
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
|
|
18 |
("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
|
|
19 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
|
|
20 |
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
|
|
21 |
("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
|
|
22 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
|
|
23 |
end
|
|
24 |
*}(*>*)
|
|
25 |
|
|
26 |
text {*
|
|
27 |
@{text "Imperative HOL"} is a leightweight framework for reasoning
|
|
28 |
about imperative data structures in @{text "Isabelle/HOL"}
|
|
29 |
\cite{Nipkow-et-al:2002:tutorial}. Its basic ideas are described in
|
|
30 |
\cite{Bulwahn-et-al:2008:imp_HOL}. However their concrete
|
|
31 |
realisation has changed since, due to both extensions and
|
|
32 |
refinements. Therefore this overview wants to present the framework
|
|
33 |
\qt{as it is} by now. It focusses on the user-view, less on matters
|
|
34 |
of constructions. For details study of the theory sources is
|
|
35 |
encouraged.
|
|
36 |
*}
|
|
37 |
|
|
38 |
|
|
39 |
section {* A polymorphic heap inside a monad *}
|
|
40 |
|
|
41 |
text {*
|
|
42 |
Heaps (@{type heap}) can be populated by values of class @{class
|
|
43 |
heap}; HOL's default types are already instantiated to class @{class
|
|
44 |
heap}.
|
|
45 |
|
|
46 |
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
|
|
47 |
following specification:
|
|
48 |
|
|
49 |
\begin{quote}
|
|
50 |
@{datatype Heap}
|
|
51 |
\end{quote}
|
|
52 |
|
|
53 |
Unwrapping of this monad type happens through
|
|
54 |
|
|
55 |
\begin{quote}
|
|
56 |
@{term_type execute} \\
|
|
57 |
@{thm execute.simps [no_vars]}
|
|
58 |
\end{quote}
|
|
59 |
|
|
60 |
This allows for equational reasoning about monadic expressions; the
|
|
61 |
fact collection @{text execute_simps} contains appropriate rewrites
|
|
62 |
for all fundamental operations.
|
|
63 |
|
39610
|
64 |
Primitive fine-granular control over heaps is available through rule
|
39307
|
65 |
@{text Heap_cases}:
|
|
66 |
|
|
67 |
\begin{quote}
|
|
68 |
@{thm [break] Heap_cases [no_vars]}
|
|
69 |
\end{quote}
|
|
70 |
|
|
71 |
Monadic expression involve the usual combinators:
|
|
72 |
|
|
73 |
\begin{quote}
|
|
74 |
@{term_type return} \\
|
|
75 |
@{term_type bind} \\
|
|
76 |
@{term_type raise}
|
|
77 |
\end{quote}
|
|
78 |
|
|
79 |
This is also associated with nice monad do-syntax. The @{typ
|
|
80 |
string} argument to @{const raise} is just a codified comment.
|
|
81 |
|
|
82 |
Among a couple of generic combinators the following is helpful for
|
|
83 |
establishing invariants:
|
|
84 |
|
|
85 |
\begin{quote}
|
|
86 |
@{term_type assert} \\
|
|
87 |
@{thm assert_def [no_vars]}
|
|
88 |
\end{quote}
|
|
89 |
*}
|
|
90 |
|
|
91 |
|
|
92 |
section {* Relational reasoning about @{type Heap} expressions *}
|
|
93 |
|
|
94 |
text {*
|
|
95 |
To establish correctness of imperative programs, predicate
|
|
96 |
|
|
97 |
\begin{quote}
|
|
98 |
@{term_type crel}
|
|
99 |
\end{quote}
|
|
100 |
|
|
101 |
provides a simple relational calculus. Primitive rules are @{text
|
|
102 |
crelI} and @{text crelE}, rules appropriate for reasoning about
|
|
103 |
imperative operation are available in the @{text crel_intros} and
|
|
104 |
@{text crel_elims} fact collections.
|
|
105 |
|
|
106 |
Often non-failure of imperative computations does not depend
|
|
107 |
on the heap at all; reasoning then can be easier using predicate
|
|
108 |
|
|
109 |
\begin{quote}
|
|
110 |
@{term_type success}
|
|
111 |
\end{quote}
|
|
112 |
|
|
113 |
Introduction rules for @{const success} are available in the
|
|
114 |
@{text success_intro} fact collection.
|
|
115 |
|
|
116 |
@{const execute}, @{const crel}, @{const success} and @{const bind}
|
|
117 |
are related by rules @{text execute_bind_success}, @{text
|
|
118 |
success_bind_executeI}, @{text success_bind_crelI}, @{text
|
|
119 |
crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
|
|
120 |
*}
|
|
121 |
|
|
122 |
|
|
123 |
section {* Monadic data structures *}
|
|
124 |
|
|
125 |
text {*
|
|
126 |
The operations for monadic data structures (arrays and references)
|
|
127 |
come in two flavours:
|
|
128 |
|
|
129 |
\begin{itemize}
|
|
130 |
|
|
131 |
\item Operations on the bare heap; their number is kept minimal
|
|
132 |
to facilitate proving.
|
|
133 |
|
|
134 |
\item Operations on the heap wrapped up in a monad; these are designed
|
|
135 |
for executing.
|
|
136 |
|
|
137 |
\end{itemize}
|
|
138 |
|
|
139 |
Provided proof rules are such that they reduce monad operations to
|
|
140 |
operations on bare heaps.
|
39717
|
141 |
|
|
142 |
Note that HOL equality coincides with reference equality and may be
|
|
143 |
used as primitive executable operation.
|
39307
|
144 |
*}
|
|
145 |
|
|
146 |
subsection {* Arrays *}
|
|
147 |
|
|
148 |
text {*
|
|
149 |
Heap operations:
|
|
150 |
|
|
151 |
\begin{quote}
|
|
152 |
@{term_type Array.alloc} \\
|
|
153 |
@{term_type Array.present} \\
|
|
154 |
@{term_type Array.get} \\
|
|
155 |
@{term_type Array.set} \\
|
|
156 |
@{term_type Array.length} \\
|
|
157 |
@{term_type Array.update} \\
|
|
158 |
@{term_type Array.noteq}
|
|
159 |
\end{quote}
|
|
160 |
|
|
161 |
Monad operations:
|
|
162 |
|
|
163 |
\begin{quote}
|
|
164 |
@{term_type Array.new} \\
|
|
165 |
@{term_type Array.of_list} \\
|
|
166 |
@{term_type Array.make} \\
|
|
167 |
@{term_type Array.len} \\
|
|
168 |
@{term_type Array.nth} \\
|
|
169 |
@{term_type Array.upd} \\
|
|
170 |
@{term_type Array.map_entry} \\
|
|
171 |
@{term_type Array.swap} \\
|
|
172 |
@{term_type Array.freeze}
|
|
173 |
\end{quote}
|
|
174 |
*}
|
|
175 |
|
|
176 |
subsection {* References *}
|
|
177 |
|
|
178 |
text {*
|
|
179 |
Heap operations:
|
|
180 |
|
|
181 |
\begin{quote}
|
|
182 |
@{term_type Ref.alloc} \\
|
|
183 |
@{term_type Ref.present} \\
|
|
184 |
@{term_type Ref.get} \\
|
|
185 |
@{term_type Ref.set} \\
|
|
186 |
@{term_type Ref.noteq}
|
|
187 |
\end{quote}
|
|
188 |
|
|
189 |
Monad operations:
|
|
190 |
|
|
191 |
\begin{quote}
|
|
192 |
@{term_type Ref.ref} \\
|
|
193 |
@{term_type Ref.lookup} \\
|
|
194 |
@{term_type Ref.update} \\
|
|
195 |
@{term_type Ref.change}
|
|
196 |
\end{quote}
|
|
197 |
*}
|
|
198 |
|
|
199 |
|
|
200 |
section {* Code generation *}
|
|
201 |
|
|
202 |
text {*
|
|
203 |
Imperative HOL sets up the code generator in a way that imperative
|
|
204 |
operations are mapped to suitable counterparts in the target
|
|
205 |
language. For @{text Haskell}, a suitable @{text ST} monad is used;
|
|
206 |
for @{text SML}, @{text Ocaml} and @{text Scala} unit values ensure
|
|
207 |
that the evaluation order is the same as you would expect from the
|
|
208 |
original monadic expressions. These units may look cumbersome; the
|
|
209 |
target language variants @{text SML_imp}, @{text Ocaml_imp} and
|
|
210 |
@{text Scala_imp} make some effort to optimize some of them away.
|
|
211 |
*}
|
|
212 |
|
|
213 |
|
|
214 |
section {* Some hints for using the framework *}
|
|
215 |
|
|
216 |
text {*
|
|
217 |
Of course a framework itself does not by itself indicate how to make
|
|
218 |
best use of it. Here some hints drawn from prior experiences with
|
|
219 |
Imperative HOL:
|
|
220 |
|
|
221 |
\begin{itemize}
|
|
222 |
|
|
223 |
\item Proofs on bare heaps should be strictly separated from those
|
|
224 |
for monadic expressions. The first capture the essence, while the
|
|
225 |
latter just describe a certain wrapping-up.
|
|
226 |
|
|
227 |
\item A good methodology is to gradually improve an imperative
|
|
228 |
program from a functional one. In the extreme case this means
|
|
229 |
that an original functional program is decomposed into suitable
|
|
230 |
operations with exactly one corresponding imperative operation.
|
|
231 |
Having shown suitable correspondence lemmas between those, the
|
|
232 |
correctness prove of the whole imperative program simply
|
|
233 |
consists of composing those.
|
|
234 |
|
|
235 |
\item Whether one should prefer equational reasoning (fact
|
|
236 |
collection @{text execute_simps} or relational reasoning (fact
|
39610
|
237 |
collections @{text crel_intros} and @{text crel_elims}) depends
|
|
238 |
on the problems to solve. For complex expressions or
|
|
239 |
expressions involving binders, the relation style usually is
|
|
240 |
superior but requires more proof text.
|
39307
|
241 |
|
|
242 |
\item Note that you can extend the fact collections of Imperative
|
39610
|
243 |
HOL yourself whenever appropriate.
|
39307
|
244 |
|
|
245 |
\end{itemize}
|
|
246 |
*}
|
|
247 |
|
|
248 |
end |