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

\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 

Exp.\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{Sub-terms are presented as strings\label{sub-term-str}}} the same way 

as whole terms. The location within the whole term is indicated by ?TODO?

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

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

depth of the tree. For instance $<$TODO 1$>$ displays the term 

$\frac{\frac{1}{x}}{\frac{2}{y}}$ 

\begin{tabbing}

with argument \=$/$ \=1 / x 1234567890\=$/$ \=$/$ \=\=\kill

with argument \>$1$ \>                \>$2$       \\

              \>$/$ \>                \>$/$       \\

              \>    \> 1 / x          \>\>$/$     \\

              \>    \> 2 / y          \>\>\> 1    \\

              \>    \>                \>\>\> x    \\

              \>    \>                \>\>$/$     \\

              \>    \>                \>\>\> 2    \\

              \>    \>                \>\>\> y

\end{tabbing}

TODO?: ``Dann eine Taste definieren, durch deren Dr\"ucken das Innere des 

ersten Klammerpaares - Z\"ahler - genauer angezeigt wird, sobald sich der 

Cursor auf einer der begrenzenden Klammern befindet.

Umgekehrt: Stehe ich irgendwo im Z\"ahler eines Bruches, dann soll es eine 

Taste geben, mit der sich der Z\"ahler zu einem geschweiften Klammerpaar 

verdichtet, vielleicht sogar eine Taste, mit der der Nenner das gleichzeitig 

auch tut.''

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