8 \setbeamercovered{transparent}
11 \usepackage[english]{babel}
12 \usepackage[utf8]{inputenc}
14 \usepackage[T1]{fontenc}
16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
17 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
19 \title[SPSC in \isac] % (optional, use only with long paper titles)
20 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}
22 \subtitle{Baccalaureate Thesis}
27 \institute % (optional, but mostly needed)
29 Technische Universit\"at Graz\\
33 % If you have a file called "university-logo-filename.xxx", where xxx
34 % is a graphic format that can be processed by latex or pdflatex,
35 % resp., then you can add a logo as follows:
37 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
38 % \logo{\pgfuseimage{university-logo}}
42 % Delete this, if you do not want the table of contents to pop up at
43 % the beginning of each subsection:
46 \begin{frame}<beamer>{Outline}
47 \tableofcontents[currentsection,currentsubsection]
53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
62 %% Table of Contents %%
63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65 \begin{frame}{Outline}
67 % You might wish to add the option [pausesections]
70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
71 %%---------------------------------------------------------------%%
72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
74 \section[Intro]{Introduction}
76 \begin{frame}{Issues to be Accomplished}
80 \item What knowledge is already mechanised in \emph{Isabelle}?
81 \item How can missing theorems and definitions be mechanised?
82 \item What is the effort for such mechanisation?
83 \item How do calculations look like, by using mechanised knowledge?
84 \item What problems and subproblems have to be solved?
85 \item Which problems are already implemented in \sisac?
86 \item How are the new problems specified (\sisac)?
87 \item Which variantes of programms in \sisac\ solve the problems?
88 \item What is the contents of the interactiv course material (Figures, etc.)?
93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94 %%---------------------------------------------------------------%%
95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97 \section[Fourier]{Fourier transformation}
98 \subsection[Fourier]{Fourier transform}
100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
104 \begin{frame}\frametitle{Fourier Transformation: Introduction}
106 \item Transform operation by using property-tables
107 \item Transform operation by using integral
108 \item Important: Visualisation?!
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
113 %% Transform expl SPEC %%
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
116 \begin{frame}\frametitle{Fourier Transformation: Specification}
119 Determine the fourier transform for the given rectangular impulse:
133 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
134 \>given \>:\> piecewise\_function \\
135 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\
136 %?(iterativer) datentyp in Isabelle/HOL
137 \> \> \> translation $T=2$\\
138 \>precond \>:\> TODO\\
139 \>find \>:\> $X(j\cdot\omega)$\\
140 \>postcond \>:\> TODO\\
146 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 %% Transform expl REQ %%
148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
150 \begin{frame}\frametitle{Fourier Transform: Development effort}
153 \begin{tabular}{l|l|r}
154 requirements & comments &effort\\ \hline\hline
155 solving Intrgrals & simple via propertie table & 20\\
156 & \emph{real} & MT\\ \hline
157 transformation table & simple transform & 20\\ \hline
158 visualisation & backend & 10\\ \hline
159 example collection & with explanations & 20\\ \hline\hline
163 effort --- in 45min units\\
164 MT --- thesis ``Integrals'' (mathematics)
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
169 %%--------------------FOURIER---Conclusion-----------------------%%
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
172 \begin{frame}{Fourier Transformation: Summary}
175 \item Standard integrals can be solved with tables
176 \item No real integration (yet avaible)
177 \item Math \emph{tricks} difficult to implement
183 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
184 %-----------------------------------------------------------------%
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
187 \section[LTI Systems]{LTI systems}
188 \subsection[Convolution]{Convolution (Faltung)}
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
194 \begin{frame}\frametitle{Convolution: Introduction}
197 \item Calculation\ldots
198 \item Visualisation\ldots
201 \ldots of parallel filter structures
205 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
207 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
209 \begin{frame}\frametitle{Convolution: Specification}
212 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
215 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\
216 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$
219 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
224 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
225 \>given \>:\> Signals h1[n], h2[n] \\
226 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\
227 %?(iterativer) datentyp in Isabelle/HOL
228 \>precond \>:\> TODO\\
229 \>find \>:\> $h1[n]\,*\,h2[n]$\\
230 \>postcond \>:\> TODO\\
236 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
238 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
240 \begin{frame}\frametitle{Convolution: Development effort}
243 \begin{tabular}{l|l|r}
244 requirements & comments &effort\\ \hline\hline
245 simplify rationals & \sisac & 0\\ \hline
246 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline
247 simplify sum & termorder & 10\\
248 & simplify rules & 20\\
249 & use simplify rationals& 0\\ \hline
250 index adjustments & with unit step & 10\\ \hline
251 example collection & with explanations & 20\\ \hline\hline
255 effort --- in 45min units\\
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
260 %%--------------------LTI-------Conclusion-----------------------%%
261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263 \begin{frame}{Convolution: Summary}
266 \item Standard example
267 \item Straight forward
268 \item Challenge are sum limits
273 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
274 %-----------------------------------------------------------------%
275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
277 \section[Z-transform]{Z-Transform}
278 \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}
280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
281 %% Z-Transform INTRO %%
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
284 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}
286 \item Pure Transformation is simple to realise with Z-Transform Properties (Table)
287 \item Partial Fraction are just math simplifications
291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
292 %% Z-Transform SPEC %%
293 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
295 \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}
298 Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion.
301 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
308 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
309 \>given \>:\> Expression of z \\
310 \> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
311 \>precond \>:\> TODO\\
312 \>find \>:\> Expression of n\\
314 \>postcond \>:\> TODO\\
320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
322 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
325 \begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort}
328 \begin{tabular}{l|l|r}
329 requirements & comments &effort\\ \hline\hline
330 solve for part.fract. & \sisac: degree 2 & 0\\
331 & complex nomminators & 30\\
332 & degree > 2 & MT\\ \hline
333 simplify polynomial & \sisac & 0\\
334 simplify rational & \sisac & 0\\ \hline
335 part.fract.decomposition& degree 2 & \\
336 & specification, method& 30\\ \hline
337 ${\cal Z}^{-1}$ table & & 20\\
338 & explanations, figures& 20\\ \hline
339 example collection & with explanations & 20\\ \hline\hline
344 effort --- in 45min units\\
345 MT --- thesis ``factorization'' (mathematics)
349 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
350 %%--------------------Z-TRANS---Conclusion-----------------------%%
351 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
353 \begin{frame}{(Inverse) Z-Transformation: Summary}
356 \item No \emph{higher} math operations
357 \item Different subproblems of math (equation systems, etc.)
358 \item Both directions have the same effort
363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
364 %-----------------------------------------------------------------%
365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
367 \section[Conclusions]{Conclusions}
369 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
370 %--------------------------CONCLUSION-----------------------------%
371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
373 \begin{frame}{Conclusions}
380 \item Pre and Post conditions
381 \item Exact mathematic behind functions
382 \item accurate mathematic notation
391 \item Spot the power of \sisac
392 \item Implementation of generell but simple math problems
393 \item Setting up a good first guideline (documentation) for furher problem implemenations
397 \centering{Efforts are only approximations, due we have no \emph{real} experience data!}
402 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
403 %--------------------------TIME LINE------------------------------%
404 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
406 \begin{frame}{Comming up}
411 Juli 2011 & project startup\\
412 Juli 2011 & information collection, 1st presentation\\
413 August 2011 & extern traineeship\\
414 September 2011 & main work\\
415 after Oktober & finishing, documentation\\