\subsection{Specification of the Problem}\label{spec}

 %WN <--> \chapter 7 der Thesis

 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..

 The problem of the running example is textually described in

 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 \\

   Specification:\\

     \>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}}

 \begin{remark}

    Defining the postcondition requires a high amount mathematical 

    knowledge, the difficult part in our case is not to set up this condition 

    nor it is more to define it in a way the interpreter is able to handle it. 

    Due the fact that implementing that mechanisms is quite the same amount as 

    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\label{exp-spec}

 \begin{verbatim}

    01  store_specification

    02    (prepare_specification

    03      ["Jan Rocnik"]

    04      "pbl_SP_Ztrans_inv"

    05      thy

    06      ( ["Inverse", "Z_Transform", "SignalProcessing"],

    07        [ ("#Given", ["filterExpression X_eq"]),

    08          ("#Pre"  , ["X_eq is_continuous"]),

    19          ("#Find" , ["stepResponse n_eq"]),

    10          ("#Post" , [" TODO "])],

    11        append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], 

    12        NONE, 

    13        [["SignalProcessing","Z_Transform","Inverse"]]));

 \end{verbatim}}

 Although the above details are partly very technical, we explain them

 in order to document some intricacies of TP-based programming in the

 present state of the {\sisac} prototype:

 \begin{description}

 \item[01..02]\textit{store\_specification:} stores the result of the

 function \textit{prep\_specification} in a global reference

 \textit{Unsynchronized.ref}, which causes principal conflicts with

 Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and

 parallel execution~\cite{Makarius-09:parall-proof} and is under

 reconstruction already.

 \textit{prep\_pbt:} translates the specification to an internal format

 which allows efficient processing; see for instance line {\rm 07}

 below.

 \item[03..04] are the ``mathematics author'' holding the copy-rights

 and a unique identifier for the specification within {\sisac},

 complare line {\rm 06}.

 \item[05] is the Isabelle \textit{theory} required to parse the

 specification in lines {\rm 07..10}.

 \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~\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

 equation solver) which is not the case here.

 \item[13] is the specific key into the tree of programs addressing a

 method which is able to find a solution which satiesfies the

 post-condition of the specification.

 \end{description}

 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"

 %WN ...

 %  type pbt = 

 %     {guh  : guh,         (*unique within this isac-knowledge*)

 %      mathauthors: string list, (*copyright*)

 %      init  : pblID,      (*to start refinement with*)

 %      thy   : theory,     (* which allows to compile that pbt

 %			  TODO: search generalized for subthy (ref.p.69*)

 %      (*^^^ WN050912 NOT used during application of the problem,

 %       because applied terms may be from 'subthy' as well as from super;

 %       thus we take 'maxthy'; see match_ags !*)

 %      cas   : term option,(*'CAS-command'*)

 %      prls  : rls,        (* for preds in where_*)

 %      where_: term list,  (* where - predicates*)

 %      ppc   : pat list,

 %      (*this is the model-pattern; 

 %       it contains "#Given","#Where","#Find","#Relate"-patterns

 %       for constraints on identifiers see "fun cpy_nam"*)

 %      met   : metID list}; (* methods solving the pbt*)

 %

 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen

 %WN oben selbst geschrieben.

 %WN das w"urde ich in \sec\label{progr} verschieben und

 %WN das SubProblem partial fractions zum Erkl"aren verwenden.

 % Such a specification is checked before the execution of a program is

 % started, the same applies for sub-programs. In the following example

 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:

 % 

 % \vbox{

 %   \begin{example}

 %   \label{eg:subprob}

 %   \hfill \\

 %   {\ttfamily \begin{tabbing}

 %   ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\

 %   ``\>\>[linear,univariate,equation,test],'' \\

 %   ``\>\>[Test,solve\_linear])'' \\

 %   ``\>[BOOL equ, REAL z])'' \\

 %   \end{tabbing}

 %   }

 %   {\small\textit{

 %     \noindent If a program requires a result which has to be

 % calculated first we can use a subproblem to do so. In our specific

 % case we wanted to calculate the zeros of a fraction and used a

 % subproblem to calculate the zeros of the denominator polynom.

 %     }}

 %   \end{example}

 % }

 \subsection{Implementation of the Method}\label{meth}

 \paragraph{todo}

 \begin{example}

 \begin{verbatim}

 01 store_met

 02  (prep_met thy "met_SP_Ztrans_inv" [] e_metID

 03  (["SignalProcessing", "Z_Transform", "Inverse"], 

 04   [("#Given" ,["filterExpression (X_eq::bool)"]),

 05    ("#Find"  ,["stepResponse (n_eq::bool)"])],

 06   {rew_ord'="tless_true",

 07    rls'= e_rls, 

 08    calc = [],

 09    srls = e_rls,

 10    prls = e_rls,

 11    crls = e_rls,

 12    errpats = [],

 13    nrls = e_rls},

 14   "empty_script"

 15  ));

 \end{verbatim}

 \end{example}