adding to "how to understand code"
authorNorbert Schirmer <norbert.schirmer@web.de>
Fri, 17 May 2019 07:29:51 +0200
changeset 568 be23597e81db
parent 567 f7c97e64cc2a
child 569 f875a25aa72d
adding to "how to understand code"
ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Thu May 16 19:56:12 2019 +0200
+++ b/ProgTutorial/Intro.thy	Fri May 17 07:29:51 2019 +0200
@@ -208,12 +208,25 @@
   alongside with examples. You can also install ``probes'' inside the copied
   code without having to recompile the whole Isabelle distribution. Such
   probes might be messages or printouts of variables (see chapter
-  \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
-  probing the code with explicit print statements is the most effective method
+  \ref{chp:firststeps}). Moreover, PolyML contains a debugger that is also supported from Isabelle/jEdit
+  with breakpoints and stack inspection.
+  Still it seems that
+  probing the code with explicit print statements is an effective method
   for understanding what some piece of code is doing. However do not expect
   quick results with this! It is painful. Depending on the size of the code
   you are looking at, you will spend the better part of a quiet afternoon with
   it. And there seems to be no better way for understanding code in Isabelle.
+  Summarizing: 
+  \begin{itemize}
+     \item Get familiar with the concepts and the applications by studying the Isabelle/Isar 
+     reference manual and the rich set of theories and libraries in the standard distribution and the AFP.
+     \item Get familiar with the implementation and the best practices (like coding style, 
+     canonical argument ordering, \<open>\<dots>\<close>) by reading the Isabelle/Isar implementation manual and by 
+     browsing, reading and digesting both the code implementing a function as well and the 
+     applications of that function.
+     \item Interactively experiment with the code.
+  \end{itemize}
+  
 \<close>