1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex Tue Apr 06 15:52:27 2021 +0200
1.3 @@ -0,0 +1,316 @@
1.4 +%:wrap=soft:maxLineLen=78:
1.5 +%remove after isabelle build started working -----------------
1.6 +\documentclass{article}
1.7 +\usepackage{../../isabelle,../../isabellesym}
1.8 +\usepackage{graphicx}
1.9 +
1.10 +\usepackage{hyperref} %\url{...} don't use together with isabelle
1.11 +\usepackage{breakurl} %\url{...} don't use together with isabelle
1.12 +\usepackage{paralist} % compactitem
1.13 +
1.14 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.15 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.16 +\def\see{$\rightarrow$}
1.17 +\newtheorem{UR}{UR}[section]
1.18 +\newtheorem{Expl}{Expl}[section]
1.19 +
1.20 +\begin{document}
1.21 +
1.22 +\section{List of terms used in the \isac-project}\label{terms}
1.23 +%============================================================================
1.24 +This list follows the original one in \cite[Appendix D]{isac:all}. It is a
1.25 +selection concerning the specify-phase. In particular, the terms used for this
1.26 +phase underwent a considerable development since 2002 and are updated to the
1.27 +current, more convenient notions.
1.28 +
1.29 +\begin{description}
1.30 +\item{\bf Calculation} is the document for interactive construction of a
1.31 +result from given items according to some \see Problem definition. It is a
1.32 +variant of ``structured derivations''~\cite{Back-SD09}.
1.33 +
1.34 +\item{\bf Descriptor} is the heading constant of a \see Model-Item in the
1.35 +fields "Given", "Find" and "Relate" (and not in pre-conditions). It indicates
1.36 +the kind of item and constrains the respective type.
1.37 +
1.38 +\item{\bf Example} specifies a particular \see Calculation. It comprises text
1.39 +and/or figure for the student and a \see Formalisation.
1.40 +
1.41 +\item{\bf Formalisation} is the formal part of an \see Example and contains
1.42 +data to complete a \see Specification as a prerequisite for automated
1.43 +generation of user-guidance in a \see Calculation.
1.44 +
1.45 +\item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:
1.46 + \begin{compactitem}
1.47 + \item {\bf RTheory}, an Isabelle theory
1.48 + \item {\bf RProblem} is a \see Model-Pattern.
1.49 + \item {\bf RMethod}: a program guarded by a \see Model serving
1.50 + ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.
1.51 + \end{compactitem}
1.52 + For simplicity reasons, a collection of \see Examples is subsumed to
1.53 + \sisac-Knowledge, too.
1.54 +
1.55 +\item{\bf Method} is a program for a class of Problems. It consists of a
1.56 +program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard
1.57 +with the structure of a \see Model.
1.58 +
1.59 +\item{\bf Model} comprises four fields of \see Model-Items in the line
1.60 +of~\cite{gries}:
1.61 + \begin{compactitem}
1.62 + \item {\bf Given} for the input-items
1.63 + \item {\bf Where} for the pre-conditions constraining the input-items
1.64 + \item {\bf Find} for the output-items
1.65 + \item {\bf Relate} for a part of the post-condition capturing the essence of
1.66 + a problem relating input and output
1.67 + \end{compactitem}
1.68 +
1.69 +\item{\bf Model-Item} is a mathematical term in a \see Model.
1.70 +
1.71 +\item{\bf Model-Pattern} comprises the same fields as a \see Model, but these
1.72 +contain variables to be instanted by the \see Formalisation of an \see Example
1.73 +in order to give \see Model.
1.74 +
1.75 +\item{\bf Problem} is the head of a \see Calculation. Calculations can
1.76 +comprise several sub-problems, arbitrarily nested, with exactly the same
1.77 +structure. A Problem consists of a \see Specification and a \see Solution.
1.78 +
1.79 +\item{\bf References} refer to three kinds of items in the \see
1.80 +\sisac-Knowledge.
1.81 +
1.82 +\item{\bf Solution} are the steps form a \see Specification to a \see
1.83 +Solution, where each step is justified by a \see Tactic. The final step
1.84 +fulfills the post-condition of the \see Model.
1.85 +
1.86 +\item{\bf Specification} comprises data to specify a problem in the \see Model
1.87 +and gives \see References into the \see \sisac-Knowledge.
1.88 +
1.89 +\item{\bf Tactic} transforms a term into another, frequently a rewrite-rule.
1.90 +Since a \see Problem can occur recusively in a Solution as a sub-problem, this
1.91 +is also a particular Tactic.
1.92 +
1.93 +\item{\bf User-Guide} supports a student during interactive \see Calculations.
1.94 +This support is only possible if a \see Formalisation has been transferred
1.95 +(invisibly for a student) from an \see Example.
1.96 +
1.97 +%\item{\bf TODO} xxx
1.98 +\end{description}
1.99 +
1.100 +
1.101 +\section{User Requirements}
1.102 +%============================================================================
1.103 +The User Requirements ({\bf UR}s) do not follow the lines of the original ones
1.104 +in \cite[Part I]{isac:all}, but limit themselves to a student in the
1.105 +specify-phase and use the updated terms from \S\ref{terms} (which are
1.106 +indicated by initial capital letters).
1.107 +
1.108 +{\bf\UR{Examples are selected from
1.109 +collections\label{example-coll}}}\footnote{The present test setup bypasses
1.110 +this UR.}
1.111 +implemented on web-pages, which look like a text book. A specific link at an
1.112 +Example starts an interactive Calculation for that Example. See
1.113 +\url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.
1.114 +
1.115 +{\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in
1.116 +case of standard problems from Computer Algebra with a respective command like
1.117 +${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is
1.118 +Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same
1.119 +structure.
1.120 +
1.121 +{\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and
1.122 +sub-Problems as well, when allowed by the User-Guide. See
1.123 +Exp.\ref{tab:calc-coll}.
1.124 +
1.125 +{\bf\UR{Switching between survey and detail\label{yyy}}} is supported by
1.126 +collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots
1.127 +Expl.\ref{tab:model-sub}
1.128 +
1.129 +{\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means
1.130 +without a preceding Example. In this case an empty Specification is generated
1.131 +by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help
1.132 +the student completing the Specification.
1.133 +
1.134 +{\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see
1.135 +Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific
1.136 +kind of Problem.
1.137 +
1.138 +{\bf\UR{Feedback during input to the Model\label{yyy}}} is given as
1.139 +\begin{compactitem}
1.140 +\item ``correct''
1.141 +\item ``syntax-error'' or type error
1.142 +\item ``superfluous''
1.143 +\item ``incomplete'' in case of lists, sets, etc.
1.144 +\item ``missing''
1.145 +\item ``true'' or ``false'' for predicates in the field Where.
1.146 +\end{compactitem}
1.147 +
1.148 +{\bf\UR{Feedback during input to References\label{yyy}}} is given in the
1.149 +Model:
1.150 +\begin{compactitem}
1.151 +\item Update RTheory: might cause ``syntax-error''
1.152 +\item Update RProblem: might cause ``superfluous'' or ``missing''
1.153 +\item Update RMethod: in this case the Model shows the guard with
1.154 +``superfluous'' or ``missing'' and the keyword Model is annotated with
1.155 +``(RMethod)''.
1.156 +\end{compactitem}
1.157 +
1.158 +{\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}}
1.159 +where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.
1.160 +
1.161 +%{\bf\UR{xxx.\label{yyy}}}
1.162 +
1.163 +
1.164 +\section{Example Calculations}
1.165 +%============================================================================
1.166 +Calculations at different stages of interactive steps towards a Solution and
1.167 +with variants of collapsing and expanding.\\
1.168 +
1.169 +{\bf\Expl{Complete Calculation expanded (sub-Problems
1.170 +collapsed).\label{tab:calc-exp}}}
1.171 +{\tiny \begin{tabbing}
1.172 +12\=12\=12\=12\=\kill
1.173 +Example $<$7.70 a$>$ \\
1.174 +Problem ("Biegelinie", \dots) \\
1.175 +.\>Specification: \\
1.176 +.\>.\>Model: \\
1.177 +.\>.\>.\>Given: "Traeger L", \\
1.178 +.\>.\>.\>Where: "q\_0 ist\dots \\
1.179 +.\>.\>.\>Find: "Biegelinie y" \\
1.180 +.\>.\>.\>Relate: "Rand\dots \\
1.181 +.\>.\>References: \\
1.182 +.\>.\>.\>RTheory: "Bie\dots" \\
1.183 +.\>.\>.\>RProblem: ["\dots] \\
1.184 +.\>.\>.\>RMethod: ["Int\dots] \\
1.185 +.\>Solution: \\
1.186 +.\>.\>Problem ("\dots") \\
1.187 +.\>.\>"[Q x = c + -1 * \dots" \\
1.188 +.\>\vdots \\
1.189 +.\>."y x = $-6 * q\_0 * *$\dots" \\
1.190 +"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
1.191 +\end{tabbing}}
1.192 +
1.193 +{\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}
1.194 +{\tiny \begin{tabbing}
1.195 +12\=12\=12\=12\=\kill
1.196 +Example $<$7.70 a$>$ \\
1.197 +Problem ("Biegelinie", \dots) \\
1.198 +"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
1.199 +\end{tabbing}}
1.200 +
1.201 +\newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.202 +{\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the
1.203 +inital state with Descriptors, if given by the Example:
1.204 +{\tiny \begin{tabbing}
1.205 +12\=12\=12\=12\=\kill
1.206 +Example $<$7.70 a$>$ \\
1.207 +Problem ("Biegelinie", \dots) \\
1.208 +.\>Specification: \\
1.209 +.\>.\>Model: \\
1.210 +.\>.\>.\>Given: "Traeger ", "Streckenlast " \\
1.211 +.\>.\>.\>Where: \\
1.212 +.\>.\>.\>Find: "Biegelinie " \\
1.213 +.\>.\>.\>Relate: "Randbedingungen [ ]" \\
1.214 +.\>.\>References: \\
1.215 +.\>Solution:
1.216 +\end{tabbing}}
1.217 +
1.218 +{\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the
1.219 +system presents an empty Specification:
1.220 +{\tiny \begin{tabbing}
1.221 +12\=12\=12\=12\=\kill
1.222 +Problem ("", []) \\
1.223 +.\>Specification: \\
1.224 +.\>.\>Model: \\
1.225 +.\>.\>.\>Given: "", "" \\
1.226 +.\>.\>.\>Where: "", "" \\
1.227 +.\>.\>.\>Find: "" \\
1.228 +.\>.\>.\>Relate: "", "" \\
1.229 +.\>.\>References: \\
1.230 +.\>.\>.\>RTheory: "" \\
1.231 +.\>.\>.\>RProblem: ["", ""] \\
1.232 +.\>.\>.\>RMethod: ["", ""] \\
1.233 +.\>Solution:
1.234 +\end{tabbing}}
1.235 +
1.236 +{\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here
1.237 +shown for RTheory and for RProblem; such editing is usually done after some
1.238 +input to the Model:
1.239 +{\tiny \begin{tabbing}
1.240 +12\=12\=12\=12\=\kill
1.241 +Example $<$7.70 a$>$ \\
1.242 +Problem ("Biegelinie", \dots) \\
1.243 +.\>Specification: \\
1.244 +.\>.\>Model: \\
1.245 +.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$" \\
1.246 +.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
1.247 +.\>.\>.\>Find: "Biegelinie y" \\
1.248 +.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
1.249 + y_0 = 0 ]$" \\
1.250 +.\>.\>References: \\
1.251 +.\>.\>.\>RTheory: {\bf"Biegelinie"} \\
1.252 +.\>.\>.\>RProblem: ["Biegelinien"] \\
1.253 +.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
1.254 +.\>Solution:
1.255 +\end{tabbing}}
1.256 +
1.257 +{\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The
1.258 +additional Given item "FunktionsVariable $x$" is usually provided behind the
1.259 +scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can
1.260 +be edited as well.
1.261 +{\tiny \begin{tabbing}
1.262 +12\=12\=12\=12\=\kill
1.263 +Example $<$7.70 a$>$ \\
1.264 +Problem ("Biegelinie", \dots) \\
1.265 +.\>Specification: \\
1.266 +.\>.\>Model (RMethod): \\
1.267 +.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable
1.268 + $x$" \\
1.269 +.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
1.270 +.\>.\>.\>Find: "Biegelinie y" \\
1.271 +.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
1.272 + y_0 = 0 ]$" \\
1.273 +.\>.\>References: \\
1.274 +.\>.\>.\>RTheory: {\bf"Biegelinie"} \\
1.275 +.\>.\>.\>RProblem: ["Biegelinien"] \\
1.276 +.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
1.277 +.\>Solution:
1.278 +\end{tabbing}}
1.279 +
1.280 +{\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}
1.281 +{\tiny \begin{tabbing}
1.282 +12\=12\=12\=12\=12\=\kill
1.283 +Example $<$7.70 a$>$ \\
1.284 +Problem ("Biegelinie", \dots) \\
1.285 +.\>Specification: \\
1.286 +.\>Solution: \\
1.287 +.\>.\>Problem ("\dots") \\
1.288 +.\>.\>.\>Specification: \\
1.289 +.\>.\>.\>.\>Model: \\
1.290 +.\>.\>.\>.\>.\>Given: "\dots" \\
1.291 +.\>.\>.\>.\>.\>Where: "\dots" \\
1.292 +.\>.\>.\>.\>.\>Find: "\dots" \\
1.293 +.\>.\>.\>.\>.\>Relate: "\dots \\
1.294 +.\>.\>.\>.\>References: \\
1.295 +.\>.\>.\>Solution: \\
1.296 +\end{tabbing}}
1.297 +
1.298 +{\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}
1.299 +{\tiny \begin{tabbing}
1.300 +12\=12\=12\=12\=\kill
1.301 +Example $<$123 d$>$ \\
1.302 +${\it solve} (x + 1 = 2, \,x)$ \\
1.303 +.\>Specification: \\
1.304 +.\>Solution: \\
1.305 +.\>.\>"$x + 1 = 2$" \\
1.306 +.\>.\>"$x = 2 - 1$" \\
1.307 +.\>.\>"$x = 1$" \\
1.308 +"$x = 1$"
1.309 +\end{tabbing}}
1.310 +
1.311 +
1.312 +
1.313 +%\subsection{TODO}
1.314 +%\subsubsection{TODO}
1.315 +
1.316 +\bibliographystyle{plain}
1.317 +\bibliography{root}
1.318 +
1.319 +\end{document}