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