1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 21:14:20 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 21:18:00 2012 +0200
1.3 @@ -704,175 +704,6 @@
1.4 The language for both axes is defined in the axis at the bottom, deductive
1.5 knowledge, in {\sisac} represented by Isabelle's theories.
1.6
1.7 -\subsection{Specification of the Problem}\label{spec}
1.8 -%WN <--> \chapter 7 der Thesis
1.9 -%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.10 -
1.11 -The problem of the running example is textually described in
1.12 -Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
1.13 -formal} specification of this problem, in traditional mathematical
1.14 -notation, could look like is this:
1.15 -
1.16 -%WN Hier brauchen wir die Spezifikation des 'running example' ...
1.17 -%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.18 -%JR der post condition - die existiert für uns ja eigentlich nicht aka
1.19 -%JR haben sie bis jetzt nicht beachtet WN...
1.20 -%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.21 -%JR2 done
1.22 -
1.23 - \label{eg:neuper2}
1.24 - {\small\begin{tabbing}
1.25 - 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.26 - \hfill \\
1.27 - Specification:\\
1.28 - \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.29 - \>precond \>: filterExpression continius on $\mathbb{R}$ \\
1.30 - \>output \>: stepResponse $x[n]$ \\
1.31 - \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
1.32 -
1.33 -\begin{remark}
1.34 - Defining the postcondition requires a high amount mathematical
1.35 - knowledge, the difficult part in our case is not to set up this condition
1.36 - nor it is more to define it in a way the interpreter is able to handle it.
1.37 - Due the fact that implementing that mechanisms is quite the same amount as
1.38 - creating the programm itself, it is not avaible in our prototype.
1.39 - \label{rm:postcond}
1.40 -\end{remark}
1.41 -
1.42 -\paragraph{The implementation} of the formal specification in the present
1.43 -prototype, still bar-bones without support for authoring:
1.44 -%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.45 -{\footnotesize\label{exp-spec}
1.46 -\begin{verbatim}
1.47 - 01 store_specification
1.48 - 02 (prepare_specification
1.49 - 03 ["Jan Rocnik"]
1.50 - 04 "pbl_SP_Ztrans_inv"
1.51 - 05 thy
1.52 - 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.53 - 07 [ ("#Given", ["filterExpression X_eq"]),
1.54 - 08 ("#Pre" , ["X_eq is_continuous"]),
1.55 - 19 ("#Find" , ["stepResponse n_eq"]),
1.56 - 10 ("#Post" , [" TODO "])],
1.57 - 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.58 - 12 NONE,
1.59 - 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.60 -\end{verbatim}}
1.61 -Although the above details are partly very technical, we explain them
1.62 -in order to document some intricacies of TP-based programming in the
1.63 -present state of the {\sisac} prototype:
1.64 -\begin{description}
1.65 -\item[01..02]\textit{store\_specification:} stores the result of the
1.66 -function \textit{prep\_specification} in a global reference
1.67 -\textit{Unsynchronized.ref}, which causes principal conflicts with
1.68 -Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1.69 -parallel execution~\cite{Makarius-09:parall-proof} and is under
1.70 -reconstruction already.
1.71 -
1.72 -\textit{prep\_pbt:} translates the specification to an internal format
1.73 -which allows efficient processing; see for instance line {\rm 07}
1.74 -below.
1.75 -\item[03..04] are the ``mathematics author'' holding the copy-rights
1.76 -and a unique identifier for the specification within {\sisac},
1.77 -complare line {\rm 06}.
1.78 -\item[05] is the Isabelle \textit{theory} required to parse the
1.79 -specification in lines {\rm 07..10}.
1.80 -\item[06] is a key into the tree of all specifications as presented to
1.81 -the user (where some branches might be hidden by the dialog
1.82 -component).
1.83 -\item[07..10] are the specification with input, pre-condition, output
1.84 -and post-condition respectively; the post-condition is not handled in
1.85 -the prototype presently. (Follow up Remark~\ref{rm:postcond})
1.86 -\item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.87 -{\sisac}) which evaluates the pre-condition for the actual input data.
1.88 -Only if the evaluation yields \textit{True}, a program con be started.
1.89 -\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.90 -problem associated to a function from Computer Algebra (like an
1.91 -equation solver) which is not the case here.
1.92 -\item[13] is the specific key into the tree of programs addressing a
1.93 -method which is able to find a solution which satiesfies the
1.94 -post-condition of the specification.
1.95 -\end{description}
1.96 -
1.97 -
1.98 -%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1.99 -%WN ...
1.100 -% type pbt =
1.101 -% {guh : guh, (*unique within this isac-knowledge*)
1.102 -% mathauthors: string list, (*copyright*)
1.103 -% init : pblID, (*to start refinement with*)
1.104 -% thy : theory, (* which allows to compile that pbt
1.105 -% TODO: search generalized for subthy (ref.p.69*)
1.106 -% (*^^^ WN050912 NOT used during application of the problem,
1.107 -% because applied terms may be from 'subthy' as well as from super;
1.108 -% thus we take 'maxthy'; see match_ags !*)
1.109 -% cas : term option,(*'CAS-command'*)
1.110 -% prls : rls, (* for preds in where_*)
1.111 -% where_: term list, (* where - predicates*)
1.112 -% ppc : pat list,
1.113 -% (*this is the model-pattern;
1.114 -% it contains "#Given","#Where","#Find","#Relate"-patterns
1.115 -% for constraints on identifiers see "fun cpy_nam"*)
1.116 -% met : metID list}; (* methods solving the pbt*)
1.117 -%
1.118 -%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1.119 -%WN oben selbst geschrieben.
1.120 -
1.121 -
1.122 -
1.123 -
1.124 -%WN das w"urde ich in \sec\label{progr} verschieben und
1.125 -%WN das SubProblem partial fractions zum Erkl"aren verwenden.
1.126 -% Such a specification is checked before the execution of a program is
1.127 -% started, the same applies for sub-programs. In the following example
1.128 -% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1.129 -%
1.130 -% \vbox{
1.131 -% \begin{example}
1.132 -% \label{eg:subprob}
1.133 -% \hfill \\
1.134 -% {\ttfamily \begin{tabbing}
1.135 -% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1.136 -% ``\>\>[linear,univariate,equation,test],'' \\
1.137 -% ``\>\>[Test,solve\_linear])'' \\
1.138 -% ``\>[BOOL equ, REAL z])'' \\
1.139 -% \end{tabbing}
1.140 -% }
1.141 -% {\small\textit{
1.142 -% \noindent If a program requires a result which has to be
1.143 -% calculated first we can use a subproblem to do so. In our specific
1.144 -% case we wanted to calculate the zeros of a fraction and used a
1.145 -% subproblem to calculate the zeros of the denominator polynom.
1.146 -% }}
1.147 -% \end{example}
1.148 -% }
1.149 -
1.150 -\subsection{Implementation of the Method}\label{meth}
1.151 -
1.152 -\paragraph{todo}
1.153 -
1.154 -\begin{example}
1.155 -\begin{verbatim}
1.156 -
1.157 -01 store_met
1.158 -02 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.159 -03 (["SignalProcessing", "Z_Transform", "Inverse"],
1.160 -04 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.161 -05 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.162 -06 {rew_ord'="tless_true",
1.163 -07 rls'= e_rls,
1.164 -08 calc = [],
1.165 -09 srls = e_rls,
1.166 -10 prls = e_rls,
1.167 -11 crls = e_rls,
1.168 -12 errpats = [],
1.169 -13 nrls = e_rls},
1.170 -14 "empty_script"
1.171 -15 ));
1.172 -\end{verbatim}
1.173 -\end{example}
1.174 -
1.175 -
1.176 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.177
1.178 \paragraph{If it is clear} how the later calculation should look like and when
1.179 @@ -1039,6 +870,174 @@
1.180 solve the given problem.
1.181 \end{description}
1.182
1.183 +\subsection{Specification of the Problem}\label{spec}
1.184 +%WN <--> \chapter 7 der Thesis
1.185 +%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.186 +
1.187 +The problem of the running example is textually described in
1.188 +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
1.189 +formal} specification of this problem, in traditional mathematical
1.190 +notation, could look like is this:
1.191 +
1.192 +%WN Hier brauchen wir die Spezifikation des 'running example' ...
1.193 +%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.194 +%JR der post condition - die existiert für uns ja eigentlich nicht aka
1.195 +%JR haben sie bis jetzt nicht beachtet WN...
1.196 +%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.197 +%JR2 done
1.198 +
1.199 + \label{eg:neuper2}
1.200 + {\small\begin{tabbing}
1.201 + 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.202 + \hfill \\
1.203 + Specification:\\
1.204 + \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.205 + \>precond \>: filterExpression continius on $\mathbb{R}$ \\
1.206 + \>output \>: stepResponse $x[n]$ \\
1.207 + \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
1.208 +
1.209 +\begin{remark}
1.210 + Defining the postcondition requires a high amount mathematical
1.211 + knowledge, the difficult part in our case is not to set up this condition
1.212 + nor it is more to define it in a way the interpreter is able to handle it.
1.213 + Due the fact that implementing that mechanisms is quite the same amount as
1.214 + creating the programm itself, it is not avaible in our prototype.
1.215 + \label{rm:postcond}
1.216 +\end{remark}
1.217 +
1.218 +\paragraph{The implementation} of the formal specification in the present
1.219 +prototype, still bar-bones without support for authoring:
1.220 +%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.221 +{\footnotesize\label{exp-spec}
1.222 +\begin{verbatim}
1.223 + 01 store_specification
1.224 + 02 (prepare_specification
1.225 + 03 ["Jan Rocnik"]
1.226 + 04 "pbl_SP_Ztrans_inv"
1.227 + 05 thy
1.228 + 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.229 + 07 [ ("#Given", ["filterExpression X_eq"]),
1.230 + 08 ("#Pre" , ["X_eq is_continuous"]),
1.231 + 19 ("#Find" , ["stepResponse n_eq"]),
1.232 + 10 ("#Post" , [" TODO "])],
1.233 + 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.234 + 12 NONE,
1.235 + 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.236 +\end{verbatim}}
1.237 +Although the above details are partly very technical, we explain them
1.238 +in order to document some intricacies of TP-based programming in the
1.239 +present state of the {\sisac} prototype:
1.240 +\begin{description}
1.241 +\item[01..02]\textit{store\_specification:} stores the result of the
1.242 +function \textit{prep\_specification} in a global reference
1.243 +\textit{Unsynchronized.ref}, which causes principal conflicts with
1.244 +Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1.245 +parallel execution~\cite{Makarius-09:parall-proof} and is under
1.246 +reconstruction already.
1.247 +
1.248 +\textit{prep\_pbt:} translates the specification to an internal format
1.249 +which allows efficient processing; see for instance line {\rm 07}
1.250 +below.
1.251 +\item[03..04] are the ``mathematics author'' holding the copy-rights
1.252 +and a unique identifier for the specification within {\sisac},
1.253 +complare line {\rm 06}.
1.254 +\item[05] is the Isabelle \textit{theory} required to parse the
1.255 +specification in lines {\rm 07..10}.
1.256 +\item[06] is a key into the tree of all specifications as presented to
1.257 +the user (where some branches might be hidden by the dialog
1.258 +component).
1.259 +\item[07..10] are the specification with input, pre-condition, output
1.260 +and post-condition respectively; the post-condition is not handled in
1.261 +the prototype presently. (Follow up Remark~\ref{rm:postcond})
1.262 +\item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.263 +{\sisac}) which evaluates the pre-condition for the actual input data.
1.264 +Only if the evaluation yields \textit{True}, a program con be started.
1.265 +\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.266 +problem associated to a function from Computer Algebra (like an
1.267 +equation solver) which is not the case here.
1.268 +\item[13] is the specific key into the tree of programs addressing a
1.269 +method which is able to find a solution which satiesfies the
1.270 +post-condition of the specification.
1.271 +\end{description}
1.272 +
1.273 +
1.274 +%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1.275 +%WN ...
1.276 +% type pbt =
1.277 +% {guh : guh, (*unique within this isac-knowledge*)
1.278 +% mathauthors: string list, (*copyright*)
1.279 +% init : pblID, (*to start refinement with*)
1.280 +% thy : theory, (* which allows to compile that pbt
1.281 +% TODO: search generalized for subthy (ref.p.69*)
1.282 +% (*^^^ WN050912 NOT used during application of the problem,
1.283 +% because applied terms may be from 'subthy' as well as from super;
1.284 +% thus we take 'maxthy'; see match_ags !*)
1.285 +% cas : term option,(*'CAS-command'*)
1.286 +% prls : rls, (* for preds in where_*)
1.287 +% where_: term list, (* where - predicates*)
1.288 +% ppc : pat list,
1.289 +% (*this is the model-pattern;
1.290 +% it contains "#Given","#Where","#Find","#Relate"-patterns
1.291 +% for constraints on identifiers see "fun cpy_nam"*)
1.292 +% met : metID list}; (* methods solving the pbt*)
1.293 +%
1.294 +%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1.295 +%WN oben selbst geschrieben.
1.296 +
1.297 +
1.298 +
1.299 +
1.300 +%WN das w"urde ich in \sec\label{progr} verschieben und
1.301 +%WN das SubProblem partial fractions zum Erkl"aren verwenden.
1.302 +% Such a specification is checked before the execution of a program is
1.303 +% started, the same applies for sub-programs. In the following example
1.304 +% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1.305 +%
1.306 +% \vbox{
1.307 +% \begin{example}
1.308 +% \label{eg:subprob}
1.309 +% \hfill \\
1.310 +% {\ttfamily \begin{tabbing}
1.311 +% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1.312 +% ``\>\>[linear,univariate,equation,test],'' \\
1.313 +% ``\>\>[Test,solve\_linear])'' \\
1.314 +% ``\>[BOOL equ, REAL z])'' \\
1.315 +% \end{tabbing}
1.316 +% }
1.317 +% {\small\textit{
1.318 +% \noindent If a program requires a result which has to be
1.319 +% calculated first we can use a subproblem to do so. In our specific
1.320 +% case we wanted to calculate the zeros of a fraction and used a
1.321 +% subproblem to calculate the zeros of the denominator polynom.
1.322 +% }}
1.323 +% \end{example}
1.324 +% }
1.325 +
1.326 +\subsection{Implementation of the Method}\label{meth}
1.327 +
1.328 +\paragraph{todo}
1.329 +
1.330 +\begin{example}
1.331 +\begin{verbatim}
1.332 +
1.333 +01 store_met
1.334 +02 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.335 +03 (["SignalProcessing", "Z_Transform", "Inverse"],
1.336 +04 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.337 +05 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.338 +06 {rew_ord'="tless_true",
1.339 +07 rls'= e_rls,
1.340 +08 calc = [],
1.341 +09 srls = e_rls,
1.342 +10 prls = e_rls,
1.343 +11 crls = e_rls,
1.344 +12 errpats = [],
1.345 +13 nrls = e_rls},
1.346 +14 "empty_script"
1.347 +15 ));
1.348 +\end{verbatim}
1.349 +\end{example}
1.350 +
1.351 \subsection{Implementation of the TP-based Program}\label{progr}
1.352 So finally all the prerequisites are described and the very topic can
1.353 be addressed. The program below comes back to the running example: it