1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 10:57:54 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 12:48:30 2012 +0200
1.3 @@ -666,7 +666,8 @@
1.4
1.5 \paragraph{At the state-of-the-art in mechanization of knowledge} in
1.6 engineering sciences, the process does not stop with the mechanization of
1.7 -mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
1.8 +mathematics traditionally used in these sciences. Rather, ``Formal Methods''.
1.9 +%% \cite{TODO-formal-methods}
1.10 are expected to proceed to formal and explicit description of physical items. Signal Processing,
1.11 for instance is concerned with physical devices for signal acquisition
1.12 and reconstruction, which involve measuring a physical signal, storing
1.13 @@ -674,7 +675,9 @@
1.14 approximation thereof. For digital systems, this typically includes
1.15 sampling and quantization; devices for signal compression, including
1.16 audio compression, image compression, and video compression, etc.
1.17 -``Domain engineering''\cite{db-domain-engineering} is concerned with
1.18 +``Domain engineering''
1.19 +%% \cite{db-domain-engineering}
1.20 +is concerned with
1.21 {\em specification} of these devices' components and features; this
1.22 part in the process of mechanization is only at the beginning in domains
1.23 like Signal Processing.
1.24 @@ -695,11 +698,11 @@
1.25 notation, could look like is this:
1.26
1.27 %WN Hier brauchen wir die Spezifikation des 'running example' ...
1.28 -
1.29 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.30 %JR der post condition - die existiert für uns ja eigentlich nicht aka
1.31 %JR haben sie bis jetzt nicht beachtet WN...
1.32 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.33 +%JR2 done
1.34
1.35 \label{eg:neuper2}
1.36 {\small\begin{tabbing}
1.37 @@ -711,12 +714,14 @@
1.38 \>output \>: stepResponse $x[n]$ \\
1.39 \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
1.40
1.41 - \paragraph{Remark on post-conditions:} Defining the postcondition requires a
1.42 - high amount mathematical knowledge, the difficult part in our case is not to
1.43 - set up this condition nor it is more to define it in a way the interpreter is
1.44 - able to handle it. Due the fact that implementing that mechanisms is quite
1.45 - the same amount as creating the programm itself, it is not avaible in our
1.46 - prototype.\label{rm:postcond}
1.47 +\begin{remark}
1.48 + Defining the postcondition requires a high amount mathematical
1.49 + knowledge, the difficult part in our case is not to set up this condition
1.50 + nor it is more to define it in a way the interpreter is able to handle it.
1.51 + Due the fact that implementing that mechanisms is quite the same amount as
1.52 + creating the programm itself, it is not avaible in our prototype.
1.53 + \label{rm:postcond}
1.54 +\end{remark}
1.55
1.56 \paragraph{The implementation} of the formal specification in the present
1.57 prototype, still bar-bones without support for authoring:
1.58 @@ -761,7 +766,7 @@
1.59 component).
1.60 \item[07..10] are the specification with input, pre-condition, output
1.61 and post-condition respectively; the post-condition is not handled in
1.62 -the prototype presently. (Follow up Remark in Section~\ref{rm:postcond})
1.63 +the prototype presently. (Follow up Remark~\ref{rm:postcond})
1.64 \item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.65 {\sisac}) which evaluates the pre-condition for the actual input data.
1.66 Only if the evaluation yields \textit{True}, a program con be started.
1.67 @@ -845,28 +850,33 @@
1.68 of the Inverse Z Transformation and the corresponding partial fraction it was
1.69 neccessary to build helping functions like \texttt{get\_denominator},
1.70 \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
1.71 -to filter the deonimonator or numerator out of a fraction, last one helps us to
1.72 +to filter the denominator or numerator out of a fraction, last one helps us to
1.73 get to know the bound variable in a equation.
1.74 \par
1.75 -By taking \texttt{get\_denominator} we want to explain how to implement new
1.76 -functions into the existing system and how we can later use them in our program.
1.77 +By taking \texttt{get\_denominator} as an example, we want to explain how to
1.78 +implement new functions into the existing system and how we can later use them
1.79 +in our program.
1.80
1.81 \subsubsection{Find a place to Store the Function}
1.82 +
1.83 The whole system builds up on a well defined structure of Knowledge. This
1.84 -Knowledge sets up at the Path: \ttfamily src/Tools/isac/Knowledge\normalfont.
1.85 +Knowledge sets up at the Path:
1.86 +\begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
1.87 For implementing the Function \texttt{get\_denominator} (which let us extract
1.88 the denominator out of a fraction) we have choosen the Theory (file)
1.89 \texttt{Rational.thy}.
1.90
1.91 \subsubsection{Write down the new Function}
1.92 +
1.93 In upper Theory we now define the new function and its purpose:
1.94 \begin{verbatim}
1.95 get_denominator :: "real => real"
1.96 \end{verbatim}
1.97 This command tells the machine that a function with the name
1.98 \texttt{get\_denominator} exists which gets a real expression as argument and
1.99 -returns once again a real expression. Now we are able to implement the function itself, Example~\ref{eg:getdenom}
1.100 -shows the implementation of \texttt{get\_denominator}.
1.101 +returns once again a real expression. Now we are able to implement the function
1.102 +itself, Example~\ref{eg:getdenom} now shows the implementation of
1.103 +\texttt{get\_denominator}.
1.104
1.105 \begin{example}
1.106 \label{eg:getdenom}
1.107 @@ -890,21 +900,57 @@
1.108 Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1.109 there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1.110 splittet
1.111 -into its two parts (\texttt{ \$num \$denom}). The lines before are additionals
1.112 +into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1.113 commands for declaring the function and the lines after are modeling and
1.114 returning a real variable out of \texttt{\$denom}.
1.115
1.116 \subsubsection{Add a test for the new Function}
1.117 -\subsubsection{Use the new Function}
1.118
1.119 +\paragraph{Everytime when adding} a new function it is essential also to add
1.120 +a test for it. Tests for all functions are sorted in the same structure as the
1.121 +knowledge it self and can be found up from the path:
1.122 +\begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1.123 +This tests are nothing very special, as a first prototype the functionallity
1.124 +of a function can be checked by evaluating the result of a simple expression
1.125 +passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1.126 +\textit{just} created function \texttt{get\_denominator}.
1.127
1.128 +\begin{example}
1.129 +\label{eg:getdenomtest}
1.130 +\begin{verbatim}
1.131 +
1.132 +01 val thy = @{theory Isac};
1.133 +02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1.134 +03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1.135 +04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1.136 +05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1.137 +\end{example}
1.138 +
1.139 +\begin{description}
1.140 +\item[01] checks if the proofer set up on our {\sisac{}} System.
1.141 +\item[02] passes a simple expression (fraction) to our suddenly created
1.142 + function.
1.143 +\item[04] checks if the resulting variable is the correct one (in this case
1.144 + ``b'' the denominator) and returns.
1.145 +\item[05] handels the error case and reports that the function is not able to
1.146 + solve the given problem.
1.147 +\end{description}
1.148
1.149 \subsection{Implementation of the TP-based Program}\label{progr}
1.150 -%WN <--> \chapter 8 der Thesis
1.151 -.\\.\\.\\
1.152
1.153 -{\small\it\begin{tabbing}
1.154 +\paragraph{After introducing} neccesarry informations about the {\sisac{}}
1.155 +System, the main part of a implementation in the TP-bases language can be shown.
1.156 +\par
1.157 +Solution~\ref{s:impl} shows us the implementation of the
1.158 +Inverse-Z-Transformation, a description on the code is given afterwards.
1.159 +
1.160 +\begin{solution}
1.161 +\label{s:impl}
1.162 +\begin{tabbing}
1.163 +\small\it
1.164 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
1.165 +\> \\
1.166 +\> \\
1.167 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
1.168 \>{\rm 02}\>\> {\tt LET} \\
1.169 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1.170 @@ -922,7 +968,9 @@
1.171 \>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\
1.172 \>{\rm 16}\>\> {\tt IN } \\
1.173 \>{\rm 15}\>\>\> X'\_eq
1.174 -\end{tabbing}}
1.175 +\end{tabbing}
1.176 +\end{solution}
1.177 +
1.178 % ORIGINAL FROM Inverse_Z_Transform.thy
1.179 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.180 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.181 @@ -944,9 +992,6 @@
1.182 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.183 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.184
1.185 -
1.186 -.\\.\\.\\
1.187 -
1.188 \section{Workflow of Programming in the Prototype}\label{workflow}
1.189
1.190 \subsection{Preparations and Trials}\label{flow-prep}