%:wrap=soft:maxLineLen=78:

 %remove after isabelle build started working -----------------

 \documentclass{article}

 \usepackage{../../isabelle,../../isabellesym}

 \usepackage{graphicx}

 \usepackage{hyperref}  %\url{...}  don't use together with isabelle

 \usepackage{breakurl}  %\url{...}  don't use together with isabelle

 \usepackage{paralist}  % compactitem

 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

 \def\see{$\rightarrow$}

 \newtheorem{UR}{UR}[section]

 \newtheorem{Expl}{Expl}[section]

 \begin{document}

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

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

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

 \bibliographystyle{plain}

 \bibliography{root}

 \end{document}