%:wrap=soft:maxLineLen=78:

 \chapter{Preliminaries}

 %############################################################################

 \section{List of terms used in the \isac-project}\label{terms}

 %============================================================================

 This list follows the original one in \cite[Appendix D]{isac:all}. It is a 

 selection concerning the specify-phase. In particular, the terms used for this 

 phase underwent a considerable development since 2002 and are updated to the 

 current, more convenient notions.

 \begin{description}

 \item{\bf Calculation} is the document for interactive construction of a 

 result from given items according to some \see Problem definition. It is a 

 variant of ``structured derivations''~\cite{Back-SD09}.

 \item{\bf Descriptor} is the heading constant of a \see Model-Item in the 

 fields "Given", "Find" and "Relate" (and not in where_-conditions). It indicates 

 the kind of item and constrains the respective type.

 \item{\bf Example} specifies a particular \see Calculation. It comprises text 

 and/or figure for the student and a \see Formalisation.

 \item{\bf Formalisation} is the formal part of an \see Example and contains 

 data to complete a \see Specification as a prerequisite for automated 

 generation of user-guidance in a \see Calculation.

 \item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:

   \begin{compactitem}

   \item {\bf RTheory}, an Isabelle theory

   \item {\bf RProblem} is a \see Model-Pattern.

   \item {\bf RMethod}: a program guarded by a \see Model serving 

     ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.

   \end{compactitem}

   For simplicity reasons, a collection of \see Examples is subsumed to  

     \sisac-Knowledge, too.

 \item{\bf Method} is a program for a class of Problems. It consists of a   

 program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard   

 with the structure of a \see Model.

 \item{\bf Model} comprises four fields of \see Model-Items in the line  

 of~\cite{gries}:

   \begin{compactitem}

   \item {\bf Given} for the input-items

   \item {\bf Where} for the where_-conditions constraining the input-items

   \item {\bf Find} for the output-items

   \item {\bf Relate} for a part of the post-condition capturing the essence of 

     a problem relating input and output

   \end{compactitem}

 \item{\bf Model-Item} is a mathematical term in a \see Model.

 \item{\bf Model-Pattern} comprises the same fields as a \see Model, but these 

 contain variables to be instanted by the \see Formalisation of an \see Example 

 in order to give \see Model.

 \item{\bf Problem} is the head of a \see Calculation. Calculations can 

 comprise several sub-problems, arbitrarily nested, with exactly the same 

 structure. A Problem consists of a \see Specification and a \see Solution.

 \item{\bf References} refer to three kinds of items in the \see 

 \sisac-Knowledge.

 \item{\bf Solution} are the steps form a \see Specification to a \see 

 Solution, where each step is justified by a \see Tactic. The final step 

 fulfills the post-condition of the \see Model.

 \item{\bf Specification} comprises data to specify a problem in the \see Model 

 and gives \see References into the \see \sisac-Knowledge.

 \item{\bf Tactic} transforms a term into another, frequently a rewrite-rule. 

 Since a \see Problem can occur recusively in a Solution as a sub-problem, this 

 is also a particular Tactic.

 \item{\bf User-Guide} supports a student during interactive \see Calculations. 

 This support is only possible if a \see Formalisation has been transferred 

 (invisibly for a student) from an \see Example.

 %\item{\bf TODO} xxx

 \end{description}

 \section{User Requirements}

 %============================================================================

 The User Requirements ({\bf UR}s) do not follow the lines of the original ones 

 in \cite[Part I]{isac:all}, but limit themselves to a student in the 

 specify-phase and use the updated terms from \S\ref{terms} (which are 

 indicated by initial capital letters).

 \subsection{General}

 %----------------------------------------------------------------------------

 {\bf\UR{The screen-reader superimposes the Braille display \label{sreader-braille}}} in the software hierarchy, i.e. the former determines output of the latter.

 {\bf\UR{Special keys can be defined by the user\label{def-spec-keys}}} for the Braille display.

 \subsection{Specify Phase}

 %----------------------------------------------------------------------------

 {\bf\UR{Examples are selected from 

 collections\label{example-coll}}}\footnote{The present test setup bypasses 

 this UR.}

 implemented on web-pages, which look like a text book. A specific link at an 

 Example starts an interactive Calculation for that Example. See 

 \url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.

 {\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in 

 case of standard problems from Computer Algebra with a respective command like 

 ${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is 

 Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same 

 structure.

 {\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and 

 sub-Problems as well, when allowed by the User-Guide. See 

 Expl.\ref{tab:calc-coll}.

 {\bf\UR{Switching between survey and detail\label{yyy}}} is supported by 

 collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots 

 Expl.\ref{tab:model-sub}

 {\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means 

 without a preceding Example. In this case an empty Specification is generated 

 by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help 

 the student completing the Specification.

 {\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see 

 Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific 

 kind of Problem.

 {\bf\UR{Feedback during input to the Model\label{yyy}}} is given as

 \begin{compactitem}

 \item ``correct''

 \item ``syntax-error'' or type error

 \item ``superfluous''

 \item ``incomplete'' in case of lists, sets, etc.

 \item ``missing''

 \item ``true'' or ``false'' for predicates in the field Where.

 \end{compactitem}

 {\bf\UR{Feedback during input to References\label{yyy}}} is given in the 

 Model:

 \begin{compactitem}

 \item Update RTheory: might cause ``syntax-error''

 \item Update RProblem: might cause ``superfluous'' or ``missing''

 \item Update RMethod: in this case the Model shows the guard with 

 ``superfluous'' or ``missing'' and the keyword Model is annotated with 

 ``(RMethod)''.

 \end{compactitem}

 {\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}} 

 where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.

 \subsection{Terms}

 %----------------------------------------------------------------------------

 {\bf\UR{Terms are presented as strings in Braille format\label{term-str}}} for 

 the blind user and as Isabelle strings for other users at the same time --- 

 for the purpose of inclusive learning in front of one and the same screen. 

 ?TODO is this reasonable?

 {\bf\UR{The Braille-format can be changed\label{braille-format}}} to different 

 standards.

 {\bf\UR{Braille-format can be displayed also in the standard frontend\label{braille-format-standard}}}, in particular for authoring purposes.

 {\bf\UR{Semantic information is available for all elements of 

 terms.\label{term-semantic}}} Such information is:

 \begin{compactenum}

 \item the type for constants and variables by a pop-up.

 \item the scope of a variable by (TODO ``internal'' and ``global'' seems to 

 coarse).

 \item the definition of constants and variables by jumping to the respective 

 location, probably in another file.

 \end{compactenum}

 {\bf\UR{On the Braille lines of pop-ups start with a special character\label{indicate-popup}}}, TODO? ``\#''.

 {\bf\UR{Sub-terms are presented as strings\label{sub-term-str}}} the same way 

 as whole terms. ?TODO? show location within the whole term.

 {\bf\UR{A term can be shown as a tree\label{term-tree}}} if requested by a 

 special key, TODO SK1. The key followed by an integer argument determines the 

 depth of the tree. For instance $<$SK1 2$>$ displays the term 

 $\frac{\frac{1}{x+2*y}}{\frac{3}{z}}$ 

 \begin{tabbing}

 123\=\#3.2 \=$/$ \=$/$ \=    \kill

    \>\#    \>$/$     \\

    \>\#1   \>\>$/$     \\

    \>\#1.1 \>\>\> 1    \\

    \>\#1.2 \>\>\> x + 2 * y\\

    \>\#2.  \>\>$/$     \\

    \>\#2.1 \>\>\> 3    \\

    \>\#2.2 \>\>\> z

 \end{tabbing}

 Note that there are operators with different arity, for instance arity one for $\sin$, arity two for $+$ and arity four for $\int^a_b\;f(x)\;dx{}$.

 {\bf\UR{Structure of the tree representation\label{yyy}}} of a term is (?TODO\dots) indicated by integer lists as shown in the example of UR\ref{term-tree}.

 {\bf\UR{Collapsing and expanding of the tree representation \label{term-coll-exp}}} for a term follow the rules established for file browsers.

 {\bf\UR{Special keys lead to the node at the deepest level\label{yyy}}} and ?TODO?

 {\bf\UR{Navigation through sub-terms is hierarchical\label{navi-sub-terms}}} 

 and supported by a special key combined with the arrow keys as follows:

 \begin{compactenum}

 \item $<$STRG$>$ $<\rightarrow>$ next element right on the same level; 

 acoustical indication at the end of the level.

 \item $<$STRG$>$ $<\leftarrow>$ next element left on the same level; 

 acoustical indication at the end of the level.

 \item $<$STRG$>$ $<\uparrow>$ next element on the higher level; acoustical 

 indication at the root.

 \item $<$STRG$>$ $<\downarrow>$ next element on the lower level; acoustical 

 indication at the bottom.

 \end{compactenum}

 %{\bf\UR{xxx.\label{yyy}}}

 \section{Example Calculations}

 %============================================================================

 Calculations at different stages of interactive steps towards a Solution and 

 with variants of collapsing and expanding.\\

 {\bf\Expl{Complete Calculation expanded (sub-Problems 

 collapsed).\label{tab:calc-exp}}}

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$              \\

 Problem ("Biegelinie", \dots)     \\

 .\>Specification:                 \\

 .\>.\>Model:                      \\

 .\>.\>.\>Given: "Traeger L",      \\

 .\>.\>.\>Where: "q\_0 ist\dots    \\

 .\>.\>.\>Find: "Biegelinie y"     \\

 .\>.\>.\>Relate: "Rand\dots       \\

 .\>.\>References:                 \\

 .\>.\>.\>RTheory: "Bie\dots"      \\

 .\>.\>.\>RProblem: ["\dots]       \\

 .\>.\>.\>RMethod: ["Int\dots]     \\

 .\>Solution:                      \\

 .\>.\>Problem ("\dots")           \\

 .\>.\>"[Q x = c + -1 * \dots"     \\

 .\>\vdots                         \\

 .\>."y x = $-6 * q\_0 * *$\dots"  \\

 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\

 \end{tabbing}}

 {\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$              \\

 Problem ("Biegelinie", \dots)     \\

 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\

 \end{tabbing}}

 \newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 {\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the 

 inital state with Descriptors, if given by the Example:

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$                        \\

 Problem ("Biegelinie", \dots)               \\

 .\>Specification:                           \\

 .\>.\>Model:                                \\

 .\>.\>.\>Given: "Traeger ", "Streckenlast " \\

 .\>.\>.\>Where:                             \\

 .\>.\>.\>Find: "Biegelinie "                \\

 .\>.\>.\>Relate: "Randbedingungen [ ]"      \\

 .\>.\>References:                           \\

 .\>Solution:

 \end{tabbing}}

 {\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the 

 system presents an empty Specification:

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Problem ("", [])            \\

 .\>Specification:           \\

 .\>.\>Model:                \\

 .\>.\>.\>Given: "", ""      \\

 .\>.\>.\>Where: "", ""      \\

 .\>.\>.\>Find:  ""          \\

 .\>.\>.\>Relate: "", ""     \\

 .\>.\>References:           \\

 .\>.\>.\>RTheory: ""        \\

 .\>.\>.\>RProblem: ["", ""] \\

 .\>.\>.\>RMethod: ["", ""]  \\

 .\>Solution:

 \end{tabbing}}

 {\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here 

 shown for RTheory and for RProblem; such editing is usually done after some 

 input to the Model:

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$                        \\

 Problem ("Biegelinie", \dots)               \\

 .\>Specification:                           \\

 .\>.\>Model:                                \\

 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$"                 \\

 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\

 .\>.\>.\>Find: "Biegelinie y"               \\

 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 

                     y_0 = 0 ]$"             \\

 .\>.\>References:                           \\

 .\>.\>.\>RTheory: {\bf"Biegelinie"}         \\

 .\>.\>.\>RProblem: ["Biegelinien"]          \\

 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\

 .\>Solution:

 \end{tabbing}}

 {\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The 

 additional Given item "FunktionsVariable $x$" is usually provided behind the 

 scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can 

 be edited as well.

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$                        \\

 Problem ("Biegelinie", \dots)               \\

 .\>Specification:                           \\

 .\>.\>Model (RMethod):                      \\

 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable 

                    $x$" \\

 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\

 .\>.\>.\>Find: "Biegelinie y"               \\

 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x 

                     y_0 = 0 ]$"             \\

 .\>.\>References:                           \\

 .\>.\>.\>RTheory: {\bf"Biegelinie"}         \\

 .\>.\>.\>RProblem: ["Biegelinien"]          \\

 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"]             \\

 .\>Solution:

 \end{tabbing}}

 {\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=12\=\kill

 Example $<$7.70 a$>$             \\

 Problem ("Biegelinie", \dots)    \\

 .\>Specification:                \\

 .\>Solution:                     \\

 .\>.\>Problem ("\dots")          \\

 .\>.\>.\>Specification:          \\

 .\>.\>.\>.\>Model:               \\

 .\>.\>.\>.\>.\>Given: "\dots"    \\

 .\>.\>.\>.\>.\>Where: "\dots"    \\

 .\>.\>.\>.\>.\>Find: "\dots"     \\

 .\>.\>.\>.\>.\>Relate: "\dots    \\

 .\>.\>.\>.\>References:          \\

 .\>.\>.\>Solution:               \\

 \end{tabbing}}

 {\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}

 {\tiny \begin{tabbing}

 12\=12\=12\=12\=\kill

 Example $<$123 d$>$             \\

 ${\it solve} (x + 1 = 2, \,x)$  \\

 .\>Specification:               \\

 .\>Solution:                    \\

 .\>.\>"$x + 1 = 2$"             \\

 .\>.\>"$x = 2 - 1$"             \\

 .\>.\>"$x = 1$"                 \\

 "$x = 1$"

 \end{tabbing}}

 %\subsection{TODO}

 %\subsubsection{TODO}