|
1 %:wrap=soft:maxLineLen=78: |
|
2 %remove after isabelle build started working ----------------- |
|
3 \documentclass{article} |
|
4 \usepackage{../../isabelle,../../isabellesym} |
|
5 \usepackage{graphicx} |
|
6 |
|
7 \usepackage{hyperref} %\url{...} don't use together with isabelle |
|
8 \usepackage{breakurl} %\url{...} don't use together with isabelle |
|
9 \usepackage{paralist} % compactitem |
|
10 |
|
11 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
12 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
13 \def\see{$\rightarrow$} |
|
14 \newtheorem{UR}{UR}[section] |
|
15 \newtheorem{Expl}{Expl}[section] |
|
16 |
|
17 \begin{document} |
|
18 |
|
19 \section{List of terms used in the \isac-project}\label{terms} |
|
20 %============================================================================ |
|
21 This list follows the original one in \cite[Appendix D]{isac:all}. It is a |
|
22 selection concerning the specify-phase. In particular, the terms used for this |
|
23 phase underwent a considerable development since 2002 and are updated to the |
|
24 current, more convenient notions. |
|
25 |
|
26 \begin{description} |
|
27 \item{\bf Calculation} is the document for interactive construction of a |
|
28 result from given items according to some \see Problem definition. It is a |
|
29 variant of ``structured derivations''~\cite{Back-SD09}. |
|
30 |
|
31 \item{\bf Descriptor} is the heading constant of a \see Model-Item in the |
|
32 fields "Given", "Find" and "Relate" (and not in pre-conditions). It indicates |
|
33 the kind of item and constrains the respective type. |
|
34 |
|
35 \item{\bf Example} specifies a particular \see Calculation. It comprises text |
|
36 and/or figure for the student and a \see Formalisation. |
|
37 |
|
38 \item{\bf Formalisation} is the formal part of an \see Example and contains |
|
39 data to complete a \see Specification as a prerequisite for automated |
|
40 generation of user-guidance in a \see Calculation. |
|
41 |
|
42 \item{\bf \sisac-Knowledge} comprises collections of three kinds of knowledge: |
|
43 \begin{compactitem} |
|
44 \item {\bf RTheory}, an Isabelle theory |
|
45 \item {\bf RProblem} is a \see Model-Pattern. |
|
46 \item {\bf RMethod}: a program guarded by a \see Model serving |
|
47 ``Lucas-Interpre-tation''~\cite{EPTCS-wn-20}. |
|
48 \end{compactitem} |
|
49 For simplicity reasons, a collection of \see Examples is subsumed to |
|
50 \sisac-Knowledge, too. |
|
51 |
|
52 \item{\bf Method} is a program for a class of Problems. It consists of a |
|
53 program to be exploited by Lucas-Interpretation \cite{EPTCS-wn-20} and a guard |
|
54 with the structure of a \see Model. |
|
55 |
|
56 \item{\bf Model} comprises four fields of \see Model-Items in the line |
|
57 of~\cite{gries}: |
|
58 \begin{compactitem} |
|
59 \item {\bf Given} for the input-items |
|
60 \item {\bf Where} for the pre-conditions constraining the input-items |
|
61 \item {\bf Find} for the output-items |
|
62 \item {\bf Relate} for a part of the post-condition capturing the essence of |
|
63 a problem relating input and output |
|
64 \end{compactitem} |
|
65 |
|
66 \item{\bf Model-Item} is a mathematical term in a \see Model. |
|
67 |
|
68 \item{\bf Model-Pattern} comprises the same fields as a \see Model, but these |
|
69 contain variables to be instanted by the \see Formalisation of an \see Example |
|
70 in order to give \see Model. |
|
71 |
|
72 \item{\bf Problem} is the head of a \see Calculation. Calculations can |
|
73 comprise several sub-problems, arbitrarily nested, with exactly the same |
|
74 structure. A Problem consists of a \see Specification and a \see Solution. |
|
75 |
|
76 \item{\bf References} refer to three kinds of items in the \see |
|
77 \sisac-Knowledge. |
|
78 |
|
79 \item{\bf Solution} are the steps form a \see Specification to a \see |
|
80 Solution, where each step is justified by a \see Tactic. The final step |
|
81 fulfills the post-condition of the \see Model. |
|
82 |
|
83 \item{\bf Specification} comprises data to specify a problem in the \see Model |
|
84 and gives \see References into the \see \sisac-Knowledge. |
|
85 |
|
86 \item{\bf Tactic} transforms a term into another, frequently a rewrite-rule. |
|
87 Since a \see Problem can occur recusively in a Solution as a sub-problem, this |
|
88 is also a particular Tactic. |
|
89 |
|
90 \item{\bf User-Guide} supports a student during interactive \see Calculations. |
|
91 This support is only possible if a \see Formalisation has been transferred |
|
92 (invisibly for a student) from an \see Example. |
|
93 |
|
94 %\item{\bf TODO} xxx |
|
95 \end{description} |
|
96 |
|
97 |
|
98 \section{User Requirements} |
|
99 %============================================================================ |
|
100 The User Requirements ({\bf UR}s) do not follow the lines of the original ones |
|
101 in \cite[Part I]{isac:all}, but limit themselves to a student in the |
|
102 specify-phase and use the updated terms from \S\ref{terms} (which are |
|
103 indicated by initial capital letters). |
|
104 |
|
105 {\bf\UR{Examples are selected from |
|
106 collections\label{example-coll}}}\footnote{The present test setup bypasses |
|
107 this UR.} |
|
108 implemented on web-pages, which look like a text book. A specific link at an |
|
109 Example starts an interactive Calculation for that Example. See |
|
110 \url{http://www.ist.tugraz.at/projects/isac/www/kbase/exp/exp_Statics_Biegel_Timischl.html}. |
|
111 |
|
112 {\bf\UR{A Calculation is headed by the keyword Problem\label{yyy}}} and in |
|
113 case of standard problems from Computer Algebra with a respective command like |
|
114 ${\it simplify} (x + 1 + 2)$ or ${\it solve} (x + 1 = 2, \,x)$. An example is |
|
115 Expl.\ref{tab:ca}. A Calculation can have sub-Problems with exactly the same |
|
116 structure. |
|
117 |
|
118 {\bf\UR{A Calculation can be completed with one keystroke\label{yyy}}} and |
|
119 sub-Problems as well, when allowed by the User-Guide. See |
|
120 Exp.\ref{tab:calc-coll}. |
|
121 |
|
122 {\bf\UR{Switching between survey and detail\label{yyy}}} is supported by |
|
123 collapsing and expanding a Calculation, see Expl.\ref{tab:calc-exp} \dots |
|
124 Expl.\ref{tab:model-sub} |
|
125 |
|
126 {\bf\UR{A Calculation can be started from scratch\label{yyy}}}, that means |
|
127 without a preceding Example. In this case an empty Specification is generated |
|
128 by the system (see Expl.\ref{tab:mod-empty}) and the User-Guide cannot help |
|
129 the student completing the Specification. |
|
130 |
|
131 {\bf\UR{Input to the Model is guided by Descriptors\label{yyy}}}, see |
|
132 Expl.\ref{tab:model}, which are given by the Model-Pattern for the specific |
|
133 kind of Problem. |
|
134 |
|
135 {\bf\UR{Feedback during input to the Model\label{yyy}}} is given as |
|
136 \begin{compactitem} |
|
137 \item ``correct'' |
|
138 \item ``syntax-error'' or type error |
|
139 \item ``superfluous'' |
|
140 \item ``incomplete'' in case of lists, sets, etc. |
|
141 \item ``missing'' |
|
142 \item ``true'' or ``false'' for predicates in the field Where. |
|
143 \end{compactitem} |
|
144 |
|
145 {\bf\UR{Feedback during input to References\label{yyy}}} is given in the |
|
146 Model: |
|
147 \begin{compactitem} |
|
148 \item Update RTheory: might cause ``syntax-error'' |
|
149 \item Update RProblem: might cause ``superfluous'' or ``missing'' |
|
150 \item Update RMethod: in this case the Model shows the guard with |
|
151 ``superfluous'' or ``missing'' and the keyword Model is annotated with |
|
152 ``(RMethod)''. |
|
153 \end{compactitem} |
|
154 |
|
155 {\bf\UR{The Model can be switched between RProblem and RMethod,\label{yyy}}} |
|
156 where the latter is indicated by ``Model (RMethod)''< see Expl.\ref{tab:refs}. |
|
157 |
|
158 %{\bf\UR{xxx.\label{yyy}}} |
|
159 |
|
160 |
|
161 \section{Example Calculations} |
|
162 %============================================================================ |
|
163 Calculations at different stages of interactive steps towards a Solution and |
|
164 with variants of collapsing and expanding.\\ |
|
165 |
|
166 {\bf\Expl{Complete Calculation expanded (sub-Problems |
|
167 collapsed).\label{tab:calc-exp}}} |
|
168 {\tiny \begin{tabbing} |
|
169 12\=12\=12\=12\=\kill |
|
170 Example $<$7.70 a$>$ \\ |
|
171 Problem ("Biegelinie", \dots) \\ |
|
172 .\>Specification: \\ |
|
173 .\>.\>Model: \\ |
|
174 .\>.\>.\>Given: "Traeger L", \\ |
|
175 .\>.\>.\>Where: "q\_0 ist\dots \\ |
|
176 .\>.\>.\>Find: "Biegelinie y" \\ |
|
177 .\>.\>.\>Relate: "Rand\dots \\ |
|
178 .\>.\>References: \\ |
|
179 .\>.\>.\>RTheory: "Bie\dots" \\ |
|
180 .\>.\>.\>RProblem: ["\dots] \\ |
|
181 .\>.\>.\>RMethod: ["Int\dots] \\ |
|
182 .\>Solution: \\ |
|
183 .\>.\>Problem ("\dots") \\ |
|
184 .\>.\>"[Q x = c + -1 * \dots" \\ |
|
185 .\>\vdots \\ |
|
186 .\>."y x = $-6 * q\_0 * *$\dots" \\ |
|
187 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\ |
|
188 \end{tabbing}} |
|
189 |
|
190 {\bf\Expl{Complete Calculation collapsed.\label{tab:calc-coll}}} |
|
191 {\tiny \begin{tabbing} |
|
192 12\=12\=12\=12\=\kill |
|
193 Example $<$7.70 a$>$ \\ |
|
194 Problem ("Biegelinie", \dots) \\ |
|
195 "y x = $-6 * q\_0 * L ^ 2 /$\dots"\\ |
|
196 \end{tabbing}} |
|
197 |
|
198 \newpage %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
199 {\bf\Expl{Interactive Specification editing the Model\label{tab:model}}}, the |
|
200 inital state with Descriptors, if given by the Example: |
|
201 {\tiny \begin{tabbing} |
|
202 12\=12\=12\=12\=\kill |
|
203 Example $<$7.70 a$>$ \\ |
|
204 Problem ("Biegelinie", \dots) \\ |
|
205 .\>Specification: \\ |
|
206 .\>.\>Model: \\ |
|
207 .\>.\>.\>Given: "Traeger ", "Streckenlast " \\ |
|
208 .\>.\>.\>Where: \\ |
|
209 .\>.\>.\>Find: "Biegelinie " \\ |
|
210 .\>.\>.\>Relate: "Randbedingungen [ ]" \\ |
|
211 .\>.\>References: \\ |
|
212 .\>Solution: |
|
213 \end{tabbing}} |
|
214 |
|
215 {\bf\Expl{Interactive Specification from scratch\label{tab:mod-empty}}}, the |
|
216 system presents an empty Specification: |
|
217 {\tiny \begin{tabbing} |
|
218 12\=12\=12\=12\=\kill |
|
219 Problem ("", []) \\ |
|
220 .\>Specification: \\ |
|
221 .\>.\>Model: \\ |
|
222 .\>.\>.\>Given: "", "" \\ |
|
223 .\>.\>.\>Where: "", "" \\ |
|
224 .\>.\>.\>Find: "" \\ |
|
225 .\>.\>.\>Relate: "", "" \\ |
|
226 .\>.\>References: \\ |
|
227 .\>.\>.\>RTheory: "" \\ |
|
228 .\>.\>.\>RProblem: ["", ""] \\ |
|
229 .\>.\>.\>RMethod: ["", ""] \\ |
|
230 .\>Solution: |
|
231 \end{tabbing}} |
|
232 |
|
233 {\bf\Expl{Interactive Specification editing References\label{tab:refs}}}, here |
|
234 shown for RTheory and for RProblem; such editing is usually done after some |
|
235 input to the Model: |
|
236 {\tiny \begin{tabbing} |
|
237 12\=12\=12\=12\=\kill |
|
238 Example $<$7.70 a$>$ \\ |
|
239 Problem ("Biegelinie", \dots) \\ |
|
240 .\>Specification: \\ |
|
241 .\>.\>Model: \\ |
|
242 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$" \\ |
|
243 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\ |
|
244 .\>.\>.\>Find: "Biegelinie y" \\ |
|
245 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x |
|
246 y_0 = 0 ]$" \\ |
|
247 .\>.\>References: \\ |
|
248 .\>.\>.\>RTheory: {\bf"Biegelinie"} \\ |
|
249 .\>.\>.\>RProblem: ["Biegelinien"] \\ |
|
250 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\ |
|
251 .\>Solution: |
|
252 \end{tabbing}} |
|
253 |
|
254 {\bf\Expl{Interactive Specification editing RMethod\label{tab:refs-met}}}. The |
|
255 additional Given item "FunktionsVariable $x$" is usually provided behind the |
|
256 scenes; but in case of editing RMethod the "Model (RMethod)" is shown and can |
|
257 be edited as well. |
|
258 {\tiny \begin{tabbing} |
|
259 12\=12\=12\=12\=\kill |
|
260 Example $<$7.70 a$>$ \\ |
|
261 Problem ("Biegelinie", \dots) \\ |
|
262 .\>Specification: \\ |
|
263 .\>.\>Model (RMethod): \\ |
|
264 .\>.\>.\>Given: "Traegerlaenge L", "Streckenlast $q_0$", "FunktionsVariable |
|
265 $x$" \\ |
|
266 .\>.\>.\>Where: "$q_0$ ist\_integrierbar\_auf $\{| 0, L |\}$", "$0 < L"$\\ |
|
267 .\>.\>.\>Find: "Biegelinie y" \\ |
|
268 .\>.\>.\>Relate: "Randbedingungen $[ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x |
|
269 y_0 = 0 ]$" \\ |
|
270 .\>.\>References: \\ |
|
271 .\>.\>.\>RTheory: {\bf"Biegelinie"} \\ |
|
272 .\>.\>.\>RProblem: ["Biegelinien"] \\ |
|
273 .\>.\>.\>RMethod: ["Integrieren", "KonstanteBestimmen2"] \\ |
|
274 .\>Solution: |
|
275 \end{tabbing}} |
|
276 |
|
277 {\bf\Expl{Interactively solving the sub-Problem.\label{tab:model-sub}}} |
|
278 {\tiny \begin{tabbing} |
|
279 12\=12\=12\=12\=12\=\kill |
|
280 Example $<$7.70 a$>$ \\ |
|
281 Problem ("Biegelinie", \dots) \\ |
|
282 .\>Specification: \\ |
|
283 .\>Solution: \\ |
|
284 .\>.\>Problem ("\dots") \\ |
|
285 .\>.\>.\>Specification: \\ |
|
286 .\>.\>.\>.\>Model: \\ |
|
287 .\>.\>.\>.\>.\>Given: "\dots" \\ |
|
288 .\>.\>.\>.\>.\>Where: "\dots" \\ |
|
289 .\>.\>.\>.\>.\>Find: "\dots" \\ |
|
290 .\>.\>.\>.\>.\>Relate: "\dots \\ |
|
291 .\>.\>.\>.\>References: \\ |
|
292 .\>.\>.\>Solution: \\ |
|
293 \end{tabbing}} |
|
294 |
|
295 {\bf\Expl{Calculation like in Computer Algebra.\label{tab:ca}}} |
|
296 {\tiny \begin{tabbing} |
|
297 12\=12\=12\=12\=\kill |
|
298 Example $<$123 d$>$ \\ |
|
299 ${\it solve} (x + 1 = 2, \,x)$ \\ |
|
300 .\>Specification: \\ |
|
301 .\>Solution: \\ |
|
302 .\>.\>"$x + 1 = 2$" \\ |
|
303 .\>.\>"$x = 2 - 1$" \\ |
|
304 .\>.\>"$x = 1$" \\ |
|
305 "$x = 1$" |
|
306 \end{tabbing}} |
|
307 |
|
308 |
|
309 |
|
310 %\subsection{TODO} |
|
311 %\subsubsection{TODO} |
|
312 |
|
313 \bibliographystyle{plain} |
|
314 \bibliography{root} |
|
315 |
|
316 \end{document} |