1 %:wrap=soft:maxLineLen=78:
3 \section{List of terms used in the \isac-project}\label{terms}
4 %============================================================================
5 This list follows the original one in \cite[Appendix D]{isac:all}. It is a
6 selection concerning the specify-phase. In particular, the terms used for this
7 phase underwent a considerable development since 2002 and are updated to the
8 current, more convenient notions.
11 \item{\bf Calculation} is the document for interactive construction of a
12 result from given items according to some \see Problem definition. It is a
13 variant of ``structured derivations''~\cite{Back-SD09}.
15 \item{\bf Descriptor} is the heading constant of a \see Model-Item in the
16 fields "Given", "Find" and "Relate" (and not in pre-conditions). It indicates
17 the kind of item and constrains the respective type.
19 \item{\bf Example} specifies a particular \see Calculation. It comprises text
20 and/or figure for the student and a \see Formalisation.
22 \item{\bf Formalisation} is the formal part of an \see Example and contains
23 data to complete a \see Specification as a prerequisite for automated
24 generation of user-guidance in a \see Calculation.
26 \item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge:
28 \item {\bf RTheory}, an Isabelle theory
29 \item {\bf RProblem} is a \see Model-Pattern.
30 \item {\bf RMethod}: a program guarded by a \see Model serving
31 ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}.
33 For simplicity reasons, a collection of \see Examples is subsumed to
34 \sisac-Knowledge, too.
36 \item{\bf Method} is a program for a class of Problems. It consists of a
37 program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard
38 with the structure of a \see Model.
40 \item{\bf Model} comprises four fields of \see Model-Items in the line
43 \item {\bf Given} for the input-items
44 \item {\bf Where} for the pre-conditions constraining the input-items
45 \item {\bf Find} for the output-items
46 \item {\bf Relate} for a part of the post-condition capturing the essence of
47 a problem relating input and output
50 \item{\bf Model-Item} is a mathematical term in a \see Model.
52 \item{\bf Model-Pattern} comprises the same fields as a \see Model, but these
53 contain variables to be instanted by the \see Formalisation of an \see Example
54 in order to give \see Model.
56 \item{\bf Problem} is the head of a \see Calculation. Calculations can
57 comprise several sub-problems, arbitrarily nested, with exactly the same
58 structure. A Problem consists of a \see Specification and a \see Solution.
60 \item{\bf References} refer to three kinds of items in the \see
63 \item{\bf Solution} are the steps form a \see Specification to a \see
64 Solution, where each step is justified by a \see Tactic. The final step
65 fulfills the post-condition of the \see Model.
67 \item{\bf Specification} comprises data to specify a problem in the \see Model
68 and gives \see References into the \see \sisac-Knowledge.
70 \item{\bf Tactic} transforms a term into another, frequently a rewrite-rule.
71 Since a \see Problem can occur recusively in a Solution as a sub-problem, this
72 is also a particular Tactic.
74 \item{\bf User-Guide} supports a student during interactive \see Calculations.
75 This support is only possible if a \see Formalisation has been transferred
76 (invisibly for a student) from an \see Example.
82 \section{User Requirements}
83 %============================================================================
84 The User Requirements ({\bf UR}s) do not follow the lines of the original ones
85 in \cite[Part I]{isac:all}, but limit themselves to a student in the
86 specify-phase and use the updated terms from \S\ref{terms} (which are
87 indicated by initial capital letters).
89 {\bf\UR{Examples are selected from
90 collections\label{example-coll}}}\footnote{The present test setup bypasses
92 implemented on web-pages, which look like a text book. A specific link at an
93 Example starts an interactive Calculation for that Example. See
94 \url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}.
96 {\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in
97 case of standard problems from Computer Algebra with a respective command like
98 ${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is
99 Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same
102 {\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and
103 sub-Problems as well, when allowed by the User-Guide. See
104 Exp.\ref{tab:calc-coll}.
106 {\bf\UR{Switching between survey and detail\label{yyy}}} is supported by
107 collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots
108 Expl.\ref{tab:model-sub}
110 {\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means
111 without a preceding Example. In this case an empty Specification is generated
112 by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help
113 the student completing the Specification.
115 {\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see
116 Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific
119 {\bf\UR{Feedback during input to the Model\label{yyy}}} is given as
122 \item ``syntax-error'' or type error
123 \item ``superfluous''
124 \item ``incomplete'' in case of lists, sets, etc.
126 \item ``true'' or ``false'' for predicates in the field Where.
129 {\bf\UR{Feedback during input to References\label{yyy}}} is given in the
132 \item Update RTheory: might cause ``syntax-error''
133 \item Update RProblem: might cause ``superfluous'' or ``missing''
134 \item Update RMethod: in this case the Model shows the guard with
135 ``superfluous'' or ``missing'' and the keyword Model is annotated with
139 {\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}}
140 where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}.
142 %{\bf\UR{xxx.\label{yyy}}}
145 \section{Example Calculations}
146 %============================================================================
147 Calculations at different stages of interactive steps towards a Solution and
148 with variants of collapsing and expanding.\\
150 {\bf\Expl{Complete Calculation expanded (sub-Problems
151 collapsed).\label{tab:calc-exp}}}
152 {\tiny \begin{tabbing}
153 12\=12\=12\=12\=\kill
154 Example $<$7.70 a$>$ \\
155 Problem ("Biegelinie", \dots) \\
158 .\>.\>.\>Given: "Traeger L", \\
159 .\>.\>.\>Where: "q\_0 ist\dots \\
160 .\>.\>.\>Find: "Biegelinie y" \\
161 .\>.\>.\>Relate: "Rand\dots \\
163 .\>.\>.\>RTheory: "Bie\dots" \\
164 .\>.\>.\>RProblem: ["\dots] \\
165 .\>.\>.\>RMethod: ["Int\dots] \\
167 .\>.\>Problem ("\dots") \\
168 .\>.\>"[Q x = c + -1 * \dots" \\
170 .\>."y x = $-6 * q\_0 * *$\dots" \\
171 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
174 {\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}}
175 {\tiny \begin{tabbing}
176 12\=12\=12\=12\=\kill
177 Example $<$7.70 a$>$ \\
178 Problem ("Biegelinie", \dots) \\
179 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\
182 \newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183 {\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the
184 inital state with Descriptors, if given by the Example:
185 {\tiny \begin{tabbing}
186 12\=12\=12\=12\=\kill
187 Example $<$7.70 a$>$ \\
188 Problem ("Biegelinie", \dots) \\
191 .\>.\>.\>Given: "Traeger ", "Streckenlast " \\
193 .\>.\>.\>Find: "Biegelinie " \\
194 .\>.\>.\>Relate: "Randbedingungen [ ]" \\
199 {\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the
200 system presents an empty Specification:
201 {\tiny \begin{tabbing}
202 12\=12\=12\=12\=\kill
206 .\>.\>.\>Given: "", "" \\
207 .\>.\>.\>Where: "", "" \\
209 .\>.\>.\>Relate: "", "" \\
211 .\>.\>.\>RTheory: "" \\
212 .\>.\>.\>RProblem: ["", ""] \\
213 .\>.\>.\>RMethod: ["", ""] \\
217 {\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here
218 shown for RTheory and for RProblem; such editing is usually done after some
220 {\tiny \begin{tabbing}
221 12\=12\=12\=12\=\kill
222 Example $<$7.70 a$>$ \\
223 Problem ("Biegelinie", \dots) \\
226 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$" \\
227 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
228 .\>.\>.\>Find: "Biegelinie y" \\
229 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
232 .\>.\>.\>RTheory: {\bf"Biegelinie"} \\
233 .\>.\>.\>RProblem: ["Biegelinien"] \\
234 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
238 {\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The
239 additional Given item "FunktionsVariable $x$" is usually provided behind the
240 scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can
242 {\tiny \begin{tabbing}
243 12\=12\=12\=12\=\kill
244 Example $<$7.70 a$>$ \\
245 Problem ("Biegelinie", \dots) \\
247 .\>.\>Model (RMethod): \\
248 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable
250 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\
251 .\>.\>.\>Find: "Biegelinie y" \\
252 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x
255 .\>.\>.\>RTheory: {\bf"Biegelinie"} \\
256 .\>.\>.\>RProblem: ["Biegelinien"] \\
257 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\
261 {\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}}
262 {\tiny \begin{tabbing}
263 12\=12\=12\=12\=12\=\kill
264 Example $<$7.70 a$>$ \\
265 Problem ("Biegelinie", \dots) \\
268 .\>.\>Problem ("\dots") \\
269 .\>.\>.\>Specification: \\
270 .\>.\>.\>.\>Model: \\
271 .\>.\>.\>.\>.\>Given: "\dots" \\
272 .\>.\>.\>.\>.\>Where: "\dots" \\
273 .\>.\>.\>.\>.\>Find: "\dots" \\
274 .\>.\>.\>.\>.\>Relate: "\dots \\
275 .\>.\>.\>.\>References: \\
276 .\>.\>.\>Solution: \\
279 {\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}}
280 {\tiny \begin{tabbing}
281 12\=12\=12\=12\=\kill
282 Example $<$123 d$>$ \\
283 ${\it solve} (x + 1 = 2, \,x)$ \\
286 .\>.\>"$x + 1 = 2$" \\
287 .\>.\>"$x = 2 - 1$" \\
293 %\subsubsection{TODO}