1.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Sun Feb 19 17:05:06 2012 +0100
1.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Mon Feb 20 18:30:27 2012 +0100
1.3 @@ -34,6 +34,7 @@
1.4
1.5 %isabelle relevant packages
1.6 \usepackage{isabelle,isabellesym}
1.7 +%\isabellestyle{it}
1.8
1.9 %define isac logos
1.10 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.11 @@ -52,6 +53,9 @@
1.12 }
1.13 }
1.14
1.15 +%this should be the last package used
1.16 +%\usepackage{pdfsetup}
1.17 +
1.18 %----------// BEGIN DOCUMENT \\----------%
1.19
1.20 \begin{document}
1.21 @@ -104,7 +108,7 @@
1.22 %the following command was replaced by \newevenside
1.23 %\thispagestyle{empty}\mbox{}\newpage
1.24
1.25 -%----------// T O C \\----------%7
1.26 +%----------// T O C \\----------%7-9
1.27
1.28 \newevenside
1.29
1.30 @@ -113,7 +117,7 @@
1.31 \tableofcontents
1.32 \clearpage
1.33 \pagenumbering{arabic}
1.34 -\setcounter{page}{8}
1.35 +\setcounter{page}{10}
1.36
1.37 %----------// PART-1 \\----------%
1.38
1.39 @@ -178,7 +182,7 @@
1.40 With writing such CTP-based programs authoring is perfect, the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter \cite{wn:lucas-interp-12}. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated CTP to check user input following personalized strategies according to a feedback module.
1.41
1.42 \medskip
1.43 -However ``application programming with CTP'' is not done with writing a program: according to the principles of CTP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}. %TODO: take your example !
1.44 +However ``application programming with CTP'' is not done with writing a program: according to the principles of CTP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}.
1.45
1.46 \begin{example}
1.47 {\small\begin{tabbing}
1.48 @@ -289,55 +293,55 @@
1.49 \subsection{Survey: Requiered Knowledge and Selected Problem(s)}\label{know-missing}
1.50 Following tables (Table~\ref{tab:eff-four},~\ref{tab:eff-conv},~\ref{tab:eff-ztrans}) are showing the expected development effort for speciefic problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
1.51
1.52 -\begin{table}[h]
1.53 -\begin{centering}
1.54 -\begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.55 -requirements & comments &effort\\ \hline\hline
1.56 -solving Intrgrals & simple via propertie table & 20\\
1.57 - & \emph{real} & MT\\ \hline
1.58 -transformation table & simple transform & 20\\ \hline
1.59 -visualisation & backend & 10\\ \hline
1.60 -example collection & with explanations & 20\\ \hline\hline
1.61 -\multicolumn{2}{c|}{} & 70-80\\
1.62 -\end{tabular}
1.63 -\par\end{centering}
1.64 -\caption{Fourier-Transformation development effort\label{tab:eff-four}}
1.65 +\begin{table}
1.66 + \centering
1.67 + \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.68 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.69 + solving Intrgrals & simple via propertie table & 20\\
1.70 + & \emph{real} & MT\\ \hline
1.71 + transformation table & simple transform & 20\\ \hline
1.72 + visualisation & backend & 10\\ \hline
1.73 + example collection & with explanations & 20\\ \hline\hline
1.74 + \multicolumn{2}{c|}{} & 70-80\\
1.75 + \end{tabular}
1.76 +
1.77 + \caption{Fourier-Transformation development effort\label{tab:eff-four}}
1.78 +\end{table}
1.79 +
1.80 +
1.81 +\begin{table}
1.82 + \centering
1.83 + \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.84 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.85 + simplify rationals & {\sisac} & 0\\ \hline
1.86 + define $\sum\limits_{i=0}^{n}i$ & partly {\sisac} & 10\\ \hline
1.87 + simplify sum & termorder & 10\\
1.88 + & simplify rules & 20\\
1.89 + & use simplify rationals& 0\\ \hline
1.90 + index adjustments & with unit step & 10\\ \hline
1.91 + example collection & with explanations & 20\\ \hline\hline
1.92 + \multicolumn{2}{c|}{} & 70-90\\
1.93 + \end{tabular}
1.94 +
1.95 + \caption{Convolution Operations development effort\label{tab:eff-conv}}
1.96 \end{table}
1.97
1.98 -\begin{table}[h]
1.99 -\begin{centering}
1.100 -\begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.101 -requirements & comments &effort\\ \hline\hline
1.102 -simplify rationals & {\sisac} & 0\\ \hline
1.103 -define $\sum\limits_{i=0}^{n}i$ & partly {\sisac} & 10\\ \hline
1.104 -simplify sum & termorder & 10\\
1.105 - & simplify rules & 20\\
1.106 - & use simplify rationals& 0\\ \hline
1.107 -index adjustments & with unit step & 10\\ \hline
1.108 -example collection & with explanations & 20\\ \hline\hline
1.109 -\multicolumn{2}{c|}{} & 70-90\\
1.110 -\end{tabular}
1.111 -\par\end{centering}
1.112 -\caption{Convolution Operations development effort\label{tab:eff-conv}}
1.113 -\end{table}
1.114 +\begin{table}
1.115 + \centering
1.116 + \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.117 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.118 + solve for part.fract. & {\sisac}: degree 2 & 0\\
1.119 + & complex nomminators & 30\\
1.120 + & degree > 2 & MT\\ \hline
1.121 + simplify polynomial & {\sisac} & 0\\
1.122 + simplify rational & {\sisac} & 0\\ \hline
1.123 + partial fraction & degree 2, & 20\\
1.124 + decomposition & specification, method& 30\\ \hline
1.125 + ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline
1.126 + example collection & with explanations & 20\\ \hline\hline
1.127 + \multicolumn{2}{c|}{} & 90-120\\
1.128 + \end{tabular}
1.129
1.130 -\begin{table}[h]
1.131 -\begin{centering}
1.132 -\begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.133 -requirements & comments &effort\\ \hline\hline
1.134 -solve for part.fract. & {\sisac}: degree 2 & 0\\
1.135 - & complex nomminators & 30\\
1.136 - & degree > 2 & MT\\ \hline
1.137 -simplify polynomial & {\sisac} & 0\\
1.138 -simplify rational & {\sisac} & 0\\ \hline
1.139 -partial fraction & degree 2, & 20\\
1.140 -decomposition & specification, method& 30\\ \hline
1.141 -${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline
1.142 -example collection & with explanations & 20\\ \hline\hline
1.143 -\multicolumn{2}{c|}{} & 90-120\\
1.144 -% & & 1 MT
1.145 -\end{tabular}
1.146 -\par\end{centering}
1.147 \caption{Z-Transformation development effort\label{tab:eff-ztrans}}
1.148 \end{table}
1.149
1.150 @@ -424,127 +428,87 @@
1.151 \end{example}
1.152 Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with.
1.153
1.154 -\section{Milestones for the Thesis}
1.155 -The thesis was splitted into six iterations
1.156 +\section{Project Controlling}
1.157 +We decided to split the thesis into five Iteration defined in Section~\ref{sec:milesurv}. As there is also a lot of work todo outer the thesis we accord on an increased contact by mail. For the coordination of the whole {\sisac} files i got access to the mercurial repository. We also appointed on periodic team meetings.
1.158 +
1.159 +\subsection{Survay on Milestones\label{sec:milesurv}}
1.160 +Doing something completly new requires a good controlling, the thesis itself also needs it. After the first meetings and the definition of the intrinsic work we decided on splitting the thesis into the following iterations.
1.161 \begin{description}
1.162 -\item[(29.06. -- 27.07.)] Collection of detailed informations about different STEOP topics \ref{ssec:infcol}
1.163 -\item[(27.07.)] First Prsentation - Decition on which Problems will be implemented \ref{ssec:pres1}
1.164 -\item[(01.09. -- 11.11.)] Implementing the Problem Class in {{\sisac{}}} \ref{ssec:impl}
1.165 -\item[(14.11. -- 02.12.)] Documentation of the Implementation \ref{ssec:doc}
1.166 -\item[(05.12. -- todo)] Writting on the thesis \ref{ssec:thes}
1.167 -\item[todo] Second Prsentation - Work review \ref{ssec:pres2}
1.168 + \item[1st Iteration] Information Collection
1.169 + \item[2nd Iteration] Problem Selection
1.170 + \item[3rd Iteration] Implementation
1.171 + \item[4th Iteration] Thesis Writing
1.172 + \item[5th Iteration] Finalization
1.173 +\end{description}
1.174 +A more detailed description of this milestones can be found in Section~\ref{sec:detmile}.
1.175 +
1.176 +\subsection{Milestone Details\label{sec:detmile}}
1.177 +\begin{description}
1.178 + \item[Information Collection] The first iteration starts by an intruduction to the {\sisac} System and ends up with the first presentation. Listeners of the first presentation were \em Dr. Walther Neuper \normalfont and \em DI Bernhard Geiger\normalfont. We talked about common SPSC problems and the possibilities of realize them in the {\sisac} System. In preparation of the Presentation \em DI Geiger \normalfont sent us a few example problems and we had a experimental survay about the realization effort.
1.179 + \item[Problem Selection] In the second iteration we collected informations about the knowledge mechanized in {\sisac} (cf. Section~\ref{know-isab}). After the first iteration it was clear that implementing of problems in {\sisac} requires a higher effort than originally excpected due this fact the second iteration ends up on the decission which of the provided problems is going to be implemented. We wrote and collected a handfull of experimental scripts regarding sums, fourie transformation and partial fraction decomposition.
1.180 + \item[Implementation] Unfortunataly the biggest and most importent part is the implementation. The iteration started with the decission on the problem and ends up by finishing the test Script (seen in Part~\ref{part:impl}) as well as the integration of this work into the {\sisac}-Knowledge. For a better controlling and result of this iteration we had severell regular meetings (\em Dr. Neuper \normalfont and \em Jan Rocnik\normalfont) and contact over e-mail to assess the state of the {\sisac}-developers work.
1.181 + \item[Thesis Writing] One part of this thesis is generated automatically out of \ttfamily Build\_Inverse\_Z\_Transform\normalfont. Maybe this part well be the most important result of the thesis as it will be used as a documentation for the upcoming developers. Due this fact this iteration started also contemporaneous with the implementation but ends up seperate after finishing the implementation with describing the needed theory and background.
1.182 + \item[Finalization] The work ends up with the last iteration - finalization. It is started by completing the written thesis and the preperation of the second presentation which concludes this project. In the second presentation we will have demonstrated our realised problem embedded in the new {\sisac}-frontend as well as the work, hiding behind. We will also want to give a clear view about the power of {\sisac} and animate the attending agents to go on working within this project.
1.183 \end{description}
1.184
1.185 -\section{Detailed Milestone Description}
1.186 -\subsection{Collection of detailed informations about different STEOP topics}\label{ssec:infcol}
1.187 -identify problems relevant for certain SP lectures
1.188 -estimate chances to realized them within the scope of this thesis
1.189 -order for implementing the problems negotiated with lecturers
1.190 -\subsection{First Prsentation - Decition on which Problems will be implemented}\label{ssec:pres1}
1.191 -\subsection{Implementing the Problem Class in {\sisac}}\label{ssec:impl}
1.192 -\subsection{Documentation of the Implementation}\label{ssec:doc}
1.193 -\subsection{Writting on the thesis}\label{ssec:thes}
1.194 -\subsection{Second Prsentation - Work review}\label{ssec:pres2}
1.195 +%\clearpage
1.196
1.197 +%----------// PART 2 \\----------%
1.198 +
1.199 +\newevenside
1.200 +
1.201 +\part{Implementation\label{part:impl}}
1.202 +\input{./preambleForGeneratedDocuments.tex}
1.203 +\HRule
1.204 +%\setcounter{section}{0}
1.205 +\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.206 +
1.207 +%\clearpage
1.208 +
1.209 +%----------// PART 3 \\----------%
1.210 +
1.211 +\newevenside
1.212 +\part{Summary, Conclusion and Related Work}
1.213 \section{Related Work}\label{sec:related}
1.214 Unusual for a Baccalaureate Thesis, there is {\em no} related work; this requires explanation.
1.215 Of course, this thesis relies on front-of-the wave computer mathematics, on CTP. But {{\sisac{}}} uses CTP in a very specific way, which is too weakly related to other work: programming in the CTP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the CTP-based programming environment.
1.216 \par Another area of work could be considered as related work: authoring of e-learning content. However, {{\sisac{}}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the CTP-based programming language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory.
1.217 \par These two reasons are given for the unusual statement, that there is no related work to be discussed in this thesis.
1.218
1.219 -\section{Review}
1.220 +\section{Summary}
1.221 todo
1.222 \section{Open Questions}
1.223 todo
1.224 \section{Conclusions}
1.225 todo
1.226
1.227 -%\bibliographystyle{alpha}
1.228 -%\bibliography{references}
1.229 -%\bibliography{bib/math-eng,bib/didact,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math}
1.230 +%----------// BIB \\-----------%
1.231
1.232 -
1.233 +\renewcommand{\refname}{\section{Reference}} % Using "Sources" as the title of the section
1.234 +\bibliographystyle{alpha}
1.235 +\bibliography{references}
1.236 \clearpage
1.237
1.238 -%----------// PART 2 \\----------%
1.239 -
1.240 -\newevenside
1.241 -
1.242 -\part{Implementation}
1.243 -
1.244 -
1.245 -\input{./preambleForGeneratedDocuments.tex}
1.246 -
1.247 -\HRule
1.248 -
1.249 -%\setcounter{section}{0}
1.250 -\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.251 -
1.252 -\clearpage
1.253 -
1.254 -
1.255 %----------// APPENDIX \\-----------%
1.256
1.257 \appendix
1.258
1.259 -%----------// BIB \\-----------%
1.260 -
1.261 -%\renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
1.262 -\bibliographystyle{alpha}
1.263 -\bibliography{references}
1.264 -\clearpage
1.265 -
1.266 %----------// WORK TIME \\-----------%
1.267
1.268 -\section{Stundenliste}
1.269 +\newevenside
1.270 +\section{Record of Working Time}
1.271 \begin{footnotesize}
1.272 \begin{longtable}[h]{l p{6.5cm} c c r}
1.273 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
1.274 \hline \hline
1.275 \endhead
1.276 29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\
1.277 -02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\
1.278 -03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\
1.279 -05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\
1.280 -06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\
1.281 -07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\
1.282 -18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\
1.283 -19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\
1.284 -19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
1.285 -21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\
1.286 -22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
1.287 -23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\
1.288 -24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\
1.289 -25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\
1.290 -26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\
1.291 -27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\
1.292 -\hline
1.293 -02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\
1.294 -05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\
1.295 -05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\
1.296 -06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\
1.297 -07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\
1.298 -08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\
1.299 -09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\
1.300 -10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\
1.301 -14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\
1.302 -16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\
1.303 -19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\
1.304 -20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\
1.305 -23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\
1.306 -23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\
1.307 -26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\
1.308 -27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\
1.309 -28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\
1.310 -01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\
1.311 -02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\
1.312 -06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\
1.313 -07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\
1.314 -09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\
1.315 -11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00
1.316 \end{longtable}
1.317 \end{footnotesize}
1.318
1.319 +%----------// CALCULATIONS \\-----------%
1.320 +
1.321 +\newevenside
1.322 \section{Calculations\label{app:calc}}
1.323 \input{calulations}
1.324 \end{document}