\documentclass{beamer}

\mode<presentation>

{

  \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}<beamer>{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}

\begin{itemize}

\item Transform operation by using property-tables

\item Transform operation by using integral

\item Important: 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 \\

\>         \> \>  \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\

                        %?(iterativer) datentyp in Isabelle/HOL

\>         \> \>  translation $T=2$\\

\>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 avaiible)

\item Math \emph{tricks} difficult to implement

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%-----------------------------------------------------------------%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section[LTI Systems]{LTI systems}

\subsection[Convolution]{Convolution}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												LTI INTRO				                       %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Convolution: Introduction}

\begin{itemize}

\item Calculation\ldots

\item Visualisation\ldots

\end{itemize}

\begin{center}

\ldots of parallel filter structures

\end{center}

\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::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\

                        %?(iterativer) datentyp in Isabelle/HOL

\>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 foreward

\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::real\,+z::imag),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[Closing]{Closing}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%--------------------------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}