1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/final/jrocnik_present1.tex Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,434 @@
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 +