\section{Development of a Program on Trial}\label{trial} 

 \section{Concepts and Tasks in TP-based Programming}\label{trial}

 As mentioned above, {\sisac} is an experimental system for a proof of

 %\section{Development of a Program on Trial}

 concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}.  The

 latter interprets a specific kind of TP-based programming language,

 This section presents all the concepts involved in TP-based

 which is as experimental as the whole prototype --- so programming in

 programming and all the tasks to be accomplished by programmers. The

 this language can be only ``on trial'', presently.  However, as a

 presentation uses the running example which has been introduced in

 prototype, the language addresses essentials described below.

 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.

 The running example, introduced by Fig.\ref{fig-interactive} on

 The running example requires to determine the inverse $\cal

 p.\pageref{fig-interactive}, requires to determine the inverse $\cal

     ];\end{verbatim}

     ];

   \end{verbatim}

   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}

   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";

   \end{verbatim}

     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}

     rewrite_set_ thy true inverse_Z sample_term;

   \end{verbatim}

 The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for

 \paragraph{Explicit Problems} require explicit methods to solve them, and within

 all kinds of evaluation. Some functionality required in programming,

 this methods we have some explicit steps to do. This steps can be unique for

 however, cannot be accomplished by rewriting. So the prototype has a

 a special problem or refindable in other problems. No mather what case, such

 mechanism to call ML-functions during rewriting, and the programmer has

 steps often require some technical functions behind. For the solving process

 to use this mechanism.

 of the Inverse Z Transformation and the corresponding partial fraction it was

 neccessary to build helping functions like \texttt{get\_denominator},

 In the running example's program on p.\pageref{s:impl} the lines {\rm

 \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us

 05} and {\rm 06} contain such functions; we go into the details with

 to filter the denominator or numerator out of a fraction, last one helps us to

 \textit{argument\_in X\_z;}. This function fetches the argument from a

 get to know the bound variable in a equation.

 function application: Line {\rm 03} in the example calculation on

 \par

 p.\pageref{exp-calc} is created by line {\rm 06} of the example

 By taking \texttt{get\_denominator} as an example, we want to explain how to 

 program on p.\pageref{s:impl} where the program's environment assigns

 implement new functions into the existing system and how we can later use them

 the value \textit{X z} to the variable \textit{X\_z}; so the function

 in our program.

 shall extract the argument \textit{z}.

 \subsubsection{Find a place to Store the Function}

 \medskip In order to be recognised as a function constant in the

 program source the function needs to be declared in a theory, here in

 The whole system builds up on a well defined structure of Knowledge. This

 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in

 Knowledge sets up at the Path:

 the context \textit{ctxt} of that theory:

 \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}

 {\footnotesize

 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:

   get_denominator :: "real => real"

    consts

 \end{verbatim}

      argument'_in     :: "real => real"            ("argument'_in _" 10)

 This command tells the machine that a function with the name

 \texttt{get\_denominator} exists which gets a real expression as argument and

    ML {* val SOME t = parse ctxt "argument_in (X z)"; *}

 returns once again a real expression. Now we are able to implement the function

 itself, upcoming example now shows the implementation of

    val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") 

 \texttt{get\_denominator}.

              $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term

 \end{verbatim}}

 %\begin{example}

   \label{eg:getdenom}

 \noindent Parsing produces a term \texttt{t} in internal

   \begin{verbatim}

 representation, consisting of \texttt{Const ("argument'\_in", type)}

 and the two variables \texttt{Free ("X", type)} and \texttt{Free ("z",

 01  (*

 type)}, \texttt{\$} is the term constructor. The function body below is

 02   *("get_denominator",

 implemented directly in ML, i.e in an \texttt{ML \{* *\}} block; the

 03   *  ("Rational.get_denominator", eval_get_denominator ""))

 function definition provides a unique prefix \texttt{eval\_} to the

 04   *)

 function name:

 05  fun eval_get_denominator (thmid:string) _ 

 06            (t as Const ("Rational.get_denominator", _) $

 {\footnotesize

 07                (Const ("Rings.inverse_class.divide", _) $num 

 08                  $denom)) thy = 

 09          SOME (mk_thmid thmid "" 

 10              (Print_Mode.setmp [] 

 11                (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

 12              Trueprop $ (mk_equality (t, denom)))

 13    | eval_get_denominator _ _ _ _ = NONE;\end{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

 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}

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

    ML {*

 01 val thy = @{theory Isac};

      fun eval_argument_in _ 

 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));

        "Build_Inverse_Z_Transform.argument'_in" 

 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;

        (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =

 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()

          if is_Free arg (*could be something to be simplified before*)

 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}

          then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))

 %\end{example}

          else NONE

      | eval_argument_in _ _ _ _ = NONE;

 \begin{description}

    *}

 \item[01] checks if the proofer set up on our {\sisac{}} System.

 \end{verbatim}}

 \item[02] passes a simple expression (fraction) to our suddenly created

           function.

 \noindent The function body creates either creates \texttt{NONE}

 \item[04] checks if the resulting variable is the correct one (in this case

 telling the rewrite-engine to search for the next redex, or creates an

           ``b'' the denominator) and returns.

 ad-hoc theorem for rewriting, thus the programmer needs to adopt many

 \item[05] handels the error case and reports that the function is not able to

 technicalities of Isabelle, for instance, the \textit{Trueprop}

           solve the given problem.

 constant.

 \end{description}

 \bigskip This sub-task particularly sheds light on basic issues in the

 design of a programming language, the integration of diffent language

 layers, the layer of Isabelle/Isar and Isabelle/ML.

 Another point of improvement for the prototype is the rewrite-engine: The

 program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}

 and {\rm 06} to

 {\small\it\label{s:impl}

 \begin{tabbing}

 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill

 \>{\rm 05/6}\>\>\>  (z::real) = argument\_in (lhs X\_eq) ;

 \end{tabbing}}

 \noindent because nested function calls would require creating redexes

 inside-out; however, the prototype's rewrite-engine only works top down

 from the root of a term down to the leaves.

 How all these ugly technicalities are to be checked in the prototype is 

 shown in \S\ref{flow-prep} below.

 % \paragraph{Explicit Problems} require explicit methods to solve them, and within

 % this methods we have some explicit steps to do. This steps can be unique for

 % 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 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} as an example, we want to explain how to 

 % 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:

 % \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, upcoming example now shows the implementation of

 % \texttt{get\_denominator}.

 % 

 % %\begin{example}

 %   \label{eg:getdenom}

 %   \begin{verbatim}

 % 

 % 01  (*

 % 02   *("get_denominator",

 % 03   *  ("Rational.get_denominator", eval_get_denominator ""))

 % 04   *)

 % 05  fun eval_get_denominator (thmid:string) _ 

 % 06            (t as Const ("Rational.get_denominator", _) $

 % 07                (Const ("Rings.inverse_class.divide", _) $num 

 % 08                  $denom)) thy = 

 % 09          SOME (mk_thmid thmid "" 

 % 10              (Print_Mode.setmp [] 

 % 11                (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

 % 12              Trueprop $ (mk_equality (t, denom)))

 % 13    | eval_get_denominator _ _ _ _ = NONE;\end{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

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

 % 

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

 The previous section presented all the duties and tasks to be accomplished by

 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great

 programmers of TP-based languages. Some tasks are interrelated and comprehensive,

 step forward for interactive theory and proof development. The

 so first experiences with the workflow in programming are noted below. The notes

 {\sisac}-prototype re-uses this IDE as a programming environment.  The

 also capture requirements for future language development.

 experiences from this re-use show, that the essential components are

 available from Isabelle/jEdit. However, additional tools and features

 are required to acchieve acceptable usability.

 So notable experiences are reported here, also as a requirement

 capture for further development of TP-based languages and respective

 IDEs.

 % Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''

 The new graphical user-interface of Isabelle~\cite{makar-jedit-12} is a great

 step forward for interactive theory and proof development --- and so it is for

  --- the re-use

 of

 and so it is for

 \begin{example}

 {\small\it\label{exp-calc}

 \hfill\\

 {\small\it