1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 18:27:17 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 21:45:07 2012 +0200
1.3 @@ -695,7 +695,7 @@
1.4 starts with a formal {\em specification} of the problem to be solved.
1.5 \begin{figure}
1.6 \begin{center}
1.7 - %\includegraphics[width=110mm]{fig/math-universe-small}
1.8 + \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.9 \caption{The three-dimensional universe of mathematics knowledge}
1.10 \label{fig:mathuni}
1.11 \end{center}
1.12 @@ -973,16 +973,18 @@
1.13 \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.14 \>precond \>: filterExpression continius on $\mathbb{R}$ \\
1.15 \>output \>: stepResponse $x[n]$ \\
1.16 - \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
1.17 + \>postcond \>: TODO\\ \end{tabbing}}
1.18
1.19 -\begin{remark}
1.20 - Defining the postcondition requires a high amount mathematical
1.21 - knowledge, the difficult part in our case is not to set up this condition
1.22 - nor it is more to define it in a way the interpreter is able to handle it.
1.23 - Due the fact that implementing that mechanisms is quite the same amount as
1.24 - creating the programm itself, it is not avaible in our prototype.
1.25 - \label{rm:postcond}
1.26 -\end{remark}
1.27 +%JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1.28 +
1.29 +% \begin{remark}
1.30 +% Defining the postcondition requires a high amount mathematical
1.31 +% knowledge, the difficult part in our case is not to set up this condition
1.32 +% nor it is more to define it in a way the interpreter is able to handle it.
1.33 +% Due the fact that implementing that mechanisms is quite the same amount as
1.34 +% creating the programm itself, it is not avaible in our prototype.
1.35 +% \label{rm:postcond}
1.36 +% \end{remark}
1.37
1.38 \paragraph{The implementation} of the formal specification in the present
1.39 prototype, still bar-bones without support for authoring:
1.40 @@ -1094,12 +1096,13 @@
1.41
1.42 \subsection{Implementation of the Method}\label{meth}
1.43
1.44 -\paragraph{After specifieing the problem} we start to implement the method(s) of
1.45 -the problem. The methods represent the different ways a problem can be solved,
1.46 -this can include different mathematical tactics as well as different tactics
1.47 -taught in different courses.
1.48 +The methods represent the different ways a problem can be solved. This can
1.49 +include mathematical tactics as well as tactics taught in different courses.
1.50 +Declaring the Method itself gives us the possibilities to describe the way of
1.51 +calculation in deep, as well we get the oppertunities to build in different
1.52 +rulesets.
1.53
1.54 -
1.55 +{\small
1.56 \begin{verbatim}
1.57 01 store_met
1.58 02 (prep_met thy "SP_InverseZTransformation_classic" [] e_metID
1.59 @@ -1107,39 +1110,45 @@
1.60 04 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.61 05 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.62 06 {rew_ord'="tless_true",
1.63 -07 rls'= e_rls,
1.64 +07 rls = rls,
1.65 08 calc = [],
1.66 09 srls = e_rls,
1.67 10 prls = e_rls,
1.68 11 crls = e_rls,
1.69 12 errpats = [],
1.70 13 nrls = e_rls},
1.71 -14 "empty_programm"
1.72 +14 "empty_program"
1.73 15 ));
1.74 \end{verbatim}
1.75 +}
1.76
1.77 -The above code is again very technical and goes hard in detail. But to document
1.78 -and present the neccessary steps follow up the description of the above code:
1.79 +The above code is again very technical and goes hard in detail. Unfortunataly
1.80 +most declerations are not essential for a basic programm but leads us to a huge
1.81 +range of powerful possibilities.
1.82
1.83 \begin{description}
1.84 -
1.85 -\item[01-02] this to lines store the method with the given name into the system
1.86 -\item[03] here, the path is specifiet; which capitel this method is belonging to
1.87 -\item[04-05] as the requirements for different methods can be different we
1.88 -specify again the \emph{given} and the \emph{find} element.
1.89 -\item[06]
1.90 -\item[07]
1.91 -\item[08]
1.92 -\item[09]
1.93 -\item[10]
1.94 -\item[11]
1.95 -\item[12]
1.96 -\item[13]
1.97 +\item[01..02] stores the method with the given name into the system under a global
1.98 +reference.
1.99 +\item[03] specifies the topic under which the method can be used.
1.100 +\item[04..05] as the requirements for different methods can deviant we
1.101 +declare what is \emph{given} and and what to \emph{find} for this specific method.
1.102 +\item[06] \emph{rewrite order} is the order of this rls, which one theorem of is
1.103 +used for rewriting one single step.
1.104 +\item[07] \texttt{rls} is the currently used ruleset for this method,
1.105 +\texttt{e\_rls} specifies a
1.106 +ruleset where conditions can be used within it.
1.107 +\item[08] we can add this method to a predefined tree of calculations ore leave
1.108 +it independend.
1.109 +\item[09] \texttt{srls}, can be used to evaluate list expressions in the source
1.110 +\item[10] \texttt{prls} indicates predicates which can be used in model patterns.
1.111 +\item[11] \texttt{crls}, gives us the possibility for checking formulas
1.112 +lementwise
1.113 +\item[12] \emph{error patterns} which are expected in this kind of method can be
1.114 +specified.
1.115 +\item[13] \texttt{crls}, declares the canonical simplifier for the specific method
1.116 \item[14] for this time we don't specify the programm itself and keep it empty.
1.117 Follow up \S\ref{progr} for informations on how to implement this \textit{main}
1.118 part.
1.119 -
1.120 -
1.121 \end{description}
1.122
1.123 \subsection{Implementation of the TP-based Program}\label{progr}