6 { |
6 { |
7 \usetheme{Hannover} |
7 \usetheme{Hannover} |
8 \setbeamercovered{transparent} |
8 \setbeamercovered{transparent} |
9 } |
9 } |
10 |
10 |
11 %\usepackage{setspace} %for "\begin{onehalfspace}" |
|
12 \usepackage[english]{babel} |
11 \usepackage[english]{babel} |
13 % or whatever |
|
14 |
|
15 \usepackage[utf8]{inputenc} |
12 \usepackage[utf8]{inputenc} |
16 % or whatever |
|
17 |
|
18 \usepackage{times} |
13 \usepackage{times} |
19 \usepackage[T1]{fontenc} |
14 \usepackage[T1]{fontenc} |
20 % Or whatever. Note that the encoding and the font should match. If T1 |
|
21 % does not look nice, try deleting the line with the fontenc. |
|
22 |
15 |
23 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
24 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
17 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
25 |
18 |
26 \title[SPSC in \isac] % (optional, use only with long paper titles) |
19 \title[SPSC in \isac] % (optional, use only with long paper titles) |
27 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} |
20 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} |
28 |
21 |
29 \subtitle{Baccalaureate Thesis} |
22 \subtitle{Baccalaureate Thesis} |
30 |
23 |
31 \author[Rocnik] % (optional, use only with lots of authors) |
24 \author[Ro\v{c}nik] |
32 {Jan~Rocnik} |
25 {Jan Rocnik} |
33 % - Give the names in the same order as the appear in the paper. |
|
34 % - Use the \inst{?} command only if the authors have different |
|
35 % affiliation. |
|
36 |
26 |
37 \institute % (optional, but mostly needed) |
27 \institute % (optional, but mostly needed) |
38 { |
28 { |
39 Technische Universit\"at Graz\\ |
29 Technische Universit\"at Graz\\ |
40 Institut f\"ur TODO |
30 Institut f\"ur TODO |
41 } |
31 } |
42 % - Use the \inst command only if there are several affiliations. |
|
43 % - Keep it simple, no one is interested in your street address. |
|
44 |
|
45 % \date[CFP 2003] % (optional, should be abbreviation of conference name) |
|
46 % {Conference on Fabulous Presentations, 2003} |
|
47 % - Either use conference name or its abbreviation. |
|
48 % - Not really informative to the audience, more for people (including |
|
49 % yourself) who are reading the slides online |
|
50 |
|
51 % \subject{Theoretical Computer Science} |
|
52 % This is only inserted into the PDF information catalog. Can be left |
|
53 % out. |
|
54 |
|
55 |
|
56 |
32 |
57 % If you have a file called "university-logo-filename.xxx", where xxx |
33 % If you have a file called "university-logo-filename.xxx", where xxx |
58 % is a graphic format that can be processed by latex or pdflatex, |
34 % is a graphic format that can be processed by latex or pdflatex, |
59 % resp., then you can add a logo as follows: |
35 % resp., then you can add a logo as follows: |
60 |
36 |
102 %%---------------------------------------------------------------%% |
71 %%---------------------------------------------------------------%% |
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
104 |
73 |
105 \section[Intro]{Introduction} |
74 \section[Intro]{Introduction} |
106 |
75 |
107 \begin{frame}{Introduction} |
76 \begin{frame}{Issues to be Accomplished} |
108 Issues to be accomplished in this thesis: |
|
109 |
77 |
110 \begin{itemize} |
78 \begin{itemize} |
111 |
79 |
112 \item What knowledge is already mechanised in \emph{isabelle}? |
80 \item What knowledge is already mechanised in \emph{isabelle}? |
113 \item How can missing theorems and definitions be mechanised? |
81 \item How can missing theorems and definitions be mechanised? |
114 \item What is the effort for such mechanisation? |
82 \item What is the effort for such mechanisation? |
115 \item How do calculations look like, if using mechanised knowledge? |
83 \item How do calculations look like, by using mechanised knowledge? |
116 \item What are the problems and subproblems to be solved? |
84 \item What problems and subproblems have to be solved? |
117 \item Which problems are already implemented in \sisac? |
85 \item Which problems are already implemented in \sisac? |
118 \item How are the new Problems specified rigorously (\sisac)? |
86 \item How are the new problems specified (\sisac)? |
119 \item Which variantes of programms in \sisac{} solving the problems? |
87 \item Which variantes of programms in \sisac\ solve the problems? |
120 \item What is the contents of the interactiv course material (Figures, etc.)? |
88 \item What is the contents of the interactiv course material (Figures, etc.)? |
121 |
89 |
122 \end{itemize} |
90 \end{itemize} |
123 \end{frame} |
91 \end{frame} |
124 |
92 |
125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
126 %%---------------------------------------------------------------%% |
94 %%---------------------------------------------------------------%% |
127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
128 |
96 |
129 \section[Fourier]{Fourier transform} |
97 \section[Fourier]{Fourier transformation} |
|
98 \subsection[Fourier]{Fourier transform} |
130 |
99 |
131 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
132 %% Fourier INTRO %% |
101 %% Fourier INTRO %% |
133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
134 |
103 |
135 \begin{frame}\frametitle{Fourier Transformation: Introduction} |
104 \begin{frame}\frametitle{Fourier Transformation: Introduction} |
136 \begin{itemize} |
105 \begin{itemize} |
137 \item Transform operation by using property-tables $\rightarrow$ \emph{easy} |
106 \item Transform operation by using property-tables |
138 \item Transform operation by using integral $\rightarrow$ \emph{difficult} |
107 \item Transform operation by using integral |
139 \item No math \emph{tricks} |
|
140 \item Important: Visualisation?! |
108 \item Important: Visualisation?! |
141 \end{itemize} |
109 \end{itemize} |
142 \end{frame} |
110 \end{frame} |
143 |
111 |
144 \subsection[simple]{Fourier transform Example 1} |
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
145 |
113 %% Transform expl SPEC %% |
146 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
147 %% Transform expl 1 SPEC %% |
115 |
148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
116 \begin{frame}\frametitle{Fourier Transformation: Specification} |
149 |
117 {\footnotesize |
150 \begin{frame}\frametitle{Fourier Transform 1: Specification} |
118 |
151 {\footnotesize\it |
119 Determine the fourier transform for the given rectangular impulse: |
152 Fourier Transform |
|
153 |
|
154 \hrulefill |
|
155 |
|
156 \begin{tabbing} |
|
157 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
|
158 \>given \>:\> Time continiues, not periodic Signal \\ |
|
159 \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\ |
|
160 \>precond \>:\> TODO\\ |
|
161 \>find \>:\> $X(j\cdot\omega)$\\ |
|
162 \>postcond \>:\> TODO\\ |
|
163 \end{tabbing} |
|
164 |
|
165 } |
|
166 \end{frame} |
|
167 |
|
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
169 %% Transform expl 1 REQ %% |
|
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
171 |
|
172 \begin{frame}\frametitle{Fourier Transform 1: Development effort} |
|
173 {\small |
|
174 \begin{center} |
|
175 \begin{tabular}{l|l|r} |
|
176 requirements & comments &effort\\ \hline\hline |
|
177 solving Intrgrals & simple via propertie table & 20\\ |
|
178 & \emph{real} & MT\\ \hline |
|
179 transformation table & simple transform & 20\\ \hline |
|
180 example collection & with explanations & 20\\ \hline\hline |
|
181 & & 60-80\\ |
|
182 \end{tabular} |
|
183 \end{center} |
|
184 effort --- in 45min units\\ |
|
185 MT --- thesis ``Integrals'' (mathematics) |
|
186 } |
|
187 \end{frame} |
|
188 |
|
189 \subsection[difficult]{Fourier transform Example 2} |
|
190 |
|
191 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
192 %% Transform expl 2 SPEC %% |
|
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
194 |
|
195 \begin{frame}\frametitle{Fourier Transform 2: Specification} |
|
196 {\footnotesize\it |
|
197 |
|
198 \textbf{(a)} Determine the fourier transform for the given rectangular impulse: |
|
199 |
120 |
200 \begin{center} |
121 \begin{center} |
201 $x(t)= \left\{ |
122 $x(t)= \left\{ |
202 \begin{array}{lr} |
123 \begin{array}{lr} |
203 1 & -1\leq t\leq1\\ |
124 1 & -1\leq t\leq1\\ |
204 0 & else |
125 0 & else |
205 \end{array} |
126 \end{array} |
206 \right.$ |
127 \right.$ |
207 \end{center} |
128 \end{center} |
|
129 |
|
130 \hrulefill |
208 |
131 |
209 \begin{tabbing} |
132 \begin{tabbing} |
210 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
133 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
211 \>given \>:\> piecewise\_function \\ |
134 \>given \>:\> piecewise\_function \\ |
212 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\ |
135 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\ |
244 |
167 |
245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
246 %%--------------------FOURIER---Conclusion-----------------------%% |
169 %%--------------------FOURIER---Conclusion-----------------------%% |
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
248 |
171 |
249 \begin{frame}{Summary} |
172 \begin{frame}{Fourier Transformation: Summary} |
250 todo |
173 \begin{itemize} |
251 |
174 |
252 \begin{itemize} |
175 \item Standard integrals can be solved with tables |
253 |
176 \item No real integration (yet avaiible) |
254 \item todo |
177 \item Math \emph{tricks} difficult to implement |
|
178 |
255 |
179 |
256 \end{itemize} |
180 \end{itemize} |
257 \end{frame} |
181 \end{frame} |
258 |
182 |
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
183 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
260 %-----------------------------------------------------------------% |
184 %-----------------------------------------------------------------% |
261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
262 |
186 |
263 \section[Discrete time]{Discrete-time systems} |
187 \section[LTI Systems]{LTI systems} |
264 \subsection[Convolution]{Convolution} |
188 \subsection[Convolution]{Convolution} |
265 |
189 |
266 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
267 %% LTI INTRO %% |
191 %% LTI INTRO %% |
268 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
422 |
347 |
423 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
424 %%--------------------Z-TRANS---Conclusion-----------------------%% |
349 %%--------------------Z-TRANS---Conclusion-----------------------%% |
425 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
426 |
351 |
427 \begin{frame}{Summary} |
352 \begin{frame}{(Inverse) Z-Transformation: Summary} |
428 todo |
353 \begin{itemize} |
429 |
354 |
430 \begin{itemize} |
355 \item No \emph{higher} math operations |
431 |
356 \item Different subproblems of math (equation systems, etc.) |
432 \item todo |
357 \item Both directions have the same effort |
433 |
358 |
434 \end{itemize} |
359 \end{itemize} |
435 \end{frame} |
360 \end{frame} |
|
361 |
|
362 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
363 %-----------------------------------------------------------------% |
|
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
365 |
|
366 \section[Closing]{Closing} |
|
367 |
|
368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
369 %--------------------------CONCLUSION-----------------------------% |
|
370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
371 |
|
372 \begin{frame}{Conclusions} |
|
373 |
|
374 Design Challanges: |
|
375 |
|
376 {\small |
|
377 \begin{itemize} |
|
378 |
|
379 \item Pre and Post conditions |
|
380 \item Exact mathematic behind functions |
|
381 \item accurate mathematic notation |
|
382 |
|
383 \end{itemize} |
|
384 } |
|
385 |
|
386 Goals: |
|
387 {\small |
|
388 \begin{itemize} |
|
389 |
|
390 \item Spot the power of \sisac |
|
391 \item Implementation of generell but simple math problems |
|
392 \item Setting up a good first guideline (documentation) for furher problem implemenations |
|
393 |
|
394 \end{itemize} |
|
395 |
|
396 \centering{Efforts are only approximations, due we have no \emph{real} experience data!} |
|
397 } |
|
398 |
|
399 \end{frame} |
|
400 |
|
401 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
402 %--------------------------TIME LINE------------------------------% |
|
403 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
404 |
|
405 \begin{frame}{Comming up} |
|
406 |
|
407 {\small |
|
408 \begin{tabular}{l r} |
|
409 |
|
410 Juli 2011 & project startup\\ |
|
411 Juli 2011 & information collection, 1st presentation\\ |
|
412 August 2011 & extern traineeship\\ |
|
413 September 2011 & main work\\ |
|
414 after Oktober & finishing, documentation\\ |
|
415 |
|
416 \end{tabular} |
|
417 } |
|
418 |
|
419 \end{frame} |
|
420 |
436 |
421 |
437 \end{document} |
422 \end{document} |
438 |
423 |
439 |
424 |