calculus, etc.~\footnote{The programs existing in the {\sisac}

 calculus, etc.~\footnote{The programs existing in the {\sisac}

 prototype are found at

 prototype are found at

 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})

 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})

 \paragraph{The mathematical background of the running example} is the

 \paragraph{The mathematical background of the running example} is the

 discrete-time signals is the counterpart of the Laplace transform for

 discrete-time signals is the counterpart of the Laplace transform for

 continuous-time signals, and they each have a similar relationship to

 continuous-time signals, and they each have a similar relationship to

 the corresponding Fourier transform. One motivation for introducing

 the corresponding Fourier transform. One motivation for introducing

 this generalization is that the Fourier transform does not converge

 this generalization is that the Fourier transform does not converge

 for all sequences, and it is useful to have a generalization of the

 for all sequences, and it is useful to have a generalization of the

 Fourier transform that encompasses a broader class of signals. A

 Fourier transform that encompasses a broader class of signals. A

 notation is often more convenient than the Fourier transform

 notation is often more convenient than the Fourier transform

 is defined as

 is defined as

 \begin{equation*}

 \begin{equation*}

 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}

 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}

 \end{equation*}

 \end{equation*}

 where a discrete time sequence $x[n]$ is transformed into the function

 where a discrete time sequence $x[n]$ is transformed into the function

 the integral

 the integral

 \begin{equation*}

 \begin{equation*}

 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz

 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz

 \end{equation*}

 \end{equation*}

 where the letter $C$ represents a contour within the range of

 where the letter $C$ represents a contour within the range of

 case of this contour. Remember that $j$ is the complex number in the

 case of this contour. Remember that $j$ is the complex number in the

 be solved, tables of commonly used transform pairs are used in

 be solved, tables of commonly used transform pairs are used in

 education as well as in engineering practice; such tables can be found

 education as well as in engineering practice; such tables can be found

 at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.

 at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.

 A completely solved and more detailed example can be found at

 A completely solved and more detailed example can be found at

 ~\cite[p. 149f]{oppenheim2010discrete}. 

 ~\cite[p. 149f]{oppenheim2010discrete}. 

 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately

 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately

 % Isabelle comprises a mechanism (called ``axiomatization''), which

 % Isabelle comprises a mechanism (called ``axiomatization''), which

 % allows to omit proofs. Such a theorem is shown in

 % allows to omit proofs. Such a theorem is shown in

 % Example~\ref{eg:neuper1}.

 % Example~\ref{eg:neuper1}.

 is accustomed to specific notation for the resulting functions, which

 is accustomed to specific notation for the resulting functions, which

 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the

 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the

 function, $n$ is the argument and the brackets indicate that the

 function, $n$ is the argument and the brackets indicate that the

 arguments are discrete. Surprisingly, Isabelle accepts the rules for

 arguments are discrete. Surprisingly, Isabelle accepts the rules for

 $z^{-1}$ in this traditional notation~\footnote{Isabelle

 $z^{-1}$ in this traditional notation~\footnote{Isabelle

   07\>\>  rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''

   07\>\>  rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''

   \end{tabbing}}

   \end{tabbing}}

 % \end{example}

 % \end{example}

 %}

 %}

 These 6 rules can be used as conditional rewrite rules, depending on

 These 6 rules can be used as conditional rewrite rules, depending on

 programming language expects these rules as {\em proved} theorems, and

 programming language expects these rules as {\em proved} theorems, and

 not as axioms implemented in the above brute force manner; otherwise

 not as axioms implemented in the above brute force manner; otherwise

 all the verification efforts envisaged (like proof of the

 all the verification efforts envisaged (like proof of the

 post-condition, see below) would be meaningless.

 post-condition, see below) would be meaningless.

 Isabelle provides a large body of knowledge, rigorously proved from

 Isabelle provides a large body of knowledge, rigorously proved from

 the basic axioms of mathematics~\footnote{This way of rigorously

 the basic axioms of mathematics~\footnote{This way of rigorously

 deriving all knowledge from first principles is called the

 deriving all knowledge from first principles is called the

 knowledge can be found in the theories on Multivariate

 knowledge can be found in the theories on Multivariate

 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,

 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,

 building up knowledge such that a proof for the above rules would be

 building up knowledge such that a proof for the above rules would be

 reasonably short and easily comprehensible, still requires lots of

 reasonably short and easily comprehensible, still requires lots of

 work (and is definitely out of scope of our case study).

 work (and is definitely out of scope of our case study).

 program has been adapted in an unelegant way.

 program has been adapted in an unelegant way.

 \item Implement an algorithms for partial fraction decomposition,

 \item Implement an algorithms for partial fraction decomposition,

 which is considered a standard normal form in Computer Algebra.

 which is considered a standard normal form in Computer Algebra.

 \item Implement a specification for partial fraction decomposition and

 \item Implement a specification for partial fraction decomposition and

 locate it appropriately in the hierarchy of specification.

 locate it appropriately in the hierarchy of specification.

 case study).

 case study).

 \end{itemize}

 \end{itemize}

 On the other hand, for the one the class of problems implemented,

 On the other hand, for the one the class of problems implemented,

 adding an arbitrary number of examples within this class requires a

 adding an arbitrary number of examples within this class requires a

 few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an

 few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an