walther@60184: %:wrap=soft:maxLineLen=78:
walther@60184: 
walther@60184: \section{List of terms used in the \isac-project}\label{terms}
walther@60184: %============================================================================
walther@60184: This list follows the original one in \cite[Appendix D]{isac:all}. It is a 
walther@60184: selection concerning the specify-phase. In particular, the terms used for this 
walther@60184: phase underwent a considerable development since 2002 and are updated to the 
walther@60184: current, more convenient notions.
walther@60184: 
walther@60184: \begin{description}
walther@60184: \item{\bf Calculation} is the document for interactive construction of a 
walther@60184: result from given items according to some \see Problem definition. It is a 
walther@60184: variant of ``structured derivations''~\cite{Back-SD09}.
walther@60184: 
walther@60184: \item{\bf Descriptor} is the heading constant of a \see Model-Item in the 
walther@60184: fields "Given", "Find" and "Relate" (and not in pre-conditions). It indicates 
walther@60184: the kind of item and constrains the respective type.
walther@60184: 
walther@60184: \item{\bf Example} specifies a particular \see Calculation. It comprises text 
walther@60184: and/or figure for the student and a \see Formalisation.
walther@60184: 
walther@60184: \item{\bf Formalisation} is the formal part of an \see Example and contains 
walther@60184: data to complete a \see Specification as a prerequisite for automated 
walther@60184: generation of user-guidance in a \see Calculation.
walther@60184: 
walther@60184: \item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:
walther@60184:   \begin{compactitem}
walther@60184:   \item {\bf RTheory}, an Isabelle theory
walther@60184:   \item {\bf RProblem} is a \see Model-Pattern.
walther@60184:   \item {\bf RMethod}: a program guarded by a \see Model serving 
walther@60184:     ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.
walther@60184:   \end{compactitem}
walther@60184:   For simplicity reasons, a collection of \see Examples is subsumed to  
walther@60184:     \sisac-Knowledge, too.
walther@60184: 
walther@60184: \item{\bf Method} is a program for a class of Problems. It consists of a   
walther@60184: program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard   
walther@60184: with the structure of a \see Model.
walther@60184: 
walther@60184: \item{\bf Model} comprises four fields of \see Model-Items in the line  
walther@60184: of~\cite{gries}:
walther@60184:   \begin{compactitem}
walther@60184:   \item {\bf Given} for the input-items
walther@60184:   \item {\bf Where} for the pre-conditions constraining the input-items
walther@60184:   \item {\bf Find} for the output-items
walther@60184:   \item {\bf Relate} for a part of the post-condition capturing the essence of 
walther@60184:     a problem relating input and output
walther@60184:   \end{compactitem}
walther@60184: 
walther@60184: \item{\bf Model-Item} is a mathematical term in a \see Model.
walther@60184: 
walther@60184: \item{\bf Model-Pattern} comprises the same fields as a \see Model, but these 
walther@60184: contain variables to be instanted by the \see Formalisation of an \see Example 
walther@60184: in order to give \see Model.
walther@60184: 
walther@60184: \item{\bf Problem} is the head of a \see Calculation. Calculations can 
walther@60184: comprise several sub-problems, arbitrarily nested, with exactly the same 
walther@60184: structure. A Problem consists of a \see Specification and a \see Solution.
walther@60184: 
walther@60184: \item{\bf References} refer to three kinds of items in the \see 
walther@60184: \sisac-Knowledge.
walther@60184: 
walther@60184: \item{\bf Solution} are the steps form a \see Specification to a \see 
walther@60184: Solution, where each step is justified by a \see Tactic. The final step 
walther@60184: fulfills the post-condition of the \see Model.
walther@60184: 
walther@60184: \item{\bf Specification} comprises data to specify a problem in the \see Model 
walther@60184: and gives \see References into the \see \sisac-Knowledge.
walther@60184: 
walther@60184: \item{\bf Tactic} transforms a term into another, frequently a rewrite-rule. 
walther@60184: Since a \see Problem can occur recusively in a Solution as a sub-problem, this 
walther@60184: is also a particular Tactic.
walther@60184: 
walther@60184: \item{\bf User-Guide} supports a student during interactive \see Calculations. 
walther@60184: This support is only possible if a \see Formalisation has been transferred 
walther@60184: (invisibly for a student) from an \see Example.
walther@60184: 
walther@60184: %\item{\bf TODO} xxx
walther@60184: \end{description}
walther@60184: 
walther@60184: 
walther@60184: \section{User Requirements}
walther@60184: %============================================================================
walther@60184: The User Requirements ({\bf UR}s) do not follow the lines of the original ones 
walther@60184: in \cite[Part I]{isac:all}, but limit themselves to a student in the 
walther@60184: specify-phase and use the updated terms from \S\ref{terms} (which are 
walther@60184: indicated by initial capital letters).
walther@60184: 
walther@60184: {\bf\UR{Examples are selected from 
walther@60184: collections\label{example-coll}}}\footnote{The present test setup bypasses 
walther@60184: this UR.}
walther@60184: implemented on web-pages, which look like a text book. A specific link at an 
walther@60184: Example starts an interactive Calculation for that Example. See 
walther@60184: \url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.
walther@60184: 
walther@60184: {\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in 
walther@60184: case of standard problems from Computer Algebra with a respective command like 
walther@60184: ${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is 
walther@60184: Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same 
walther@60184: structure.
walther@60184: 
walther@60184: {\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and 
walther@60184: sub-Problems as well, when allowed by the User-Guide. See 
walther@60184: Exp.\ref{tab:calc-coll}.
walther@60184: 
walther@60184: {\bf\UR{Switching between survey and detail\label{yyy}}} is supported by 
walther@60184: collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots 
walther@60184: Expl.\ref{tab:model-sub}
walther@60184: 
walther@60184: {\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means 
walther@60184: without a preceding Example. In this case an empty Specification is generated 
walther@60184: by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help 
walther@60184: the student completing the Specification.
walther@60184: 
walther@60184: {\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see 
walther@60184: Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific 
walther@60184: kind of Problem.
walther@60184: 
walther@60184: {\bf\UR{Feedback during input to the Model\label{yyy}}} is given as
walther@60184: \begin{compactitem}
walther@60184: \item ``correct''
walther@60184: \item ``syntax-error'' or type error
walther@60184: \item ``superfluous''
walther@60184: \item ``incomplete'' in case of lists, sets, etc.
walther@60184: \item ``missing''
walther@60184: \item ``true'' or ``false'' for predicates in the field Where.
walther@60184: \end{compactitem}
walther@60184: 
walther@60184: {\bf\UR{Feedback during input to References\label{yyy}}} is given in the 
walther@60184: Model:
walther@60184: \begin{compactitem}
walther@60184: \item Update RTheory: might cause ``syntax-error''
walther@60184: \item Update RProblem: might cause ``superfluous'' or ``missing''
walther@60184: \item Update RMethod: in this case the Model shows the guard with 
walther@60184: ``superfluous'' or ``missing'' and the keyword Model is annotated with 
walther@60184: ``(RMethod)''.
walther@60184: \end{compactitem}
walther@60184: 
walther@60184: {\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}} 
walther@60184: where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.
walther@60184: 
walther@60184: %{\bf\UR{xxx.\label{yyy}}}
walther@60184: 
walther@60184: 
walther@60184: \section{Example Calculations}
walther@60184: %============================================================================
walther@60184: Calculations at different stages of interactive steps towards a Solution and 
walther@60184: with variants of collapsing and expanding.\\
walther@60184: 
walther@60184: {\bf\Expl{Complete Calculation expanded (sub-Problems 
walther@60184: collapsed).\label{tab:calc-exp}}}
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$              \\
walther@60184: Problem ("Biegelinie", \dots)     \\
walther@60184: .\>Specification:                 \\
walther@60184: .\>.\>Model:                      \\
walther@60184: .\>.\>.\>Given: "Traeger L",      \\
walther@60184: .\>.\>.\>Where: "q\_0 ist\dots    \\
walther@60184: .\>.\>.\>Find: "Biegelinie y"     \\
walther@60184: .\>.\>.\>Relate: "Rand\dots       \\
walther@60184: .\>.\>References:                 \\
walther@60184: .\>.\>.\>RTheory: "Bie\dots"      \\
walther@60184: .\>.\>.\>RProblem: ["\dots]       \\
walther@60184: .\>.\>.\>RMethod: ["Int\dots]     \\
walther@60184: .\>Solution:                      \\
walther@60184: .\>.\>Problem ("\dots")           \\
walther@60184: .\>.\>"[Q x = c + -1 * \dots"     \\
walther@60184: .\>\vdots                         \\
walther@60184: .\>."y x = $-6 * q\_0 * *$\dots"  \\
walther@60184: "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$              \\
walther@60184: Problem ("Biegelinie", \dots)     \\
walther@60184: "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: \newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
walther@60184: {\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the 
walther@60184: inital state with Descriptors, if given by the Example:
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$                        \\
walther@60184: Problem ("Biegelinie", \dots)               \\
walther@60184: .\>Specification:                           \\
walther@60184: .\>.\>Model:                                \\
walther@60184: .\>.\>.\>Given: "Traeger ", "Streckenlast " \\
walther@60184: .\>.\>.\>Where:                             \\
walther@60184: .\>.\>.\>Find: "Biegelinie "                \\
walther@60184: .\>.\>.\>Relate: "Randbedingungen [ ]"      \\
walther@60184: .\>.\>References:                           \\
walther@60184: .\>Solution:
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the 
walther@60184: system presents an empty Specification:
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Problem ("", [])            \\
walther@60184: .\>Specification:           \\
walther@60184: .\>.\>Model:                \\
walther@60184: .\>.\>.\>Given: "", ""      \\
walther@60184: .\>.\>.\>Where: "", ""      \\
walther@60184: .\>.\>.\>Find:  ""          \\
walther@60184: .\>.\>.\>Relate: "", ""     \\
walther@60184: .\>.\>References:           \\
walther@60184: .\>.\>.\>RTheory: ""        \\
walther@60184: .\>.\>.\>RProblem: ["", ""] \\
walther@60184: .\>.\>.\>RMethod: ["", ""]  \\
walther@60184: .\>Solution:
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here 
walther@60184: shown for RTheory and for RProblem; such editing is usually done after some 
walther@60184: input to the Model:
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$                        \\
walther@60184: Problem ("Biegelinie", \dots)               \\
walther@60184: .\>Specification:                           \\
walther@60184: .\>.\>Model:                                \\
walther@60184: .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$"                 \\
walther@60184: .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
walther@60184: .\>.\>.\>Find: "Biegelinie y"               \\
walther@60184: .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 
walther@60184:                     y_0 = 0 ]$"             \\
walther@60184: .\>.\>References:                           \\
walther@60184: .\>.\>.\>RTheory: {\bf"Biegelinie"}         \\
walther@60184: .\>.\>.\>RProblem: ["Biegelinien"]          \\
walther@60184: .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\
walther@60184: .\>Solution:
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The 
walther@60184: additional Given item "FunktionsVariable $x$" is usually provided behind the 
walther@60184: scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can 
walther@60184: be edited as well.
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$                        \\
walther@60184: Problem ("Biegelinie", \dots)               \\
walther@60184: .\>Specification:                           \\
walther@60184: .\>.\>Model (RMethod):                      \\
walther@60184: .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable 
walther@60184:                    $x$" \\
walther@60184: .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
walther@60184: .\>.\>.\>Find: "Biegelinie y"               \\
walther@60184: .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 
walther@60184:                     y_0 = 0 ]$"             \\
walther@60184: .\>.\>References:                           \\
walther@60184: .\>.\>.\>RTheory: {\bf"Biegelinie"}         \\
walther@60184: .\>.\>.\>RProblem: ["Biegelinien"]          \\
walther@60184: .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\
walther@60184: .\>Solution:
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=12\=\kill
walther@60184: Example $<$7.70 a$>$             \\
walther@60184: Problem ("Biegelinie", \dots)    \\
walther@60184: .\>Specification:                \\
walther@60184: .\>Solution:                     \\
walther@60184: .\>.\>Problem ("\dots")          \\
walther@60184: .\>.\>.\>Specification:          \\
walther@60184: .\>.\>.\>.\>Model:               \\
walther@60184: .\>.\>.\>.\>.\>Given: "\dots"    \\
walther@60184: .\>.\>.\>.\>.\>Where: "\dots"    \\
walther@60184: .\>.\>.\>.\>.\>Find: "\dots"     \\
walther@60184: .\>.\>.\>.\>.\>Relate: "\dots    \\
walther@60184: .\>.\>.\>.\>References:          \\
walther@60184: .\>.\>.\>Solution:               \\
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: {\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}
walther@60184: {\tiny \begin{tabbing}
walther@60184: 12\=12\=12\=12\=\kill
walther@60184: Example $<$123 d$>$             \\
walther@60184: ${\it solve} (x + 1 = 2, \,x)$  \\
walther@60184: .\>Specification:               \\
walther@60184: .\>Solution:                    \\
walther@60184: .\>.\>"$x + 1 = 2$"             \\
walther@60184: .\>.\>"$x = 2 - 1$"             \\
walther@60184: .\>.\>"$x = 1$"                 \\
walther@60184: "$x = 1$"
walther@60184: \end{tabbing}}
walther@60184: 
walther@60184: %\subsection{TODO}
walther@60184: %\subsubsection{TODO}