%--*- latex -*-----------------------------------------------------------------
%$Author: saulius $
%$Date: 2020-06-04 14:58:32 +0300 (Thu, 04 Jun 2020) $ 
%$Revision: 1524 $
%$URL: svn+ssh://saulius-grazulis.lt/home/saulius/svn-repositories/seminarai/2020-verifikacjos-seminarui/slides.tex $
%------------------------------------------------------------------------------

\documentclass[mathserif]{beamer}
\usetheme{Warwick}
\useoutertheme{infolines}
\setbeamertemplate{headline}{} % removes the headline that infolines inserts
%\setbeamertemplate{footline}[frame number]
\renewcommand\familydefault{\rmdefault}
% For XeLaTeX:
% https://tex.stackexchange.com/questions/452151/how-do-i-render-the-word-v%C7%ABlundarkvi%C3%B0a-with-bookman-and-xelatex
% "Use an OpenType clone of Bookman, for instance TeX Gyre Bonum":
\usepackage{fontspec}
\setmainfont{TeX Gyre Bonum}

\usepackage{colordvi}
\usepackage{graphicx}
\usepackage{tikz}
\usetikzlibrary{snakes}
\usepackage{verbatim}
\usepackage{listings}
\usepackage{chemfig}
\usepackage{listings}

% https://en.wikibooks.org/wiki/LaTeX/Algorithms
% http://mirror.datacenter.by/pub/mirrors/CTAN/macros/latex/contrib/algorithmicx/algorithmicx.pdf
\usepackage{algpseudocode}
\usepackage{algorithm}
\usepackage{amssymb}

\include{commands}

\newcommand{\RCSid}[1]{\fontsize{7pt}{7pt}\selectfont $#1$ \today}

\title{Potential applications of formal methods in crystallography?}

\author{Saulius Gražulis}

\date{Vilnius, 2020}

\begin{document}

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

\begin{frame}
    \titlepage

    \centerline{\scriptsize Vilnius University Institute of Biotechnology}

    \begin{center}
      \mbox{}
      \hfill\hfill\hfill
      \includegraphics[height=1.5cm]{images/sp_VU_zenklas.eps}
      \hfill
      \includegraphics[height=1.5cm]{images/BTI-logo-no-text.eps}
      \hfill\hfill\hfill
      \mbox{}
    \end{center}

    \vfill

    \RCSid{
      $Id: slides.tex 1524 2020-06-04 11:58:32Z saulius $
    }
\end{frame}

%==============================================================================

\begin{frame}
  \frametitle{Crystall lattice}

  \begin{center}
    \only<1>{
      \includegraphics[width=0.9\textwidth]{images/crystall-lattice.pdf}
    }
    \only<2>{
      \includegraphics[width=0.9\textwidth]{images/crystall-lattice-translations.pdf}
    }
  \end{center}

\end{frame}

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

\begin{frame}
  \frametitle{Rotation operations}

  \begin{center}
    \includegraphics[width=0.9\textwidth]{images/posūkio-operatoriai.pdf}
  \end{center}

\end{frame}

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

\begin{frame}
  \frametitle{Group theory algorithms}

  Spacegroup Builder
  \vspace{0.7\baselineskip}

  \scriptsize
  \begin{algorithmic}[0]
    \Require{$\mathbb{H}$ -- a subgroup of a finite group
      $\mathbb{G}$} \Require{$g$ -- an element of the
      finite group $\mathbb{G}$, $g \in \mathbb{G}$}
    \Ensure{The list $L$ of the operators of a subgroup
      $\mathbb{L}\leq\mathbb{G}$ without duplicates}
    \Ensure{$\mathbb{L} = \langle \mathbb{H}, \langle g
      \rangle \rangle$}

    \Procedure{SimpleBuider}{$\mathbb{H},g$}
    \newline
    \Comment{Build a spacegroup generated by $\mathbb{H}$ and $g$}
    \State $L\gets (e,h_1,h_2,\dots,h_n)$,
    where $h_i\in\mathbb{H} \; \forall i$
    \State $L_{new}\gets (g)$
    \While{$L_{new}$ is not empty}
    \State $g' \gets \textrm{shift}(L_{new})$
    \State $L \gets (L, g')$
    \ForAll{$h' \in L$}
    \State $g'' \gets h' g'$
    \If{$g'' \notin L \cup L_{new}$}
    \State $L_{new} \gets (L_{new}, g'')$
    \EndIf
    \EndFor
    \EndWhile
    \State \textbf{return} $L$
    \EndProcedure
  \end{algorithmic}

\end{frame}

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

\begin{frame}
  \frametitle{Algorithm correctness issues}

  Questions:

  \begin{itemize}
  \item Is this algorithm ``correct''?
  \item Are the specified invariants specified?
  \item Under which assumptions the invariants hold (e.g. is it
    essential that the group $\mathbb{H}$ is finite)?
  \end{itemize}
  
\end{frame}

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

\begin{frame}
  \frametitle{General program correctness}

  \begin{center}
    \only<1>{
      \includegraphics[height=7.5cm]{images/spec-sharp-failing.png}
    }
    \only<2>{
      \includegraphics[height=7.5cm]{images/spec-sharp-verified.png}
    }
  \end{center}
  
\end{frame}

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

\begin{frame}
  \frametitle{General program correctness}

  \lstset{basicstyle=\small\tt,frame=trBL,language=Java,keywordstyle=\color{blue},commentstyle=\tt\color{red}}
  \only<1>{
    \lstinputlisting{programos/mono/spec-example.cs}
  }
  \only<2->{
    \lstinputlisting{programos/mono/spec-example-failing.cs}
  }
  
\end{frame}

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

\begin{frame}[containsverbatim]
  \frametitle{Real life...}

  \lstset{basicstyle=\tiny\tt,frame=trBL,language=Java,keywordstyle=\color{blue},commentstyle=\tt\color{red}}
  \lstinputlisting{programos/mono/spec-example-failing.cs}

\begin{verbatim}
saulius@kolibris integer-overflow-check/ $ mono spec
-2147483648
\end{verbatim}

\end{frame}

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

\begin{frame}
  \frametitle{Euklido algoritmas pasibaigia:}

  \lstset{language=perl}
  \showfile[basicstyle=\ttfamily\scriptsize,commentstyle=\color{blue}\sl]
           {programos/perl/gcd-finitness-proof.perl}

\end{frame}

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

\begin{frame}
  \frametitle{Euklido algoritmas tikrai duoda DBD:}

  \lstset{language=perl}
  \showfile[basicstyle=\ttfamily\scriptsize,commentstyle=\color{blue}\sl]
           {programos/perl/gcd-correctness-proof.perl}

\end{frame}

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

\begin{frame}
  \frametitle{Pradinių sąlygų užtikrinimas}
  \lstset{language=perl}
  \showfile[basicstyle=\ttfamily\scriptsize]
           {programos/perl/gcd-with-asserts.perl}

\end{frame}

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

\begin{frame}
  \frametitle{Floating point vs BigRat}

  Real numbers:
  $$
  \sum_{n = 1}^3 \frac{1}{3} = 1
  $$
  
  Floats:
  $$
  \sum_{n = 1}^3 \frac{1}{3} \ne 1
  $$
  
  Real numbers:
  $$
  \sum_{n = 1}^{256} \frac{1}{256} = 1
  $$
  
  Floats:
  $$
  \sum_{n = 1}^{256} \frac{1}{256} = 1
  $$
  
\end{frame}

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

\begin{frame}
  \frametitle{Questions}

  \begin{itemize}
  \item will my float lose precission?
  \item will my rational number overlow RAM?
  \end{itemize}
  
\end{frame}

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

\setbeamertemplate{footline}{
  \tiny
  \rule[-0.4\baselineskip]{0pt}{1.2\baselineskip}
  \hspace{1ex}
  {\em
    A path to freedom: 
    GNU $\rightarrow$
    Linux $\rightarrow$
    Ubuntu $\rightarrow$
    MySQL $\rightarrow$
    R $\rightarrow$
    \LaTeX $\rightarrow$
    TikZ $\rightarrow$
    Beamer
  }
}
  
\begin{frame}

  \centerline{\Large Thank you!}

  \vfill

  \begin{centering}
    %% \includegraphics[height=3cm]{images/Sphalerite-Quartz-261762.eps.gz}
      \begin{tabbing}
        \hspace{8mm} \=
        \includegraphics[width=4cm]{images/topaz-picture.png} \=
        \hspace{1cm} \=
        \includegraphics[width=5cm]{images/topaz-structure.png} \\
        \>
        \tiny
        \mywebref{http://en.wikipedia.org/wiki/Topaz} \> \>
        \tiny
        \mywebref{http://www.crystallography.net/2207377.html} \\
      \end{tabbing}
  \end{centering}

\end{frame}

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

\begin{frame}[allowframebreaks]
  \frametitle{References}

  \scriptsize
  %% \bibliographystyle{plain}                                                                                                                                                           
  \bibliographystyle{apalike}
  \bibliography{bibliography/citations}

\end{frame}

%------------------------------------------------------------------------------                                                                                                          
\end{document}
