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