1.1 --- a/src/Tools/isac/Doc/Specify_Phase/document/root.bib Sun Apr 04 13:31:04 2021 +0200
1.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/root.bib Tue Apr 06 15:52:27 2021 +0200
1.3 @@ -1,8 +1,40 @@
1.4 @TechReport{isac:all,
1.5 author = {\isac{}- Team},
1.6 - title = {\isac{} -- User Requirements Document},
1.7 - institution = {Institute for Softwaretechnology,
1.8 - University of Technology},
1.9 + title = {\isac{} -- User Requirements Document, Software Requirements Document,
1.10 + Architectural Design Document, Software Design Document, Use Cases, Test Cases},
1.11 + institution = {Institute for Softwaretechnology, University of Technology},
1.12 year = {2002},
1.13 - note = {\url{https://static.miraheze.org/isacwiki/TODO/URD.pdf}}
1.14 + note = {\url{https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf}}
1.15 }
1.16 +@TECHREPORT{Back-SD09,
1.17 + author = {Back, Ralph-Johan},
1.18 + title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
1.19 + institution = {TUCS - Turku Centre for Computer Science},
1.20 + year = {2009},
1.21 + type = {TUCS Technical Report},
1.22 + number = {949},
1.23 + address = {Turku, Finland},
1.24 + month = {July}
1.25 +}
1.26 +@Book{gries,
1.27 + author = {Gries, David},
1.28 + title = {The science of programming},
1.29 + publisher = {Springer-Verlag},
1.30 + year = {1981},
1.31 + series = {Texts and monographs in computer science}
1.32 +}
1.33 +@Inproceedings{EPTCS-wn-20,
1.34 + author = {Neuper, Walther},
1.35 + year = {2020},
1.36 + title = {Lucas-Interpretation on Isabelle's Functions},
1.37 + editor = {Quaresma, Pedro and Neuper, Walther and Marcos, Jo\~ao},
1.38 + booktitle = {{\rm Proceedings 9th International Workshop on}
1.39 + Theorem Proving Components for Educational Software,
1.40 + {\rm Paris, France, 29th June 2020}},
1.41 + series = {Electronic Proceedings in Theoretical Computer Science},
1.42 + volume = {328},
1.43 + publisher = {Open Publishing Association},
1.44 + pages = {79-95},
1.45 + doi = {10.4204/EPTCS.328.5},
1.46 + note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?thedu2020.5}}
1.47 +}
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex Tue Apr 06 15:52:27 2021 +0200
2.3 @@ -0,0 +1,316 @@
2.4 +%:wrap=soft:maxLineLen=78:
2.5 +%remove after isabelle build started working -----------------
2.6 +\documentclass{article}
2.7 +\usepackage{../../isabelle,../../isabellesym}
2.8 +\usepackage{graphicx}
2.9 +
2.10 +\usepackage{hyperref} %\url{...} don't use together with isabelle
2.11 +\usepackage{breakurl} %\url{...} don't use together with isabelle
2.12 +\usepackage{paralist} % compactitem
2.13 +
2.14 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
2.15 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
2.16 +\def\see{$\rightarrow$}
2.17 +\newtheorem{UR}{UR}[section]
2.18 +\newtheorem{Expl}{Expl}[section]
2.19 +
2.20 +\begin{document}
2.21 +
2.22 +\section{List of terms used in the \isac-project}\label{terms}
2.23 +%============================================================================
2.24 +This list follows the original one in \cite[Appendix D]{isac:all}. It is a
2.25 +selection concerning the specify-phase. In particular, the terms used for this
2.26 +phase underwent a considerable development since 2002 and are updated to the
2.27 +current, more convenient notions.
2.28 +
2.29 +\begin{description}
2.30 +\item{\bf Calculation} is the document for interactive construction of a
2.31 +result from given items according to some \see Problem definition. It is a
2.32 +variant of ``structured derivations''~\cite{Back-SD09}.
2.33 +
2.34 +\item{\bf Descriptor} is the heading constant of a \see Model-Item in the
2.35 +fields "Given", "Find" and "Relate" (and not in pre-conditions). It indicates
2.36 +the kind of item and constrains the respective type.
2.37 +
2.38 +\item{\bf Example} specifies a particular \see Calculation. It comprises text
2.39 +and/or figure for the student and a \see Formalisation.
2.40 +
2.41 +\item{\bf Formalisation} is the formal part of an \see Example and contains
2.42 +data to complete a \see Specification as a prerequisite for automated
2.43 +generation of user-guidance in a \see Calculation.
2.44 +
2.45 +\item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:
2.46 + \begin{compactitem}
2.47 + \item {\bf RTheory}, an Isabelle theory
2.48 + \item {\bf RProblem} is a \see Model-Pattern.
2.49 + \item {\bf RMethod}: a program guarded by a \see Model serving
2.50 + ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.
2.51 + \end{compactitem}
2.52 + For simplicity reasons, a collection of \see Examples is subsumed to
2.53 + \sisac-Knowledge, too.
2.54 +
2.55 +\item{\bf Method} is a program for a class of Problems. It consists of a
2.56 +program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard
2.57 +with the structure of a \see Model.
2.58 +
2.59 +\item{\bf Model} comprises four fields of \see Model-Items in the line
2.60 +of~\cite{gries}:
2.61 + \begin{compactitem}
2.62 + \item {\bf Given} for the input-items
2.63 + \item {\bf Where} for the pre-conditions constraining the input-items
2.64 + \item {\bf Find} for the output-items
2.65 + \item {\bf Relate} for a part of the post-condition capturing the essence of
2.66 + a problem relating input and output
2.67 + \end{compactitem}
2.68 +
2.69 +\item{\bf Model-Item} is a mathematical term in a \see Model.
2.70 +
2.71 +\item{\bf Model-Pattern} comprises the same fields as a \see Model, but these
2.72 +contain variables to be instanted by the \see Formalisation of an \see Example
2.73 +in order to give \see Model.
2.74 +
2.75 +\item{\bf Problem} is the head of a \see Calculation. Calculations can
2.76 +comprise several sub-problems, arbitrarily nested, with exactly the same
2.77 +structure. A Problem consists of a \see Specification and a \see Solution.
2.78 +
2.79 +\item{\bf References} refer to three kinds of items in the \see
2.80 +\sisac-Knowledge.
2.81 +
2.82 +\item{\bf Solution} are the steps form a \see Specification to a \see
2.83 +Solution, where each step is justified by a \see Tactic. The final step
2.84 +fulfills the post-condition of the \see Model.
2.85 +
2.86 +\item{\bf Specification} comprises data to specify a problem in the \see Model
2.87 +and gives \see References into the \see \sisac-Knowledge.
2.88 +
2.89 +\item{\bf Tactic} transforms a term into another, frequently a rewrite-rule.
2.90 +Since a \see Problem can occur recusively in a Solution as a sub-problem, this
2.91 +is also a particular Tactic.
2.92 +
2.93 +\item{\bf User-Guide} supports a student during interactive \see Calculations.
2.94 +This support is only possible if a \see Formalisation has been transferred
2.95 +(invisibly for a student) from an \see Example.
2.96 +
2.97 +%\item{\bf TODO} xxx
2.98 +\end{description}
2.99 +
2.100 +
2.101 +\section{User Requirements}
2.102 +%============================================================================
2.103 +The User Requirements ({\bf UR}s) do not follow the lines of the original ones
2.104 +in \cite[Part I]{isac:all}, but limit themselves to a student in the
2.105 +specify-phase and use the updated terms from \S\ref{terms} (which are
2.106 +indicated by initial capital letters).
2.107 +
2.108 +{\bf\UR{Examples are selected from
2.109 +collections\label{example-coll}}}\footnote{The present test setup bypasses
2.110 +this UR.}
2.111 +implemented on web-pages, which look like a text book. A specific link at an
2.112 +Example starts an interactive Calculation for that Example. See
2.113 +\url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.
2.114 +
2.115 +{\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in
2.116 +case of standard problems from Computer Algebra with a respective command like
2.117 +${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is
2.118 +Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same
2.119 +structure.
2.120 +
2.121 +{\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and
2.122 +sub-Problems as well, when allowed by the User-Guide. See
2.123 +Exp.\ref{tab:calc-coll}.
2.124 +
2.125 +{\bf\UR{Switching between survey and detail\label{yyy}}} is supported by
2.126 +collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots
2.127 +Expl.\ref{tab:model-sub}
2.128 +
2.129 +{\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means
2.130 +without a preceding Example. In this case an empty Specification is generated
2.131 +by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help
2.132 +the student completing the Specification.
2.133 +
2.134 +{\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see
2.135 +Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific
2.136 +kind of Problem.
2.137 +
2.138 +{\bf\UR{Feedback during input to the Model\label{yyy}}} is given as
2.139 +\begin{compactitem}
2.140 +\item ``correct''
2.141 +\item ``syntax-error'' or type error
2.142 +\item ``superfluous''
2.143 +\item ``incomplete'' in case of lists, sets, etc.
2.144 +\item ``missing''
2.145 +\item ``true'' or ``false'' for predicates in the field Where.
2.146 +\end{compactitem}
2.147 +
2.148 +{\bf\UR{Feedback during input to References\label{yyy}}} is given in the
2.149 +Model:
2.150 +\begin{compactitem}
2.151 +\item Update RTheory: might cause ``syntax-error''
2.152 +\item Update RProblem: might cause ``superfluous'' or ``missing''
2.153 +\item Update RMethod: in this case the Model shows the guard with
2.154 +``superfluous'' or ``missing'' and the keyword Model is annotated with
2.155 +``(RMethod)''.
2.156 +\end{compactitem}
2.157 +
2.158 +{\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}}
2.159 +where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.
2.160 +
2.161 +%{\bf\UR{xxx.\label{yyy}}}
2.162 +
2.163 +
2.164 +\section{Example Calculations}
2.165 +%============================================================================
2.166 +Calculations at different stages of interactive steps towards a Solution and
2.167 +with variants of collapsing and expanding.\\
2.168 +
2.169 +{\bf\Expl{Complete Calculation expanded (sub-Problems
2.170 +collapsed).\label{tab:calc-exp}}}
2.171 +{\tiny \begin{tabbing}
2.172 +12\=12\=12\=12\=\kill
2.173 +Example $<$7.70 a$>$ \\
2.174 +Problem ("Biegelinie", \dots) \\
2.175 +.\>Specification: \\
2.176 +.\>.\>Model: \\
2.177 +.\>.\>.\>Given: "Traeger L", \\
2.178 +.\>.\>.\>Where: "q\_0 ist\dots \\
2.179 +.\>.\>.\>Find: "Biegelinie y" \\
2.180 +.\>.\>.\>Relate: "Rand\dots \\
2.181 +.\>.\>References: \\
2.182 +.\>.\>.\>RTheory: "Bie\dots" \\
2.183 +.\>.\>.\>RProblem: ["\dots] \\
2.184 +.\>.\>.\>RMethod: ["Int\dots] \\
2.185 +.\>Solution: \\
2.186 +.\>.\>Problem ("\dots") \\
2.187 +.\>.\>"[Q x = c + -1 * \dots" \\
2.188 +.\>\vdots \\
2.189 +.\>."y x = $-6 * q\_0 * *$\dots" \\
2.190 +"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
2.191 +\end{tabbing}}
2.192 +
2.193 +{\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}
2.194 +{\tiny \begin{tabbing}
2.195 +12\=12\=12\=12\=\kill
2.196 +Example $<$7.70 a$>$ \\
2.197 +Problem ("Biegelinie", \dots) \\
2.198 +"y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
2.199 +\end{tabbing}}
2.200 +
2.201 +\newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.202 +{\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the
2.203 +inital state with Descriptors, if given by the Example:
2.204 +{\tiny \begin{tabbing}
2.205 +12\=12\=12\=12\=\kill
2.206 +Example $<$7.70 a$>$ \\
2.207 +Problem ("Biegelinie", \dots) \\
2.208 +.\>Specification: \\
2.209 +.\>.\>Model: \\
2.210 +.\>.\>.\>Given: "Traeger ", "Streckenlast " \\
2.211 +.\>.\>.\>Where: \\
2.212 +.\>.\>.\>Find: "Biegelinie " \\
2.213 +.\>.\>.\>Relate: "Randbedingungen [ ]" \\
2.214 +.\>.\>References: \\
2.215 +.\>Solution:
2.216 +\end{tabbing}}
2.217 +
2.218 +{\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the
2.219 +system presents an empty Specification:
2.220 +{\tiny \begin{tabbing}
2.221 +12\=12\=12\=12\=\kill
2.222 +Problem ("", []) \\
2.223 +.\>Specification: \\
2.224 +.\>.\>Model: \\
2.225 +.\>.\>.\>Given: "", "" \\
2.226 +.\>.\>.\>Where: "", "" \\
2.227 +.\>.\>.\>Find: "" \\
2.228 +.\>.\>.\>Relate: "", "" \\
2.229 +.\>.\>References: \\
2.230 +.\>.\>.\>RTheory: "" \\
2.231 +.\>.\>.\>RProblem: ["", ""] \\
2.232 +.\>.\>.\>RMethod: ["", ""] \\
2.233 +.\>Solution:
2.234 +\end{tabbing}}
2.235 +
2.236 +{\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here
2.237 +shown for RTheory and for RProblem; such editing is usually done after some
2.238 +input to the Model:
2.239 +{\tiny \begin{tabbing}
2.240 +12\=12\=12\=12\=\kill
2.241 +Example $<$7.70 a$>$ \\
2.242 +Problem ("Biegelinie", \dots) \\
2.243 +.\>Specification: \\
2.244 +.\>.\>Model: \\
2.245 +.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$" \\
2.246 +.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
2.247 +.\>.\>.\>Find: "Biegelinie y" \\
2.248 +.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
2.249 + y_0 = 0 ]$" \\
2.250 +.\>.\>References: \\
2.251 +.\>.\>.\>RTheory: {\bf"Biegelinie"} \\
2.252 +.\>.\>.\>RProblem: ["Biegelinien"] \\
2.253 +.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
2.254 +.\>Solution:
2.255 +\end{tabbing}}
2.256 +
2.257 +{\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The
2.258 +additional Given item "FunktionsVariable $x$" is usually provided behind the
2.259 +scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can
2.260 +be edited as well.
2.261 +{\tiny \begin{tabbing}
2.262 +12\=12\=12\=12\=\kill
2.263 +Example $<$7.70 a$>$ \\
2.264 +Problem ("Biegelinie", \dots) \\
2.265 +.\>Specification: \\
2.266 +.\>.\>Model (RMethod): \\
2.267 +.\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable
2.268 + $x$" \\
2.269 +.\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
2.270 +.\>.\>.\>Find: "Biegelinie y" \\
2.271 +.\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
2.272 + y_0 = 0 ]$" \\
2.273 +.\>.\>References: \\
2.274 +.\>.\>.\>RTheory: {\bf"Biegelinie"} \\
2.275 +.\>.\>.\>RProblem: ["Biegelinien"] \\
2.276 +.\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
2.277 +.\>Solution:
2.278 +\end{tabbing}}
2.279 +
2.280 +{\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}
2.281 +{\tiny \begin{tabbing}
2.282 +12\=12\=12\=12\=12\=\kill
2.283 +Example $<$7.70 a$>$ \\
2.284 +Problem ("Biegelinie", \dots) \\
2.285 +.\>Specification: \\
2.286 +.\>Solution: \\
2.287 +.\>.\>Problem ("\dots") \\
2.288 +.\>.\>.\>Specification: \\
2.289 +.\>.\>.\>.\>Model: \\
2.290 +.\>.\>.\>.\>.\>Given: "\dots" \\
2.291 +.\>.\>.\>.\>.\>Where: "\dots" \\
2.292 +.\>.\>.\>.\>.\>Find: "\dots" \\
2.293 +.\>.\>.\>.\>.\>Relate: "\dots \\
2.294 +.\>.\>.\>.\>References: \\
2.295 +.\>.\>.\>Solution: \\
2.296 +\end{tabbing}}
2.297 +
2.298 +{\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}
2.299 +{\tiny \begin{tabbing}
2.300 +12\=12\=12\=12\=\kill
2.301 +Example $<$123 d$>$ \\
2.302 +${\it solve} (x + 1 = 2, \,x)$ \\
2.303 +.\>Specification: \\
2.304 +.\>Solution: \\
2.305 +.\>.\>"$x + 1 = 2$" \\
2.306 +.\>.\>"$x = 2 - 1$" \\
2.307 +.\>.\>"$x = 1$" \\
2.308 +"$x = 1$"
2.309 +\end{tabbing}}
2.310 +
2.311 +
2.312 +
2.313 +%\subsection{TODO}
2.314 +%\subsubsection{TODO}
2.315 +
2.316 +\bibliographystyle{plain}
2.317 +\bibliography{root}
2.318 +
2.319 +\end{document}