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