equal
deleted
inserted
replaced
300 \label{fig-interactive}} |
300 \label{fig-interactive}} |
301 \end{center} |
301 \end{center} |
302 \end{figure} |
302 \end{figure} |
303 If the student gets stuck and does not know the formula to proceed |
303 If the student gets stuck and does not know the formula to proceed |
304 with, there is the button \framebox{NEXT} presenting the next formula |
304 with, there is the button \framebox{NEXT} presenting the next formula |
305 on the Worksheet. The button \framebox{AUTO} immediately delivers the |
305 on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the |
306 final result in case the student is not interested in intermediate |
306 final result in case the student is not interested in intermediate |
307 steps. |
307 steps. |
308 |
308 |
309 Adaptive dialogue guidance is already under |
309 Adaptive dialogue guidance is already under |
310 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear, |
310 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear, |
324 as well as interactive access to specifications and programs |
324 as well as interactive access to specifications and programs |
325 respectively. |
325 respectively. |
326 |
326 |
327 There is also a simple web-based representation of knowledge items; |
327 There is also a simple web-based representation of knowledge items; |
328 the items under consideration in this paper can be looked up as |
328 the items under consideration in this paper can be looked up as |
329 well~\footnote{ |
329 well~\footnote{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}~\footnote{ |
330 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Inverse\_Z\_Transform.html}}~\footnote{ |
330 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}~\footnote{ |
331 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Partial\_Fractions.html}}. |
331 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}. |
332 |
332 |
333 % can be explained by having a look at |
333 % can be explained by having a look at |
334 % Fig.\ref{fig-interactive} which shows the beginning of the interactive |
334 % Fig.\ref{fig-interactive} which shows the beginning of the interactive |
335 % construction of a solution for the problem. This construction is done in the |
335 % construction of a solution for the problem. This construction is done in the |
336 % right window named ``Worksheet''. |
336 % right window named ``Worksheet''. |
1052 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. |
1052 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. |
1053 |
1053 |
1054 Mechanical treatment requires to translate a textual problem |
1054 Mechanical treatment requires to translate a textual problem |
1055 description like in Fig.\ref{fig-interactive} on |
1055 description like in Fig.\ref{fig-interactive} on |
1056 p.\pageref{fig-interactive} into a {\em formal} specification. The |
1056 p.\pageref{fig-interactive} into a {\em formal} specification. The |
1057 formal specification of the running example could look like is this: |
1057 formal specification of the running example could look like is this |
|
1058 ~\footnote{The ``TODO'' in the postcondition indicates, that postconditions |
|
1059 are not yet handled in the prototype; in particular, the postcondition, i.e. |
|
1060 the correctness of the result is not yet automatically proved.}: |
1058 |
1061 |
1059 %WN Hier brauchen wir die Spezifikation des 'running example' ... |
1062 %WN Hier brauchen wir die Spezifikation des 'running example' ... |
1060 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei |
1063 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei |
1061 %JR der post condition - die existiert für uns ja eigentlich nicht aka |
1064 %JR der post condition - die existiert für uns ja eigentlich nicht aka |
1062 %JR haben sie bis jetzt nicht beachtet WN... |
1065 %JR haben sie bis jetzt nicht beachtet WN... |