1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 14:56:34 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 16:29:03 2012 +0200
     1.3 @@ -735,7 +735,7 @@
     1.4  \paragraph{The implementation} of the formal specification in the present
     1.5  prototype, still bar-bones without support for authoring:
     1.6  %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
     1.7 -{\footnotesize
     1.8 +{\footnotesize\label{exp-spec}
     1.9  \begin{verbatim}
    1.10     01  store_specification
    1.11     02    (prepare_specification
    1.12 @@ -845,10 +845,22 @@
    1.13  TODO
    1.14  \subsection{Preparation of Simplifiers for the Program}\label{simp}
    1.15  
    1.16 -\paragraph{After collecting} informations about the problem and reviewing the
    1.17 -calculations, the programm may be seem hard and heavy, therefor we can set up
    1.18 +\paragraph{After collecting} informations about the problem 
    1.19 +%WN4 welche 'informations' ?
    1.20 +%WN4 Wenn das welche sind, die oben NICHT vorgekommen sind, dann anf"uhren
    1.21 +%WN4 Wenn das welche sind, die oben SCHON vorgekommen sind, dann weglassen
    1.22 +%WN4                       und Platz sparen.
    1.23 +%WN4 
    1.24 +%WN4 Wenn wir diese Bemerkung hier weglassen (sie m"usste eigentlich an jedem
    1.25 +%WN4 Beginn von 3.* stehen), dann kommt sie gleich an den Anfang
    1.26 +%WN4 nach der "Uberschrift von 3.
    1.27 +and reviewing the calculations, 
    1.28 +%WN4 welche 'calculations', ist von solchen bisher schon die Rede gewesen ?
    1.29 +the programm may be seem hard and heavy, therefor we can set up
    1.30  some simplifications, for e.g. is the simplification of reational expressions
    1.31 -already provided in the {\sisac{}} system. Also obligate is the use of the 
    1.32 +already provided in the {\sisac{}} system. 
    1.33 +%WN4 
    1.34 +Also obligate is the use of the 
    1.35  function \texttt{drop\_questionmarks} which excludes irrelevant symbols out of
    1.36  the expression. (Irrelevant symbols may be result out of the system during the
    1.37  calculation.)
    1.38 @@ -967,17 +979,16 @@
    1.39  \end{description}
    1.40  
    1.41  \subsection{Implementation of the TP-based Program}\label{progr} 
    1.42 -So finally all the prerequisites are described and the program can be
    1.43 -presented which computes a solution for the problem of the running
    1.44 -example from p.\pageref{fig-interactive}. The reader remembering the
    1.45 -introduction of the programming language in \S\ref{PL-isab} might
    1.46 -immediately comprehend the program:
    1.47 +So finally all the prerequisites are described and the very topic can
    1.48 +be addressed. The program below comes back to the running example: it
    1.49 +computes a solution for the problem from Fig.\ref{fig-interactive} on
    1.50 +p.\pageref{fig-interactive}. The reader is reminded of
    1.51 +\S\ref{PL-isab}, the introduction of the programming language:
    1.52  {\small\it
    1.53  \begin{tabbing}\label{s:impl}
    1.54  123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
    1.55 -\> \\
    1.56 -\> \\
    1.57 -\>{\rm 01}\>  {\tt Program} InverseZTransform (X\_eq::bool) =   \\
    1.58 +\>{\rm 00}\>val program =\\
    1.59 +\>{\rm 01}\>  "{\tt Program} InverseZTransform (X\_eq::bool) =   \\
    1.60  \>{\rm 02}\>\>  {\tt LET}                                       \\
    1.61  \>{\rm 03}\>\>\>  X\_eq = {\tt Take} X\_eq ;   \\
    1.62  \>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
    1.63 @@ -988,11 +999,10 @@
    1.64  %\>{\rm 10}\>\>\>\>\>\>\>\>\>  [simplification, of\_rationals, to\_partial\_fraction] ) \\
    1.65  \>{\rm 09}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\
    1.66  \>{\rm 10}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
    1.67 -
    1.68  \>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@   \\
    1.69  \>{\rm 12}\>\>\>\>\>  $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
    1.70  \>{\rm 13}\>\>  {\tt IN } \\
    1.71 -\>{\rm 14}\>\>\>  X'\_eq\\
    1.72 +\>{\rm 14}\>\>\>  X'\_eq"
    1.73  \end{tabbing}}
    1.74  % ORIGINAL FROM Inverse_Z_Transform.thy
    1.75  % "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
    1.76 @@ -1014,35 +1024,58 @@
    1.77  % "  n_eq = (Rewrite_Set inverse_z False) X_zeq;      "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
    1.78  % "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
    1.79  % "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
    1.80 -As mentioned in \S\ref{PL} the program is purely functional and lacks
    1.81 -any input statements and output statements. So the steps of
    1.82 -calculation towards a solution (and interactive tutoring in step-wise
    1.83 -problem solving) are created as a side-effect by Lucas-Interpretation.
    1.84 -The break-points for the interpreter are the tactics \textit{Take},
    1.85 -\textit{Rewrite}, \textit{SubProblem} and \textit{Rewrite\_Set} in the
    1.86 -above lines {\rm 03, 04, 07, 10, 11} and {\rm 12} respectively. These
    1.87 -tactics produce the lines in the calculation on p.\pageref{flow-impl}.
    1.88 +The program is represented as a string and part of the method in
    1.89 +\S\ref{meth}.  As mentioned in \S\ref{PL} the program is purely
    1.90 +functional and lacks any input statements and output statements. So
    1.91 +the steps of calculation towards a solution (and interactive tutoring
    1.92 +in step-wise problem solving) are created as a side-effect by
    1.93 +Lucas-Interpretation.  The side-effects are triggered by the tactics
    1.94 +\textit{Take}, \textit{Rewrite}, \textit{SubProblem} and
    1.95 +\textit{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
    1.96 +{\rm 12} respectively. These tactics produce the lines in the
    1.97 +calculation on p.\pageref{flow-impl}.
    1.98  
    1.99 -The above program also indicates the dominant role of interactive
   1.100 +The above lines {\rm 05, 06} do not contain a tactics, so they do not
   1.101 +immediately contribute to the calculation on p.\pageref{flow-impl};
   1.102 +rather, they compute actual arguments for the \textit{SubProblem} in
   1.103 +line {\rm 09}~\footnote{The tactics also are break-points for the
   1.104 +interpreter, where control is handed over to the user in interactive
   1.105 +tutoring.}.
   1.106 +
   1.107 +\medskip The above program also indicates the dominant role of interactive
   1.108  selection of knowledge in the three-dimensional universe of
   1.109  mathematics as depicted in Fig.\ref{fig:mathuni} on
   1.110  p.\pageref{fig:mathuni}, The \textit{SubProblem} in the above lines
   1.111  {\rm 07..09} is more than a function call with the actual arguments
   1.112  \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
   1.113  three items:
   1.114 +
   1.115  \begin{enumerate}
   1.116  \item the theory, in the example \textit{Isac} because different
   1.117  methods can be selected in Pt.3 below, which are defined in different
   1.118  theories with \textit{Isac} collecting them.
   1.119 -\item the specification identified by \textit{[partial\_fraction, rational, simplification]} in the tree of specifications; this specification is analogous to the specification of the main program described in \S\ref{spec}.
   1.120 -\item the method in the above example is \textit{[ ]}, i.e. empty, which allows
   1.121 -the interpreter to select one of the methods predefined in the specification
   1.122 +\item the specification identified by \textit{[partial\_fraction,
   1.123 +rational, simplification]} in the tree of specifications; this
   1.124 +specification is analogous to the specification of the main program
   1.125 +described in \S\ref{spec}; the problem is to find a ``partial fraction
   1.126 +decomposition'' for a univariate rational polynomial.
   1.127 +\item the method in the above example is \textit{[ ]}, i.e. empty,
   1.128 +which supposes the interpreter to select one of the methods predefined
   1.129 +in the specification, for instance in line {\rm 13} in the running
   1.130 +example's specification on p.\pageref{exp-spec}~\footnote{The freedom
   1.131 +(or obligation) for selection carries over to the student in
   1.132 +interactive tutoring.}.
   1.133  \end{enumerate}
   1.134  
   1.135 -.\\.\\.\\
   1.136 -
   1.137 +The program code, above presented as a string, is parsed by Isabelle's
   1.138 +parser --- the program is an Isabelle term. This fact is expected to
   1.139 +simplify verification tasks in the future; on the other hand, this
   1.140 +fact causes troubles in error detectetion which are discussed as part
   1.141 +of the workflow in the subsequent section.
   1.142  
   1.143  \section{Workflow of Programming in the Prototype}\label{workflow}
   1.144 +The previous section presented all the duties and tasks to be accomplished by
   1.145 +programmers of TP-based languages. The tasks are interrelated
   1.146  
   1.147  \subsection{Preparations and Trials}\label{flow-prep}
   1.148  TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''