1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Wed Sep 12 17:38:44 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Wed Sep 12 21:14:15 2012 +0200
1.3 @@ -129,28 +129,20 @@
1.4 support, guiding the learner towards a solution, another kind of
1.5 technology is required. %TODO ... connect to prototype ...
1.6
1.7 -A prototype combines TP with a programming language, the latter
1.8 -interpreted in a specific way: certain statements in a program, called
1.9 -tactics, are treated as breakpoints where control is handed over to
1.10 -the user. An input formula is checked by TP (using logical context
1.11 -built up by the interpreter); and if a learner gets stuck, a program
1.12 -describing the steps towards a solution of a problem ``knows the next
1.13 -step''. This kind of interpretation is called Lucas-Interpretation for
1.14 -\emph{TP-based programming languages}.
1.15 +Both kinds of support can be acchieved by so-called
1.16 +Lucas-Interpretation which combines deduction and computation and, for
1.17 +the latter, uses a novel kind of programming language. This language
1.18 +is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
1.19 +programming language''.
1.20
1.21 -This paper describes the prototype's TP-based programming language
1.22 -within a case study creating interactive material for an advanced
1.23 -course in Signal Processing: implementation of definitions and
1.24 -theorems in TP, formal specification of a problem and step-wise
1.25 -development of the program solving the problem. Experiences with the
1.26 -ork flow in iterative development with testing and identifying errors
1.27 -are described, too. The description clarifies the components missing
1.28 -in the prototype's language as well as deficiencies experienced during
1.29 -programming.
1.30 -\par
1.31 -These experiences are particularly notable, because the author is the
1.32 -first programmer using the language beyond the core team which
1.33 -developed the prototype's TP-based language interpreter.
1.34 +This paper is the experience report of the first ``application
1.35 +programmer'' using this language, the experience gained from a
1.36 +prototype of the programming language and of it's interpreter.
1.37 +
1.38 +The report concludes with a positive proof of concept, states
1.39 +insuggicient usability of the prototype and captures the requirements
1.40 +for further development of both, the programming language and the
1.41 +interpreter.
1.42 %
1.43 \end{abstract}%
1.44 %
1.45 @@ -222,17 +214,17 @@
1.46 interpreter will be briefly re-introduced in order to make the paper
1.47 self-contained.
1.48
1.49 -\paragraph{The main part} of the paper is an account of first experiences
1.50 +The main part of the paper is an account of first experiences
1.51 with programming in this TP-based language. The experience was gained
1.52 in a case study by the author. The author was considered an ideal
1.53 candidate for this study for the following reasons: as a student in
1.54 Telematics (computer science with focus on Signal Processing) he had
1.55 general knowledge in programming as well as specific domain knowledge
1.56 -in Signal Processing; and he was not involved in the development of
1.57 +in Signal Processing; and he was {\em not} involved in the development of
1.58 {\sisac}'s programming language and interpeter, thus a novice to the
1.59 language.
1.60
1.61 -\paragraph{The goal} of the case study was (1) some TP-based programs for
1.62 +The goal of the case study was (1) some TP-based programs for
1.63 interactive course material for a specific ``Adavanced Signal
1.64 Processing Lab'' in a higher semester, (2) respective program
1.65 development with as little advice from the {\sisac}-team and (3) records
1.66 @@ -252,7 +244,7 @@
1.67 \end{figure}
1.68
1.69 The problem is from the domain of Signal Processing and requests to
1.70 -determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
1.71 +determine the inverse ${\cal Z}$-transform for a given term. Fig.\ref{fig-interactive}
1.72 also shows the beginning of the interactive construction of a solution
1.73 for the problem. This construction is done in the right window named
1.74 ``Worksheet''.
1.75 @@ -266,19 +258,19 @@
1.76 formal specification of the problem (here hidden from the user) by the
1.77 Lucas-Interpreter.
1.78 \item If the user gets stuck, the program developed below in this
1.79 -paper ``knows the next step'' from behind the scenes. How the latter
1.80 -TP-service is exploited by dialogue authoring is out of scope of this
1.81 +paper ``knows the next step'' and Lucas-Interpretation provides services
1.82 +featuring so-called ``next-step-guidance''; this is out of scope of this
1.83 paper and can be studied in~\cite{gdaroczy-EP-13}.
1.84 \end{enumerate} It should be noted that the programmer using the
1.85 TP-based language is not concerned with interaction at all; we will
1.86 see that the program contains neither input-statements nor
1.87 -output-statements. Rather, interaction is handled by services
1.88 -generated automatically.
1.89 -\par
1.90 -So there is a clear separation of concerns: Dialogues are
1.91 -adapted by dialogue authors (in Java-based tools), using automatically
1.92 -generated TP services, while the TP-based program is written by
1.93 -mathematics experts (in Isabelle/ML). The latter is concern of this
1.94 +output-statements. Rather, interaction is handled by the interpreter
1.95 +pf the language.
1.96 +
1.97 +So there is a clear separation of concerns: Dialogues are adapted by
1.98 +dialogue authors (in Java-based tools), using TP services provided by
1.99 +Lucas-Interpretation. The latter acts on programs developed by
1.100 +mathematics-authors (in Isabelle/ML); their task is concern of this
1.101 paper.
1.102
1.103 \paragraph{The paper is structed} as follows: The introduction
1.104 @@ -286,20 +278,21 @@
1.105 programming language in \S\ref{PL}, which extends the executable
1.106 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
1.107 play a specific role in Lucas-Interpretation and in providing the TP
1.108 -services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
1.109 +services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
1.110 the main steps in developing the program for the running example:
1.111 prepare domain knowledge, implement the formal specification of the
1.112 -problem, prepare the environment for the program, implement the
1.113 -program. The workflow of programming, debugging and testing is
1.114 +problem, prepare the environment for the interpreter, implement the
1.115 +program in \S\ref{isabisac} to \S\ref{progr} respectively.
1.116 +The workflow of programming, debugging and testing is
1.117 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
1.118 give directions identified for future development.
1.119
1.120
1.121 \section{\isac's Prototype for a Programming Language}\label{PL}
1.122 -The prototype's language extends the executable fragment in the
1.123 -language of the theorem prover
1.124 -Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
1.125 -by tactics which have a specific role in Lucas-Interpretation.
1.126 +The prototype of the language and of the Lucas-Interpreter are briefly
1.127 +described from the point of view of a programmer. The language extends
1.128 +the executable fragment in the language of the theorem prover
1.129 +Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
1.130
1.131 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
1.132 The executable fragment consists of data-type and function
1.133 @@ -374,7 +367,7 @@
1.134 The prototype extends Isabelle's language by specific statements
1.135 called tactics~\footnote{{\sisac}'s tactics are different from
1.136 Isabelle's tactics: the former concern steps in a calculation, the
1.137 -latter concern proof steps.} and tacticals. For the programmer these
1.138 +latter concern proofs.} and tacticals. For the programmer these
1.139 statements are functions with the following signatures:
1.140
1.141 \begin{description}
1.142 @@ -402,8 +395,10 @@
1.143 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
1.144 % list}$:
1.145
1.146 +%SPACEvvv
1.147 \item[Substitute:] ${\it substitution}\Rightarrow{\it
1.148 term}\Rightarrow{\it term}$: allows to access sub-terms.
1.149 +%SPACE^^^
1.150
1.151 \item[Take:] ${\it term}\Rightarrow{\it term}$:
1.152 this tactic has no effect in the program; but it creates a side-effect
1.153 @@ -425,7 +420,7 @@
1.154 break-points where, as a side-effect, a line is added to a calculation
1.155 as a protocol for proceeding towards a solution in step-wise problem
1.156 solving. At the same points Lucas-Interpretation serves interactive
1.157 -tutoring and control is handed over to the user. The user is free to
1.158 +tutoring and hands over control to the user. The user is free to
1.159 investigate underlying knowledge, applicable theorems, etc. And the
1.160 user can proceed constructing a solution by input of a tactic to be
1.161 applied or by input of a formula; in the latter case the
1.162 @@ -467,14 +462,14 @@
1.163 etc as long as the first {\it term} is true.
1.164 \end{description}
1.165 The tacticals are not treated as break-points by Lucas-Interpretation
1.166 -and thus do not contribute to the calculation nor to interaction.
1.167 +and thus do neither contribute to the calculation nor to interaction.
1.168
1.169 \section{Concepts and Tasks in TP-based Programming}\label{trial}
1.170 %\section{Development of a Program on Trial}
1.171
1.172 This section presents all the concepts involved in TP-based
1.173 programming and all the tasks to be accomplished by programmers. The
1.174 -presentation uses the running example which has been introduced in
1.175 +presentation uses the running example from
1.176 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
1.177
1.178 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.179 @@ -628,9 +623,9 @@
1.180 The running example requires to determine the inverse $\cal
1.181 Z$-transform for a class of functions. The domain of Signal Processing
1.182 is accustomed to specific notation for the resulting functions, which
1.183 -are absolutely summable and are called TODO: $u[n]$, where $u$ is the
1.184 +are absolutely summable and are called step-response: $u[n]$, where $u$ is the
1.185 function, $n$ is the argument and the brackets indicate that the
1.186 -arguments are TODO. Surprisingly, Isabelle accepts the rules for
1.187 +arguments are discrete. Surprisingly, Isabelle accepts the rules for
1.188 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.189 experts might be particularly surprised, that the brackets do not
1.190 cause errors in typing (as lists).}:
1.191 @@ -666,7 +661,7 @@
1.192 Isabelle provides a large body of knowledge, rigorously proven from
1.193 the basic axioms of mathematics~\footnote{This way of rigorously
1.194 deriving all knowledge from first principles is called the
1.195 -LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
1.196 +LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced
1.197 knowledge can be found in the theoris on Multivariate
1.198 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.199 building up knowledge such that a proof for the above rules would be
1.200 @@ -690,18 +685,19 @@
1.201 Processing.
1.202
1.203 TP-based programming, concern of this paper, is determined to
1.204 -add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
1.205 -p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.206 -starts with a formal {\em specification} of the problem to be solved.
1.207 -\begin{figure}
1.208 - \begin{center}
1.209 - \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.210 - \caption{The three-dimensional universe of mathematics knowledge}
1.211 - \label{fig:mathuni}
1.212 - \end{center}
1.213 -\end{figure}
1.214 -The language for both axes is defined in the axis at the bottom, deductive
1.215 -knowledge, in {\sisac} represented by Isabelle's theories.
1.216 +add ``algorithmic knowledge'' to the mechanised body of knowledge.
1.217 +% in Fig.\ref{fig:mathuni} on
1.218 +% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.219 +% starts with a formal {\em specification} of the problem to be solved.
1.220 +% \begin{figure}
1.221 +% \begin{center}
1.222 +% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.223 +% \caption{The three-dimensional universe of mathematics knowledge}
1.224 +% \label{fig:mathuni}
1.225 +% \end{center}
1.226 +% \end{figure}
1.227 +% The language for both axes is defined in the axis at the bottom, deductive
1.228 +% knowledge, in {\sisac} represented by Isabelle's theories.
1.229
1.230 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.231
1.232 @@ -865,11 +861,12 @@
1.233 %WN3 Bite bei der rewrite_set_ demo oben bitte schummeln !
1.234
1.235 \subsection{Preparation of ML-Functions}\label{funs}
1.236 -The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for
1.237 -all kinds of evaluation. Some functionality required in programming,
1.238 -however, cannot be accomplished by rewriting. So the prototype has a
1.239 -mechanism to call ML-functions during rewriting, and the programmer has
1.240 -to use this mechanism.
1.241 +Some functionality required in programming, cannot be accomplished by
1.242 +rewriting. So the prototype has a mechanism to call functions within
1.243 +the rewrite-engine: certain redexes in Isabelle terms call these
1.244 +functions written in SML~\cite{pl:milner97}, the implementation {\em
1.245 +and} meta-language of Isabelle. The programmer has to use this
1.246 +mechanism.
1.247
1.248 In the running example's program on p.\pageref{s:impl} the lines {\rm
1.249 05} and {\rm 06} contain such functions; we go into the details with
1.250 @@ -884,24 +881,24 @@
1.251 program source the constant needs to be declared in a theory, here in
1.252 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
1.253 the context \textit{ctxt} of that theory:
1.254 +
1.255 {\footnotesize
1.256 \begin{verbatim}
1.257 consts
1.258 - argument'_in :: "real => real" ("argument'_in _" 10)
1.259 + argument'_in :: "real => real" ("argument'_in _" 10)
1.260
1.261 ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.262 -
1.263 val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
1.264 $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
1.265 \end{verbatim}}
1.266
1.267 \noindent Parsing produces a term \texttt{t} in internal
1.268 -representation~\footnote{The attentive reader realizes the delicate
1.269 +representation~\footnote{The attentive reader realizes the
1.270 differences between interal and extermal representation even in the
1.271 strings, i.e \texttt{'\_}}, consisting of \texttt{Const
1.272 ("argument'\_in", type)} and the two variables \texttt{Free ("X",
1.273 type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
1.274 -constructor. The function body below is implemented directly in ML,
1.275 +constructor. The function body below is implemented directly in SML,
1.276 i.e in an \texttt{ML \{* *\}} block; the function definition provides
1.277 a unique prefix \texttt{eval\_} to the function name:
1.278
1.279 @@ -942,7 +939,7 @@
1.280 inside-out; however, the prototype's rewrite-engine only works top down
1.281 from the root of a term down to the leaves.
1.282
1.283 -How all these ugly technicalities are to be checked in the prototype is
1.284 +How all these technicalities are to be checked in the prototype is
1.285 shown in \S\ref{flow-prep} below.
1.286
1.287 % \paragraph{Explicit Problems} require explicit methods to solve them, and within
1.288 @@ -1042,10 +1039,10 @@
1.289 %WN <--> \chapter 7 der Thesis
1.290 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.291
1.292 -The problem of the running example is textually described in
1.293 -Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
1.294 -formal} specification of this problem, in traditional mathematical
1.295 -notation, could look like is this:
1.296 +Mechanical treatment requires to translate a textual problem
1.297 +description like in Fig.\ref{fig-interactive} on
1.298 +p.\pageref{fig-interactive} into a {\em formal} specification. The
1.299 +formal specification of the running example could look like is this:
1.300
1.301 %WN Hier brauchen wir die Spezifikation des 'running example' ...
1.302 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.303 @@ -1054,15 +1051,16 @@
1.304 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.305 %JR2 done
1.306
1.307 - \label{eg:neuper2}
1.308 - {\small\begin{tabbing}
1.309 - 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.310 - \hfill \\
1.311 - Specification:\\
1.312 - \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.313 - \>precond \>: filterExpression continius on $\mathbb{R}$ \\
1.314 - \>output \>: stepResponse $x[n]$ \\
1.315 - \>postcond \>: TODO\\ \end{tabbing}}
1.316 +\label{eg:neuper2}
1.317 +{\small\begin{tabbing}
1.318 + 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.319 + %\hfill \\
1.320 + \>Specification:\\
1.321 + \> \>input \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.322 + \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1.323 + \>\>output \>: stepResponse $x[n]$ \\
1.324 + \>\>postcond \>: TODO
1.325 +\end{tabbing}}
1.326
1.327 %JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1.328
1.329 @@ -1075,25 +1073,30 @@
1.330 % \label{rm:postcond}
1.331 % \end{remark}
1.332
1.333 -\paragraph{The implementation} of the formal specification in the present
1.334 -prototype, still bar-bones without support for authoring:
1.335 +The implementation of the formal specification in the present
1.336 +prototype, still bar-bones without support for authoring, is done
1.337 +like that:
1.338 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.339 +
1.340 {\footnotesize\label{exp-spec}
1.341 \begin{verbatim}
1.342 + 00 ML {*
1.343 01 store_specification
1.344 02 (prepare_specification
1.345 - 03 ["Jan Rocnik"]
1.346 - 04 "pbl_SP_Ztrans_inv"
1.347 + 03 "pbl_SP_Ztrans_inv"
1.348 + 04 ["Jan Rocnik"]
1.349 05 thy
1.350 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.351 07 [ ("#Given", ["filterExpression X_eq"]),
1.352 - 08 ("#Pre" , ["X_eq is_continuous"]),
1.353 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
1.354 09 ("#Find" , ["stepResponse n_eq"]),
1.355 10 ("#Post" , [" TODO "])],
1.356 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.357 12 NONE,
1.358 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.359 + 14 *}
1.360 \end{verbatim}}
1.361 +
1.362 Although the above details are partly very technical, we explain them
1.363 in order to document some intricacies of TP-based programming in the
1.364 present state of the {\sisac} prototype:
1.365 @@ -1105,12 +1108,11 @@
1.366 parallel execution~\cite{Makarius-09:parall-proof} and is under
1.367 reconstruction already.
1.368
1.369 -\textit{prep\_pbt:} translates the specification to an internal format
1.370 +\textit{prep\_specification:} translates the specification to an internal format
1.371 which allows efficient processing; see for instance line {\rm 07}
1.372 below.
1.373 -\item[03..04] are the ``mathematics author'' holding the copy-rights
1.374 -and a unique identifier for the specification within {\sisac},
1.375 -complare line {\rm 06}.
1.376 +\item[03..04] are a unique identifier for the specification within {\sisac}
1.377 +and the ``mathematics author'' holding the copy-rights.
1.378 \item[05] is the Isabelle \textit{theory} required to parse the
1.379 specification in lines {\rm 07..10}.
1.380 \item[06] is a key into the tree of all specifications as presented to
1.381 @@ -1118,16 +1120,15 @@
1.382 component).
1.383 \item[07..10] are the specification with input, pre-condition, output
1.384 and post-condition respectively; the post-condition is not handled in
1.385 -the prototype presently. (Follow up Remark~\ref{rm:postcond})
1.386 -\item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.387 +the prototype presently.
1.388 +\item[11] creates a rule-set (abbreviated \textit{rls} in
1.389 {\sisac}) which evaluates the pre-condition for the actual input data.
1.390 -Only if the evaluation yields \textit{True}, a program con be started.
1.391 +Only if the evaluation yields \textit{True}, a program can be started.
1.392 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.393 problem associated to a function from Computer Algebra (like an
1.394 equation solver) which is not the case here.
1.395 -\item[13] is the specific key into the tree of programs addressing a
1.396 -method which is able to find a solution which satiesfies the
1.397 -post-condition of the specification.
1.398 +\item[13] is a list of methods solving the specified problem (here
1.399 +only one list item) represented analogously to {\rm 06}.
1.400 \end{description}
1.401
1.402
1.403 @@ -1184,69 +1185,95 @@
1.404 % }
1.405
1.406 \subsection{Implementation of the Method}\label{meth}
1.407 -
1.408 -The methods represent the different ways a problem can be solved. This can
1.409 -include mathematical tactics as well as tactics taught in different courses.
1.410 -Declaring the Method itself gives us the possibilities to describe the way of
1.411 -calculation in deep, as well we get the oppertunities to build in different
1.412 -rulesets.
1.413 +A method collects all data required to interpret a certain program by
1.414 +Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1.415 +the running example is embedded in the following method:
1.416 +%The methods represent the different ways a problem can be solved. This can
1.417 +%include mathematical tactics as well as tactics taught in different courses.
1.418 +%Declaring the Method itself gives us the possibilities to describe the way of
1.419 +%calculation in deep, as well we get the oppertunities to build in different
1.420 +%rulesets.
1.421
1.422 {\footnotesize
1.423 \begin{verbatim}
1.424 -01 store_met
1.425 -02 (prep_met thy "SP_InverseZTransformation_classic" [] e_metID
1.426 -03 (["SignalProcessing", "Z_Transform", "Inverse"],
1.427 -04 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.428 -05 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.429 -06 {rew_ord'="tless_true",
1.430 -07 rls = rls,
1.431 -08 calc = [],
1.432 -09 srls = e_rls,
1.433 -10 prls = e_rls,
1.434 -11 crls = e_rls,
1.435 -12 errpats = [],
1.436 -13 nrls = e_rls},
1.437 -14 "empty_program"
1.438 -15 ));
1.439 -\end{verbatim}
1.440 -}
1.441 + 00 ML {*
1.442 + 01 store_method
1.443 + 02 (prep_method
1.444 + 03 "SP_InverseZTransformation_classic"
1.445 + 04 ["Jan Rocnik"]
1.446 + 05 thy
1.447 + 06 (["SignalProcessing", "Z_Transform", "Inverse"],
1.448 + 07 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.449 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
1.450 + 09 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.451 + 10 {rew_ord = tless_true, rls = rls,
1.452 + 11 srls = srls, calc = [],
1.453 + 12 prls = prls, crls = crls,
1.454 + 13 nrls = nrls,
1.455 + 14 errpats = []},
1.456 + 15 program));
1.457 + 16 *}
1.458 +\end{verbatim}}
1.459
1.460 -The above code is again very technical and goes hard in detail. Unfortunataly
1.461 -most declerations are not essential for a basic programm but leads us to a huge
1.462 -range of powerful possibilities.
1.463 +\noindent The above code stores the whole structure analogously to a
1.464 +specification,
1.465 +\begin{description}
1.466 +\item[01..06] are identical to those for the example specification on
1.467 +p.\pageref{exp-spec}.
1.468
1.469 -\begin{description}
1.470 -\item[01..02] stores the method with the given name into the system under a global
1.471 -reference.
1.472 -\item[03] specifies the topic within which context the method can be found.
1.473 -\item[04..05] as the requirements for different methods can be deviant we
1.474 -declare what is \emph{given} and and what to \emph{find} for this specific method.
1.475 -The code again helds on the topic of the case studie, where the inverse
1.476 -z-transformation does a switch between a term describing a electrical filter into
1.477 -its step response. Also the datatype has to be declared (bool - due the fact that
1.478 -we handle equations).
1.479 -\item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1.480 -theorem of it is used for rewriting one single step.
1.481 -\item[07] \texttt{rls} is the currently used ruleset for this method. This set
1.482 -has already been defined before.
1.483 -\item[08] we would have the possiblitiy to add this method to a predefined tree of
1.484 -calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1.485 -independend.
1.486 -\item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1.487 -the source.
1.488 -\item[10] \emph{predicates ruleset} can be used to indicates predicates within
1.489 -model patterns.
1.490 -\item[11] The \emph{check ruleset} summarizes rules for checking formulas
1.491 -elementwise.
1.492 -\item[12] \emph{error patterns} which are expected in this kind of method can be
1.493 -pre-specified to recognize them during the method.
1.494 -\item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1.495 -of the specific method.
1.496 -\item[14] for this code snipset we don't specify the programm itself and keep it
1.497 -empty. Follow up \S\ref{progr} for informations on how to implement this
1.498 -\textit{main} part.
1.499 +\item[07..09] show something looking like the specification; this is a
1.500 +{\em guard}: as long as not all \texttt{Given} items are present and
1.501 +the \texttt{Pre}-conditions is not true, interpretation of the program
1.502 +is not started.
1.503 +
1.504 +\item[01..09]
1.505 +
1.506 +\item[01..09]
1.507 +
1.508 +\item[01..09]
1.509 +
1.510 +\item[01..09]
1.511 \end{description}
1.512
1.513 +
1.514 +.\\.\\.\\
1.515 +
1.516 +% is again very technical and goes hard in detail. Unfortunataly
1.517 +% most declerations are not essential for a basic programm but leads us to a huge
1.518 +% range of powerful possibilities.
1.519 +%
1.520 +% \begin{description}
1.521 +% \item[01..02] stores the method with the given name into the system under a global
1.522 +% reference.
1.523 +% \item[03] specifies the topic within which context the method can be found.
1.524 +% \item[04..05] as the requirements for different methods can be deviant we
1.525 +% declare what is \emph{given} and and what to \emph{find} for this specific method.
1.526 +% The code again helds on the topic of the case studie, where the inverse
1.527 +% z-transformation does a switch between a term describing a electrical filter into
1.528 +% its step response. Also the datatype has to be declared (bool - due the fact that
1.529 +% we handle equations).
1.530 +% \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1.531 +% theorem of it is used for rewriting one single step.
1.532 +% \item[07] \texttt{rls} is the currently used ruleset for this method. This set
1.533 +% has already been defined before.
1.534 +% \item[08] we would have the possiblitiy to add this method to a predefined tree of
1.535 +% calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1.536 +% independend.
1.537 +% \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1.538 +% the source.
1.539 +% \item[10] \emph{predicates ruleset} can be used to indicates predicates within
1.540 +% model patterns.
1.541 +% \item[11] The \emph{check ruleset} summarizes rules for checking formulas
1.542 +% elementwise.
1.543 +% \item[12] \emph{error patterns} which are expected in this kind of method can be
1.544 +% pre-specified to recognize them during the method.
1.545 +% \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1.546 +% of the specific method.
1.547 +% \item[14] for this code snipset we don't specify the programm itself and keep it
1.548 +% empty. Follow up \S\ref{progr} for informations on how to implement this
1.549 +% \textit{main} part.
1.550 +% \end{description}
1.551 +
1.552 \subsection{Implementation of the TP-based Program}\label{progr}
1.553 So finally all the prerequisites are described and the very topic can
1.554 be addressed. The program below comes back to the running example: it
1.555 @@ -1257,6 +1284,7 @@
1.556 {\footnotesize\it\label{s:impl}
1.557 \begin{tabbing}
1.558 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.559 +\> \>ML \{*
1.560 \>{\rm 00}\>val program =\\
1.561 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1.562 \>{\rm 02}\>\> {\tt let} \\
1.563 @@ -1272,7 +1300,8 @@
1.564 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
1.565 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1.566 \>{\rm 13}\>\> {\tt in } \\
1.567 -\>{\rm 14}\>\>\> X'\_eq"
1.568 +\>{\rm 14}\>\>\> X'\_eq"\\
1.569 +\> \>*\}
1.570 \end{tabbing}}
1.571 % ORIGINAL FROM Inverse_Z_Transform.thy
1.572 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)