142 |
142 |
143 A few exercises are scattered around the text. Their solutions are given |
143 A few exercises are scattered around the text. Their solutions are given |
144 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
144 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
145 to solve the exercises on your own, and then look at the solutions. |
145 to solve the exercises on your own, and then look at the solutions. |
146 *} |
146 *} |
|
147 |
|
148 section {* How To Understand Code in Isabelle *} |
|
149 |
|
150 text {* |
|
151 One of the more difficult aspects of programming is to understand somebody |
|
152 else's code. This is aggravated in Isabelle by the fact that many parts of |
|
153 the code contain only few comments. There is one strategy that might be |
|
154 helpful to navigate your way: ML is an interactive programming environment, |
|
155 which means you can evaluate code on the fly (for example inside an |
|
156 \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy |
|
157 self-contained chunks of existing code into a separate theory file and then |
|
158 study it alongside with examples. You can also install probes inside the |
|
159 copied code without having to recompile the whole Isabelle distributions. Such |
|
160 probes might be messages or printouts of variables (see chapter |
|
161 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
|
162 probing the code with explicit print statements is the most efficient method |
|
163 for understanding what some code is doing. However do not expect quick |
|
164 results with this! Depending on the size of the code you are looking at, |
|
165 you will spend the better part of a quiet afternoon with it. But there |
|
166 seems to be no better way around it. |
|
167 *} |
|
168 |
147 |
169 |
148 section {* Aaaaargh! My Code Does not Work Anymore *} |
170 section {* Aaaaargh! My Code Does not Work Anymore *} |
149 |
171 |
150 text {* |
172 text {* |
151 One unpleasant aspect of any code development inside a larger system is that |
173 One unpleasant aspect of any code development inside a larger system is that |
246 \end{itemize} |
268 \end{itemize} |
247 |
269 |
248 Please let me know of any omissions. Responsibility for any remaining |
270 Please let me know of any omissions. Responsibility for any remaining |
249 errors lies with me.\bigskip |
271 errors lies with me.\bigskip |
250 |
272 |
251 \vspace{5cm} |
273 \newpage |
|
274 \mbox{}\\[5cm] |
|
275 |
|
276 |
252 {\Large\bf |
277 {\Large\bf |
253 This tutorial is still in the process of being written! All of the |
278 This tutorial is still in the process of being written! All of the |
254 text is still under construction. Sections and |
279 text is still under construction. Sections and |
255 chapters that are under \underline{heavy} construction are marked |
280 chapters that are under \underline{heavy} construction are marked |
256 with TBD.} |
281 with TBD.} |