diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/final/jrocnik_present1.tex --- a/src/Doc/isac/jrocnik/final/jrocnik_present1.tex Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,434 +0,0 @@ - -\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} - -