diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/final/jrocnik_present1.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-isac/jrocnik/final/jrocnik_present1.tex Tue Sep 17 09:50:52 2013 +0200 @@ -0,0 +1,434 @@ + +\documentclass{beamer} + + +\mode +{ + \usetheme{Hannover} + \setbeamercovered{transparent} +} + +\usepackage[english]{babel} +\usepackage[utf8]{inputenc} +\usepackage{times} +\usepackage[T1]{fontenc} + +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} + +\title[SPSC in \isac] % (optional, use only with long paper titles) +{Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} + +\subtitle{Baccalaureate Thesis} + +\author[Ro\v{c}nik] +{Jan Rocnik} + +\institute % (optional, but mostly needed) +{ + Technische Universit\"at Graz\\ + Institut f\"ur TODO +} + +% If you have a file called "university-logo-filename.xxx", where xxx +% is a graphic format that can be processed by latex or pdflatex, +% resp., then you can add a logo as follows: + +% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename} +% \logo{\pgfuseimage{university-logo}} + + + +% Delete this, if you do not want the table of contents to pop up at +% the beginning of each subsection: +\AtBeginSubsection[] +{ + \begin{frame}{Outline} + \tableofcontents[currentsection,currentsubsection] + \end{frame} +} + +\begin{document} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Title Page %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame} + \titlepage +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Table of Contents %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Outline} + \tableofcontents + % You might wish to add the option [pausesections] +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%---------------------------------------------------------------%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section[Intro]{Introduction} + +\begin{frame}{Issues to be Accomplished} + +\begin{itemize} + +\item What knowledge is already mechanised in \emph{Isabelle}? +\item How can missing theorems and definitions be mechanised? +\item What is the effort for such mechanisation? +\item How do calculations look like, by using mechanised knowledge? +\item What problems and subproblems have to be solved? +\item Which problems are already implemented in \sisac? +\item How are the new problems specified (\sisac)? +\item Which variantes of programms in \sisac\ solve the problems? +\item What is the contents of the interactiv course material (Figures, etc.)? + +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%---------------------------------------------------------------%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section[Fourier]{Fourier transformation} +\subsection[Fourier]{Fourier transform} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Fourier INTRO %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Fourier Transformation: Introduction} +Possibilities: +\begin{itemize} +\item Transform operation by using property-tables +\item Transform operation by using integral +\end{itemize} +Also Important: +\begin{itemize} +\item Visualisation?! +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Transform expl SPEC %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Fourier Transformation: Specification} +{\footnotesize + +Determine the fourier transform for the given rectangular impulse: + +\begin{center} +$x(t)= \left\{ + \begin{array}{lr} + 1 & -1\leq t\leq1\\ + 0 & else + \end{array} + \right.$ +\end{center} + +\hrulefill + +\begin{tabbing} +1\=postcond \=: \= \= $\;\;\;\;$\=\kill +\>given \>:\> piecewise\_function \\ +\> \> \> \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\ +\>precond \>:\> TODO\\ +\>find \>:\> $X(j\cdot\omega)$\\ +\>postcond \>:\> TODO\\ +\end{tabbing} + +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Transform expl REQ %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Fourier Transform: Development effort} +{\small +\begin{center} +\begin{tabular}{l|l|r} +requirements & comments &effort\\ \hline\hline +solving Intrgrals & simple via propertie table & 20\\ + & \emph{real} & MT\\ \hline +transformation table & simple transform & 20\\ \hline +visualisation & backend & 10\\ \hline +example collection & with explanations & 20\\ \hline\hline + & & 70-80\\ +\end{tabular} +\end{center} +effort --- in 45min units\\ +MT --- thesis ``Integrals'' (mathematics) +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%--------------------FOURIER---Conclusion-----------------------%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Fourier Transformation: Summary} +\begin{itemize} + +\item Standard integrals can be solved with tables +\item No real integration (yet avaible) +\item Math \emph{tricks} difficult to implement + + +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%-----------------------------------------------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section[LTI Systems]{LTI systems} +\subsection[Convolution]{Convolution (Faltung)} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% LTI INTRO %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Convolution: Introduction} +\begin{itemize} +\item Calculation include sums +\item Demonstrative examples +\item Visualisation is important +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% LTI SPEC %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Convolution: Specification} +{\footnotesize + +Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response: + +\begin{center} +$h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\ +$h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$ +\end{center} + +The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. + +\hrulefill + +\begin{tabbing} +1\=postcond \=: \= \= $\;\;\;\;$\=\kill +\>given \>:\> Signals h1[n], h2[n] \\ +\> \> \> \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\ + +\>precond \>:\> TODO\\ +\>find \>:\> $h1[n]\,*\,h2[n]$\\ +\>postcond \>:\> TODO\\ +\end{tabbing} + +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% LTI REQ %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{Convolution: Development effort} +{\small +\begin{center} +\begin{tabular}{l|l|r} +requirements & comments &effort\\ \hline\hline +simplify rationals & \sisac & 0\\ \hline +define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline +simplify sum & termorder & 10\\ + & simplify rules & 20\\ + & use simplify rationals& 0\\ \hline +index adjustments & with unit step & 10\\ \hline +example collection & with explanations & 20\\ \hline\hline + & & 70-90\\ +\end{tabular} +\end{center} +effort --- in 45min units\\ +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%--------------------LTI-------Conclusion-----------------------%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Convolution: Summary} +\begin{itemize} + +\item Standard example +\item Straight forward +\item Challenge are sum limits + +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%-----------------------------------------------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section[Z-transform]{Z-Transform} +\subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Z-Transform INTRO %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction} +\begin{itemize} +\item Pure Transformation is simple to realise with Z-Transform Properties (Table) +\item Partial Fraction are just math simplifications +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Z-Transform SPEC %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}\frametitle{(Inverse) Z-Transformation: Specification} +{\footnotesize + +Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion. + +\begin{center} +$X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable +\end{center} + + +\hrulefill + +\begin{tabbing} +1\=postcond \=: \= \= $\;\;\;\;$\=\kill +\>given \>:\> Expression of z \\ +\> \> \> \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\ +\>precond \>:\> TODO\\ +\>find \>:\> Expression of n\\ +\> \> \> \>$h[n]$\\ +\>postcond \>:\> TODO\\ +\end{tabbing} + +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Z expl REQ %% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort} +{\small +\begin{center} +\begin{tabular}{l|l|r} +requirements & comments &effort\\ \hline\hline +solve for part.fract. & \sisac: degree 2 & 0\\ + & complex nomminators & 30\\ + & degree > 2 & MT\\ \hline +simplify polynomial & \sisac & 0\\ +simplify rational & \sisac & 0\\ \hline +part.fract.decomposition& degree 2 & \\ + & specification, method& 30\\ \hline +${\cal Z}^{-1}$ table & & 20\\ + & explanations, figures& 20\\ \hline +example collection & with explanations & 20\\ \hline\hline + & & 90-120\\ +% & & 1 MT +\end{tabular} +\end{center} +effort --- in 45min units\\ +MT --- thesis ``factorization'' (mathematics) +} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%--------------------Z-TRANS---Conclusion-----------------------%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{(Inverse) Z-Transformation: Summary} +\begin{itemize} + +\item No \emph{higher} math operations +\item Different subproblems of math (equation systems, etc.) +\item Both directions have the same effort + +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%-----------------------------------------------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section[Conclusions]{Conclusions} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%--------------------------DEMONSTRATION--------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Demonstration} + +\centering{Demonstration} + +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%--------------------------CONCLUSION-----------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Conclusions} + +Design Challanges: + +{\small +\begin{itemize} + +\item Pre and Post conditions +\item Exact mathematic behind functions +\item Accurate mathematic notation + +\end{itemize} +} + +Goals: +{\small +\begin{itemize} + +\item Spot the power of \sisac +\item Implementation of generell but simple math problems +\item Setting up a good first guideline (documentation) for furher problem implemenations + +\end{itemize} + +\centering{Efforts are only approximations, due we have no \emph{real} experience data!} +} + +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%--------------------------TIME LINE------------------------------% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}{Comming up} + +{\small +\begin{tabular}{l r} + +Juli 2011 & project startup\\ +Juli 2011 & information collection, 1st presentation\\ +August 2011 & extern traineeship\\ +September 2011 & main work\\ +after Oktober & finishing, documentation\\ + +\end{tabular} +} + +\end{frame} + + +\end{document} + +