1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 06 21:54:54 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Sep 07 13:34:07 2012 +0200
1.3 @@ -346,7 +346,13 @@
1.4 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
1.5 % x. \; x$ is the identity function.
1.6
1.7 -%JR warum auskommentiert?
1.8 +%JR warum auskommentiert? WN2...
1.9 +%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
1.10 +%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
1.11 +%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
1.12 +%WN2 gel"oscht.
1.13 +%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
1.14 +%WN2 Platz f"ur Anderes weg.
1.15
1.16 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
1.17 constants \textit{True} and \textit{False} and the usual logical
1.18 @@ -462,7 +468,7 @@
1.19
1.20 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.21
1.22 -%WN was Fachleute unter obigem Titel interessiert findet
1.23 +%WN was Fachleute unter obigem Titel interessiert findet sich
1.24 %WN unterhalb des auskommentierten Textes.
1.25
1.26 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
1.27 @@ -691,7 +697,8 @@
1.28
1.29 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.30 %JR der post condition - die existiert für uns ja eigentlich nicht aka
1.31 -%JR haben sie bis jetzt nicht beachtet
1.32 +%JR haben sie bis jetzt nicht beachtet WN...
1.33 +%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.34
1.35 \label{eg:neuper2}
1.36 {\small\begin{tabbing}
1.37 @@ -826,7 +833,73 @@
1.38 TODO
1.39 \subsection{Implementation of the TP-based Program}\label{progr}
1.40 %WN <--> \chapter 8 der Thesis
1.41 -TODO
1.42 +.\\.\\.\\
1.43 +
1.44 +{\small\it\begin{tabbing}
1.45 +123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
1.46 +\>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
1.47 +\>{\rm 02}\>\> {\tt LET} \\
1.48 +\>{\rm 03}\>\>\> X = {\tt Take} X\_eq ; \\
1.49 +\>{\rm 04}\>\>\> X' = {\tt Rewrite} ruleZY X ; \\
1.50 +\>{\rm 05}\>\>\> (X'\_z::real) = lhs X' ; \\
1.51 +\>{\rm 06}\>\>\> (zzz::real) = argument\_in X'\_z; \\
1.52 +\>{\rm 07}\>\>\> (funterm::real) = rhs X’; \\
1.53 +\>{\rm 07}\>\>\> (pbz::real) = {\tt SubProblem} \\
1.54 +\>{\rm 08}\>\>\>\>\>\>\>\> ( \> Inverse\_Z\_Transform, \\
1.55 +\>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction,rational,simplification]\\
1.56 +\>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\
1.57 +\>{\rm 10}\>\>\>\>\>\>\>\> [ funterm::real, zzz::real ]; \\
1.58 +\>{\rm 12}\>\>\> (pbz\_eq::bool) = {\tt Take} (X'\_z = pbz) ; \\
1.59 +
1.60 +\>{\rm 12}\>\>\> pbz\_eq = {\tt Rewrite} ruleYZ pbz\_eq ; \\
1.61 +\>{\rm 13}\>\>\> pbz\_eq = drop\_questionmarks pbz\_eq ; \\
1.62 +\>{\rm 14}\>\>\> (X\_zeq::bool) = {\tt Take} (X\_z = rhs pbz\_eq) ; \\
1.63 +\>{\rm 15}\>\>\> n\_eq = {\tt Rewrite\_Set} inverse\_z X\_zeq ; \\
1.64 +\>{\rm 15}\>\>\> n\_eq = drop\_questionmarks n\_eq \\
1.65 +\>{\rm 16}\>\> {\tt IN } \\
1.66 +\>{\rm 15}\>\>\> n\_eq
1.67 +\end{tabbing}}
1.68 +
1.69 +{\small\it\begin{tabbing}
1.70 +123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill\label{exp-calc}
1.71 +\>{\rm 01}\> $\bullet$\> {\tt Problem } [maximum\_by, calculus] \`- - -\\
1.72 +\>{\rm 02}\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$ \`- - -\\
1.73 +\>{\rm 03}\>\> $\bullet$\> {\tt Problem } [make, diffable, function] \`- - -\\
1.74 +\>{\rm 04}\>\> \dots\> $\widetilde{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$ \`- - -\\
1.75 +\\
1.76 +\\
1.77 +\>{\rm 18}\>\> $\bullet$\> {\tt Problem} [find\_values, tool] \`- - -\\
1.78 +% \`{\tt Apply\_Method} [tool, find\_values]\\
1.79 +\>{\rm 19}\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] \`- - -\\
1.80 +% \`{\tt Check\_Postcond}\\
1.81 +\>{\rm 20}\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
1.82 +
1.83 +\end{tabbing}}
1.84 +
1.85 +
1.86 +.\\.\\.\\
1.87 +{\footnotesize
1.88 +\begin{verbatim}
1.89 + "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.90 + "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.91 + " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.92 + " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.93 + " (zzz::real) = argument_in X'_z; "^(* z *)
1.94 + " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.95 +
1.96 + " (pbz::real) = (SubProblem (Isac', "^(**)
1.97 + " [partial_fraction,rational,simplification], "^
1.98 + " [simplification,of_rationals,to_partial_fraction]) "^
1.99 + " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.100 +
1.101 + " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.102 + " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.103 + " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.104 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.105 + " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.106 + " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.107 + "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.108 +\end{verbatim}}
1.109
1.110 \section{Workflow of Programming in the Prototype}\label{workflow}
1.111 %WN ``workflow'' heisst: das mache ich zuerst, dann das ...
1.112 @@ -1043,7 +1116,12 @@
1.113
1.114 %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1.115 %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1.116 -%JR gefordert werden...
1.117 +%JR gefordert werden WN2...
1.118 +%WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1.119 +%WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1.120 +%WN2 zusammenschneiden um die R"ander weg zu bekommen)
1.121 +%WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1.122 +%WN2 png + pdf figures mitzuschicken.
1.123
1.124 \subsection{Notes on Problems with Traditional Notation}
1.125