1.1 --- a/src/Doc/isac/jrocnik/final/jrocnik_present1.tex Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,434 +0,0 @@
1.4 -
1.5 -\documentclass{beamer}
1.6 -
1.7 -
1.8 -\mode<presentation>
1.9 -{
1.10 - \usetheme{Hannover}
1.11 - \setbeamercovered{transparent}
1.12 -}
1.13 -
1.14 -\usepackage[english]{babel}
1.15 -\usepackage[utf8]{inputenc}
1.16 -\usepackage{times}
1.17 -\usepackage[T1]{fontenc}
1.18 -
1.19 -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.20 -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.21 -
1.22 -\title[SPSC in \isac] % (optional, use only with long paper titles)
1.23 -{Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}
1.24 -
1.25 -\subtitle{Baccalaureate Thesis}
1.26 -
1.27 -\author[Ro\v{c}nik]
1.28 -{Jan Rocnik}
1.29 -
1.30 -\institute % (optional, but mostly needed)
1.31 -{
1.32 - Technische Universit\"at Graz\\
1.33 - Institut f\"ur TODO
1.34 -}
1.35 -
1.36 -% If you have a file called "university-logo-filename.xxx", where xxx
1.37 -% is a graphic format that can be processed by latex or pdflatex,
1.38 -% resp., then you can add a logo as follows:
1.39 -
1.40 -% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
1.41 -% \logo{\pgfuseimage{university-logo}}
1.42 -
1.43 -
1.44 -
1.45 -% Delete this, if you do not want the table of contents to pop up at
1.46 -% the beginning of each subsection:
1.47 -\AtBeginSubsection[]
1.48 -{
1.49 - \begin{frame}<beamer>{Outline}
1.50 - \tableofcontents[currentsection,currentsubsection]
1.51 - \end{frame}
1.52 -}
1.53 -
1.54 -\begin{document}
1.55 -
1.56 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.57 -%% Title Page %%
1.58 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.59 -
1.60 -\begin{frame}
1.61 - \titlepage
1.62 -\end{frame}
1.63 -
1.64 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.65 -%% Table of Contents %%
1.66 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.67 -
1.68 -\begin{frame}{Outline}
1.69 - \tableofcontents
1.70 - % You might wish to add the option [pausesections]
1.71 -\end{frame}
1.72 -
1.73 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.74 -%%---------------------------------------------------------------%%
1.75 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.76 -
1.77 -\section[Intro]{Introduction}
1.78 -
1.79 -\begin{frame}{Issues to be Accomplished}
1.80 -
1.81 -\begin{itemize}
1.82 -
1.83 -\item What knowledge is already mechanised in \emph{Isabelle}?
1.84 -\item How can missing theorems and definitions be mechanised?
1.85 -\item What is the effort for such mechanisation?
1.86 -\item How do calculations look like, by using mechanised knowledge?
1.87 -\item What problems and subproblems have to be solved?
1.88 -\item Which problems are already implemented in \sisac?
1.89 -\item How are the new problems specified (\sisac)?
1.90 -\item Which variantes of programms in \sisac\ solve the problems?
1.91 -\item What is the contents of the interactiv course material (Figures, etc.)?
1.92 -
1.93 -\end{itemize}
1.94 -\end{frame}
1.95 -
1.96 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.97 -%%---------------------------------------------------------------%%
1.98 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.99 -
1.100 -\section[Fourier]{Fourier transformation}
1.101 -\subsection[Fourier]{Fourier transform}
1.102 -
1.103 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.104 -%% Fourier INTRO %%
1.105 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.106 -
1.107 -\begin{frame}\frametitle{Fourier Transformation: Introduction}
1.108 -Possibilities:
1.109 -\begin{itemize}
1.110 -\item Transform operation by using property-tables
1.111 -\item Transform operation by using integral
1.112 -\end{itemize}
1.113 -Also Important:
1.114 -\begin{itemize}
1.115 -\item Visualisation?!
1.116 -\end{itemize}
1.117 -\end{frame}
1.118 -
1.119 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.120 -%% Transform expl SPEC %%
1.121 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.122 -
1.123 -\begin{frame}\frametitle{Fourier Transformation: Specification}
1.124 -{\footnotesize
1.125 -
1.126 -Determine the fourier transform for the given rectangular impulse:
1.127 -
1.128 -\begin{center}
1.129 -$x(t)= \left\{
1.130 - \begin{array}{lr}
1.131 - 1 & -1\leq t\leq1\\
1.132 - 0 & else
1.133 - \end{array}
1.134 - \right.$
1.135 -\end{center}
1.136 -
1.137 -\hrulefill
1.138 -
1.139 -\begin{tabbing}
1.140 -1\=postcond \=: \= \= $\;\;\;\;$\=\kill
1.141 -\>given \>:\> piecewise\_function \\
1.142 -\> \> \> \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\
1.143 -\>precond \>:\> TODO\\
1.144 -\>find \>:\> $X(j\cdot\omega)$\\
1.145 -\>postcond \>:\> TODO\\
1.146 -\end{tabbing}
1.147 -
1.148 -}
1.149 -\end{frame}
1.150 -
1.151 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.152 -%% Transform expl REQ %%
1.153 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.154 -
1.155 -\begin{frame}\frametitle{Fourier Transform: Development effort}
1.156 -{\small
1.157 -\begin{center}
1.158 -\begin{tabular}{l|l|r}
1.159 -requirements & comments &effort\\ \hline\hline
1.160 -solving Intrgrals & simple via propertie table & 20\\
1.161 - & \emph{real} & MT\\ \hline
1.162 -transformation table & simple transform & 20\\ \hline
1.163 -visualisation & backend & 10\\ \hline
1.164 -example collection & with explanations & 20\\ \hline\hline
1.165 - & & 70-80\\
1.166 -\end{tabular}
1.167 -\end{center}
1.168 -effort --- in 45min units\\
1.169 -MT --- thesis ``Integrals'' (mathematics)
1.170 -}
1.171 -\end{frame}
1.172 -
1.173 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.174 -%%--------------------FOURIER---Conclusion-----------------------%%
1.175 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.176 -
1.177 -\begin{frame}{Fourier Transformation: Summary}
1.178 -\begin{itemize}
1.179 -
1.180 -\item Standard integrals can be solved with tables
1.181 -\item No real integration (yet avaible)
1.182 -\item Math \emph{tricks} difficult to implement
1.183 -
1.184 -
1.185 -\end{itemize}
1.186 -\end{frame}
1.187 -
1.188 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.189 -%-----------------------------------------------------------------%
1.190 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.191 -
1.192 -\section[LTI Systems]{LTI systems}
1.193 -\subsection[Convolution]{Convolution (Faltung)}
1.194 -
1.195 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.196 -%% LTI INTRO %%
1.197 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.198 -
1.199 -\begin{frame}\frametitle{Convolution: Introduction}
1.200 -\begin{itemize}
1.201 -\item Calculation include sums
1.202 -\item Demonstrative examples
1.203 -\item Visualisation is important
1.204 -\end{itemize}
1.205 -\end{frame}
1.206 -
1.207 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.208 -%% LTI SPEC %%
1.209 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.210 -
1.211 -\begin{frame}\frametitle{Convolution: Specification}
1.212 -{\footnotesize
1.213 -
1.214 -Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
1.215 -
1.216 -\begin{center}
1.217 -$h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\
1.218 -$h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$
1.219 -\end{center}
1.220 -
1.221 -The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
1.222 -
1.223 -\hrulefill
1.224 -
1.225 -\begin{tabbing}
1.226 -1\=postcond \=: \= \= $\;\;\;\;$\=\kill
1.227 -\>given \>:\> Signals h1[n], h2[n] \\
1.228 -\> \> \> \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\
1.229 -
1.230 -\>precond \>:\> TODO\\
1.231 -\>find \>:\> $h1[n]\,*\,h2[n]$\\
1.232 -\>postcond \>:\> TODO\\
1.233 -\end{tabbing}
1.234 -
1.235 -}
1.236 -\end{frame}
1.237 -
1.238 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.239 -%% LTI REQ %%
1.240 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.241 -
1.242 -\begin{frame}\frametitle{Convolution: Development effort}
1.243 -{\small
1.244 -\begin{center}
1.245 -\begin{tabular}{l|l|r}
1.246 -requirements & comments &effort\\ \hline\hline
1.247 -simplify rationals & \sisac & 0\\ \hline
1.248 -define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline
1.249 -simplify sum & termorder & 10\\
1.250 - & simplify rules & 20\\
1.251 - & use simplify rationals& 0\\ \hline
1.252 -index adjustments & with unit step & 10\\ \hline
1.253 -example collection & with explanations & 20\\ \hline\hline
1.254 - & & 70-90\\
1.255 -\end{tabular}
1.256 -\end{center}
1.257 -effort --- in 45min units\\
1.258 -}
1.259 -\end{frame}
1.260 -
1.261 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.262 -%%--------------------LTI-------Conclusion-----------------------%%
1.263 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.264 -
1.265 -\begin{frame}{Convolution: Summary}
1.266 -\begin{itemize}
1.267 -
1.268 -\item Standard example
1.269 -\item Straight forward
1.270 -\item Challenge are sum limits
1.271 -
1.272 -\end{itemize}
1.273 -\end{frame}
1.274 -
1.275 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.276 -%-----------------------------------------------------------------%
1.277 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.278 -
1.279 -\section[Z-transform]{Z-Transform}
1.280 -\subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}
1.281 -
1.282 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.283 -%% Z-Transform INTRO %%
1.284 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.285 -
1.286 -\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}
1.287 -\begin{itemize}
1.288 -\item Pure Transformation is simple to realise with Z-Transform Properties (Table)
1.289 -\item Partial Fraction are just math simplifications
1.290 -\end{itemize}
1.291 -\end{frame}
1.292 -
1.293 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.294 -%% Z-Transform SPEC %%
1.295 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.296 -
1.297 -\begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}
1.298 -{\footnotesize
1.299 -
1.300 -Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion.
1.301 -
1.302 -\begin{center}
1.303 -$X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
1.304 -\end{center}
1.305 -
1.306 -
1.307 -\hrulefill
1.308 -
1.309 -\begin{tabbing}
1.310 -1\=postcond \=: \= \= $\;\;\;\;$\=\kill
1.311 -\>given \>:\> Expression of z \\
1.312 -\> \> \> \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
1.313 -\>precond \>:\> TODO\\
1.314 -\>find \>:\> Expression of n\\
1.315 -\> \> \> \>$h[n]$\\
1.316 -\>postcond \>:\> TODO\\
1.317 -\end{tabbing}
1.318 -
1.319 -}
1.320 -\end{frame}
1.321 -
1.322 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.323 -%% Z expl REQ %%
1.324 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.325 -
1.326 -
1.327 -\begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort}
1.328 -{\small
1.329 -\begin{center}
1.330 -\begin{tabular}{l|l|r}
1.331 -requirements & comments &effort\\ \hline\hline
1.332 -solve for part.fract. & \sisac: degree 2 & 0\\
1.333 - & complex nomminators & 30\\
1.334 - & degree > 2 & MT\\ \hline
1.335 -simplify polynomial & \sisac & 0\\
1.336 -simplify rational & \sisac & 0\\ \hline
1.337 -part.fract.decomposition& degree 2 & \\
1.338 - & specification, method& 30\\ \hline
1.339 -${\cal Z}^{-1}$ table & & 20\\
1.340 - & explanations, figures& 20\\ \hline
1.341 -example collection & with explanations & 20\\ \hline\hline
1.342 - & & 90-120\\
1.343 -% & & 1 MT
1.344 -\end{tabular}
1.345 -\end{center}
1.346 -effort --- in 45min units\\
1.347 -MT --- thesis ``factorization'' (mathematics)
1.348 -}
1.349 -\end{frame}
1.350 -
1.351 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.352 -%%--------------------Z-TRANS---Conclusion-----------------------%%
1.353 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.354 -
1.355 -\begin{frame}{(Inverse) Z-Transformation: Summary}
1.356 -\begin{itemize}
1.357 -
1.358 -\item No \emph{higher} math operations
1.359 -\item Different subproblems of math (equation systems, etc.)
1.360 -\item Both directions have the same effort
1.361 -
1.362 -\end{itemize}
1.363 -\end{frame}
1.364 -
1.365 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.366 -%-----------------------------------------------------------------%
1.367 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.368 -
1.369 -\section[Conclusions]{Conclusions}
1.370 -
1.371 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.372 -%--------------------------DEMONSTRATION--------------------------%
1.373 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.374 -
1.375 -\begin{frame}{Demonstration}
1.376 -
1.377 -\centering{Demonstration}
1.378 -
1.379 -\end{frame}
1.380 -
1.381 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.382 -%--------------------------CONCLUSION-----------------------------%
1.383 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.384 -
1.385 -\begin{frame}{Conclusions}
1.386 -
1.387 -Design Challanges:
1.388 -
1.389 -{\small
1.390 -\begin{itemize}
1.391 -
1.392 -\item Pre and Post conditions
1.393 -\item Exact mathematic behind functions
1.394 -\item Accurate mathematic notation
1.395 -
1.396 -\end{itemize}
1.397 -}
1.398 -
1.399 -Goals:
1.400 -{\small
1.401 -\begin{itemize}
1.402 -
1.403 -\item Spot the power of \sisac
1.404 -\item Implementation of generell but simple math problems
1.405 -\item Setting up a good first guideline (documentation) for furher problem implemenations
1.406 -
1.407 -\end{itemize}
1.408 -
1.409 -\centering{Efforts are only approximations, due we have no \emph{real} experience data!}
1.410 -}
1.411 -
1.412 -\end{frame}
1.413 -
1.414 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.415 -%--------------------------TIME LINE------------------------------%
1.416 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.417 -
1.418 -\begin{frame}{Comming up}
1.419 -
1.420 -{\small
1.421 -\begin{tabular}{l r}
1.422 -
1.423 -Juli 2011 & project startup\\
1.424 -Juli 2011 & information collection, 1st presentation\\
1.425 -August 2011 & extern traineeship\\
1.426 -September 2011 & main work\\
1.427 -after Oktober & finishing, documentation\\
1.428 -
1.429 -\end{tabular}
1.430 -}
1.431 -
1.432 -\end{frame}
1.433 -
1.434 -
1.435 -\end{document}
1.436 -
1.437 -