wneuper/isa: comparison doc-src/isac/jrocnik/eJMT-paper/jrocnik

equal deleted inserted replaced

-:aafbbd5a85a5
+:36e2e192f716
 reasonably short and easily comprehensible, still requires lots of
 work (and is definitely out of scope of our case study).
 \paragraph{At the state-of-the-art in mechanization of knowledge} in
 engineering sciences, the process does not stop with the mechanization of
-mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
+mathematics traditionally used in these sciences. Rather, ``Formal Methods''.
+%% \cite{TODO-formal-methods}
 are expected to proceed to formal and explicit description of physical items.  Signal Processing,
 for instance is concerned with physical devices for signal acquisition
 and reconstruction, which involve measuring a physical signal, storing
 it, and possibly later rebuilding the original signal or an
 approximation thereof. For digital systems, this typically includes
 sampling and quantization; devices for signal compression, including
 audio compression, image compression, and video compression, etc.
-``Domain engineering''\cite{db-domain-engineering} is concerned with
+``Domain engineering''
+%% \cite{db-domain-engineering}
+is concerned with
 {\em specification} of these devices' components and features; this
 part in the process of mechanization is only at the beginning in domains
 like Signal Processing.
 \subparagraph{TP-based programming, concern of this paper,} is determined to
 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
 formal} specification of this problem, in traditional mathematical
 notation, could look like is this:
 %WN Hier brauchen wir die Spezifikation des 'running example' ...
 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
 %JR der post condition - die existiert für uns ja eigentlich nicht aka
 %JR haben sie bis jetzt nicht beachtet WN...
 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
+%JR2 done
 \label{eg:neuper2}
 {\small\begin{tabbing}
 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
 \hfill \\
 \>input    \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
 \>precond  \>: filterExpression continius on $\mathbb{R}$ \\
 \>output   \>: stepResponse $x[n]$ \\
 \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
-\paragraph{Remark on post-conditions:} Defining the postcondition requires a
+\begin{remark}
-high amount mathematical knowledge, the difficult part in our case is not to
+Defining the postcondition requires a high amount mathematical
-set up this condition nor it is more to define it in a way the interpreter is
+knowledge, the difficult part in our case is not to set up this condition
-able to handle it. Due the fact that implementing that mechanisms is quite
+nor it is more to define it in a way the interpreter is able to handle it.
-the same amount as creating the programm itself, it is not avaible in our
+Due the fact that implementing that mechanisms is quite the same amount as
-prototype.\label{rm:postcond}
+creating the programm itself, it is not avaible in our prototype.
+\label{rm:postcond}
+\end{remark}
 \paragraph{The implementation} of the formal specification in the present
 prototype, still bar-bones without support for authoring:
 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
 {\footnotesize
 \item[06] is a key into the tree of all specifications as presented to
 the user (where some branches might be hidden by the dialog
 component).
 \item[07..10] are the specification with input, pre-condition, output
 and post-condition respectively; the post-condition is not handled in
-the prototype presently. (Follow up Remark in Section~\ref{rm:postcond})
+the prototype presently. (Follow up Remark~\ref{rm:postcond})
 \item[11] creates a term rewriting system (abbreviated \textit{rls} in
 {\sisac}) which evaluates the pre-condition for the actual input data.
 Only if the evaluation yields \textit{True}, a program con be started.
 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
 problem associated to a function from Computer Algebra (like an
 a special problem or refindable in other problems. No mather what case, such
 steps often require some technical functions behind. For the solving process
 of the Inverse Z Transformation and the corresponding partial fraction it was
 neccessary to build helping functions like \texttt{get\_denominator},
 \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
-to filter the deonimonator or numerator out of a fraction, last one helps us to
+to filter the denominator or numerator out of a fraction, last one helps us to
 get to know the bound variable in a equation.
 \par
-By taking \texttt{get\_denominator} we want to explain how to implement new
+By taking \texttt{get\_denominator} as an example, we want to explain how to
-functions into the existing system and how we can later use them in our program.
+implement new functions into the existing system and how we can later use them
+in our program.
 \subsubsection{Find a place to Store the Function}
 The whole system builds up on a well defined structure of Knowledge. This
-Knowledge sets up at the Path: \ttfamily src/Tools/isac/Knowledge\normalfont.
+Knowledge sets up at the Path:
+\begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
 For implementing the Function \texttt{get\_denominator} (which let us extract
 the denominator out of a fraction) we have choosen the Theory (file)
 \texttt{Rational.thy}.
 \subsubsection{Write down the new Function}
 In upper Theory we now define the new function and its purpose:
 \begin{verbatim}
 get_denominator :: "real => real"
 \end{verbatim}
 This command tells the machine that a function with the name
 \texttt{get\_denominator} exists which gets a real expression as argument and
-returns once again a real expression. Now we are able to implement the function itself, Example~\ref{eg:getdenom}
+returns once again a real expression. Now we are able to implement the function
-shows the implementation of \texttt{get\_denominator}.
+itself, Example~\ref{eg:getdenom} now shows the implementation of
+\texttt{get\_denominator}.
 \begin{example}
 \label{eg:getdenom}
 \begin{verbatim}
 \end{example}
 Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
 there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
 splittet
-into its two parts (\texttt{ \$num \$denom}). The lines before are additionals
+into its two parts (\texttt{\$num \$denom}). The lines before are additionals
 commands for declaring the function and the lines after are modeling and
 returning a real variable out of \texttt{\$denom}.
 \subsubsection{Add a test for the new Function}
-\subsubsection{Use the new Function}
+\paragraph{Everytime when adding} a new function it is essential also to add
+a test for it. Tests for all functions are sorted in the same structure as the
+knowledge it self and can be found up from the path:
+\begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
+This tests are nothing very special, as a first prototype the functionallity
+of a function can be checked by evaluating the result of a simple expression
+passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
+\textit{just} created function \texttt{get\_denominator}.
+\begin{example}
+\label{eg:getdenomtest}
+\begin{verbatim}
+01 val thy = @{theory Isac};
+02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
+03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
+04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
+05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
+\end{example}
+\begin{description}
+\item[01] checks if the proofer set up on our {\sisac{}} System.
+\item[02] passes a simple expression (fraction) to our suddenly created
+function.
+\item[04] checks if the resulting variable is the correct one (in this case
+``b'' the denominator) and returns.
+\item[05] handels the error case and reports that the function is not able to
+solve the given problem.
+\end{description}
 \subsection{Implementation of the TP-based Program}\label{progr}
-%WN <--> \chapter 8 der Thesis
-.\\.\\.\\
+\paragraph{After introducing} neccesarry informations about the {\sisac{}}
+System, the main part of a implementation in the TP-bases language can be shown.
-{\small\it\begin{tabbing}
+\par
+Solution~\ref{s:impl} shows us the implementation of the
+Inverse-Z-Transformation, a description on the code is given afterwards.
+\begin{solution}
+\label{s:impl}
+\begin{tabbing}
+\small\it
 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
+\> \\
+\> \\
 \>{\rm 01}\>  {\tt Program} InverseZTransform (X\_eq::bool) =   \\
 \>{\rm 02}\>\>  {\tt LET}                                       \\
 \>{\rm 03}\>\>\>  X\_eq = {\tt Take} X\_eq ;   \\
 \>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
 \>{\rm 05}\>\>\>  (X\_z::real) = lhs X\_eq ;       \\ %no inside-out evaluation
 \>{\rm 12}\>\>\>  X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ;   \\
 \>{\rm 15}\>\>\>  X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\
 \>{\rm 16}\>\>  {\tt IN } \\
 \>{\rm 15}\>\>\>  X'\_eq
-\end{tabbing}}
+\end{tabbing}
+\end{solution}
 % ORIGINAL FROM Inverse_Z_Transform.thy
 % "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
 % "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
 % "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
 % "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
 % "  pbz_eq = drop_questionmarks pbz_eq;              "^(*               4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
 % "  (X_zeq::bool) = Take (X_z = rhs pbz_eq);         "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
 % "  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]*)
 % "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
 % "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
-.\\.\\.\\
 \section{Workflow of Programming in the Prototype}\label{workflow}
 \subsection{Preparations and Trials}\label{flow-prep}
 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''

changeset 42473	36e2e192f716
parent 42470	aafbbd5a85a5
child 42475	d856a6f9e82a
child 42477	3c0590a3a3b5