defence.tex

\documentclass{beamer}

% copy-paste from mystyle...
\usepackage[utf8]{inputenc}

\usepackage{inconsolata} %nicer font for code listings. (Use \ttfamily for lstinline bastype)

\usepackage[english, estonian]{babel} %the thesis is in Estonian

% widen, narrow - https://tex.stackexchange.com/a/203931, https://tex.stackexchange.com/q/50057
% this looks weird with partially thicker overlapping lines...
\usepackage{scalerel}
\def\widen{\mathrel{\ThisStyle{\stretchrel*{\ooalign{%
  \raise0.2\LMex\hbox{$\SavedStyle\sqcup$}\cr%
  \raise-0.2\LMex\hbox{$\SavedStyle\sqcup$}}}{\sqcup}}}}
\def\narrow{\mathrel{\ThisStyle{\stretchrel*{\ooalign{%
  \raise0.2\LMex\hbox{$\SavedStyle\sqcap$}\cr%
  \raise-0.2\LMex\hbox{$\SavedStyle\sqcap$}}}{\sqcap}}}}

\usepackage{tabu}   % Wide lines in tables
\usepackage{multirow}

\usepackage[outputdir=build]{minted}
\setminted{
	autogobble=true,
	tabsize=4
}
% \RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{} % center all minted - https://tex.stackexchange.com/a/161128
\usepackage{xpatch,letltxmacro}
\LetLtxMacro{\bminted}{\minted}
\let\endbminted\endminted
\xpretocmd{\bminted}{\RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{}}{}{}
% BVerbatim removes margins (https://tex.stackexchange.com/q/142444) and doesn't support frame

% If you really want to draw figures in LaTeX use packages tikz or pstricks
% However, getting a corresponding illustrations is really painful
\usepackage{tikz}
\usetikzlibrary{positioning,automata,arrows,fit,calc}

\renewcommand<>{\emph}[1]{{\only#2{\em}#1}} % https://tex.stackexchange.com/a/274385
\renewcommand{\em}{\bfseries} % always bold emphasis

\usepackage{comment}

\usepackage{appendixnumberbeamer}

\usepackage{pifont}
\DeclareUnicodeCharacter{2713}{\ding{51}}
\DeclareUnicodeCharacter{2717}{\hspace{1pt}\ding{55}\hspace{1pt}} % TODO: fucking hack

\usepackage{xcolor}


\input{mymacros}
\newcommand{\emptycolumn}[1]{\begin{column}{#1}\end{column}} % beamer columns must be manually padded to center...


\title[Domeenide testimine]{\mytitle}
\subtitle[]{Bakalaureusetöö}
\author{\myauthor}
\institute[]{Tartu Ülikool, arvutiteaduse instituut}
\date{13. juuni 2018}

\usetheme{Madrid}

\begin{document}

\frame{\titlepage}

\begin{frame}{Ülesehitus}
	\tableofcontents
\end{frame}

\section{Sissejuhatus}
\begin{frame}{Sissejuhatus}
\begin{itemize}
	\item Staatiline analüüs --- programme ei käivitata
	\begin{itemize}
		\item Vigade otsimine
		\item Vigade puudumise tõestamine
	\end{itemize}

	\item Abstraktne interpretatsioon
	\begin{itemize}
		\item Ligikaudsed seisundid --- domeen
		\item Teooria garanteerib korrektsuse (\ingl{sound})
	\end{itemize}

	\item Analüsaatorites esineb vigu
	\begin{itemize}
		\item Analüüs ja selle korrektsus rikutud
	\end{itemize}
\end{itemize}

\vfill
\pause
\begin{block}{Eesmärk}
	Analüsaatori Goblint
	\begin{itemize}
		\item Domeenide omaduspõhine testimine
		\item Vigade tuvastamine
	\end{itemize}
\end{block}
\end{frame}

\begin{frame}{Näiteks intervallid}
\begin{itemize}
	\item Täisarvude staatiliseks analüüsiks saab kasutada \emph{intervalle}
	\begin{itemize}
		\item Näiteks $[0, 3],\; [-1, 5],\; [2, 2],\; [1, +\infty],\; [-\infty, +\infty]$
	\end{itemize}

	\item Aritmeetilised tehted intervallidel
	\begin{itemize}
		\item Näiteks liitmine $[0, 3] + [-1, 5] = [-1, 8]$
	\end{itemize}

	\pause
	\item Osalise järjestuse seos sisalduvuse kaudu
	\begin{itemize}
		\item Näiteks $[2, 2] \sqleq [0, 3] \sqleq [-1, 5] \sqleq [-\infty, +\infty]$
		\item Kokkuleppeliselt väiksem tähendab täpsemat
	\end{itemize}

	\item Ühendamise tehe ühendi kaudu
	\begin{itemize}
		\item Näiteks $[0, 3] \sqcup [5, 7] = [0, 7]$
	\end{itemize}

	\item Suurim intervall
	\begin{itemize}
		\item $\top = [-\infty, +\infty]$
	\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Näidisanalüüs intervallidega}
\begin{columns}
	\emptycolumn{0.05\textwidth}
	\begin{column}{0.4\textwidth}
		\centering
		\begin{bminted}{c}
			int x = 0;
			while (x < 100)
				x++;
		\end{bminted}
	\end{column}
	\begin{column}{0.5\textwidth}
		\visible<2->{\alert{Muutuja \texttt{x} väärtus}}

		\centering
		\begin{tikzpicture}[
			->,>=stealth,
			node distance=0.75cm,
			every state/.style={inner sep=3pt, minimum size=0pt},
			stmt/.style={font=\ttfamily},
			initial text={},
			initial where=above
		]
			\node[initial,state,label=right:{{\visible<2->{\alert{$\bot$}}}}] (1) {1};
			\node[state,label={[yshift=0.2cm]right:{{\visible<2->{\alert{$[0, 100]$}}}}}] (2) [below=of 1] {2};
			\node[state,label=left:{{\visible<2->{\alert{$[0, 99]$}}}}] (3) [below left=of 2] {3};
			\node[accepting,state,label=right:{{\visible<2->{\alert{$[100, 100]$}}}}] (4) [below right=of 2] {4};

			\path
				(1) edge node[stmt,right] {x = 0} (2)
				(2) edge[bend right] node[stmt,above left,near start] {x < 100} (3)
				    edge node[stmt,above right] {x >= 100} (4)
				(3) edge[bend right] node[stmt,below right,very near start] {x++} (2);
		\end{tikzpicture}
	\end{column}
	\emptycolumn{0.05\textwidth}
\end{columns}
\end{frame}

\section{Teoreetiline taust}
\begin{frame}{Täielikud võred}
%\begin{itemize}
	%\item
	Domeen moodustab \emph{täieliku võre}:
	\begin{itemize}
		\item Elementide hulk $\mathbb{D}$
		\item Osalise järjestuse seos $\sqleq$
		\item Ülemise raja tehe $\sqcup$
		\item Alumise raja tehe $\sqcap$
		\item Suurim element $\top$
		\item Vähim element $\bot$
	\end{itemize}
%\end{itemize}
\end{frame}

\begin{frame}[fragile]{Domeenide omadused}
Olgu $\mathbb{D}$ täielik võre, siis iga $a, b, c \in \mathbb{D}$ korral:

\begin{columns}[onlytextwidth]
	\begin{column}{0.6\textwidth}
		%\paragraph{Osalise järjestuse omadused}
		\begin{itemize}[<2->]
			\item $a \sqleq a$
			\item kui $a \sqleq b$ ja $b \sqleq c$, siis $a \sqleq c$
			\item kui $a \sqleq b$ ja $b \sqleq a$, siis $a = b$
		\end{itemize}

		%\paragraph{Rajade omadused}
		\begin{itemize}[<3->]
			\item $a \sqleq a \sqcup b$ ja $b \sqleq a \sqcup b$
			\item $a \sqcap b \sqleq a$ ja $a \sqcap b \sqleq b$
			\item kui $a \sqleq c$ ja $b \sqleq c$, siis $a \sqcup b \sqleq c$
			\item kui $c \sqleq a$ ja $c \sqleq b$, siis $c \sqleq a \sqcap b$
		\end{itemize}
	\end{column}

	\begin{column}{0.4\textwidth}
		%\paragraph{Vähima ja suurima elemendi omadused}
		\begin{itemize}[<5->]
			\item $\bot \sqleq a$
			\item $a \sqleq \top$
			\item $a \sqcup \bot = a$
			\item $a \sqcap \top = a$
		\end{itemize}

		%\paragraph{Järjestuse ja rajade tehete seosed}
		\visible<6->{Samaväärsed:}
		\begin{enumerate}[<6->]
			\item $a \sqleq b$
			\item $a \sqcup b = b$
			\item $a \sqcap b = a$
		\end{enumerate}
	\end{column}
\end{columns}

%\paragraph{Rajade tehete omadused}
\begin{comment}
\begin{itemize}
	\item $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$ ja $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$
	\item $a \sqcup b = b \sqcup a$ ja $a \sqcap b = b \sqcap a$
	\item $a \sqcup a = a$ ja $a \sqcap a = a$
	\item $a \sqcup (a \sqcap b) = a$ ja $a \sqcap (a \sqcup b) = a$
\end{itemize}
\end{comment}
\begin{columns}[onlytextwidth]
	\begin{column}{0.5\textwidth}
		\begin{itemize}[<4->]
			\item $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$
			\item $a \sqcup b = b \sqcup a$
			\item $a \sqcup a = a$
			\item $a \sqcup (a \sqcap b) = a$
		\end{itemize}
	\end{column}
	\begin{column}{0.5\textwidth}
		\begin{itemize}[<4->]
			\item $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$
			\item $a \sqcap b = b \sqcap a$
			\item $a \sqcap a = a$
			\item $a \sqcap (a \sqcup b) = a$
		\end{itemize}
	\end{column}
\end{columns}
\end{frame}

\section{Analüsaator Goblint}
\begin{frame}{Omaduspõhine testimine ja analüsaator Goblint}
\begin{columns}[t]
	\begin{column}{0.5\textwidth}
		Omaduspõhine testimine:
		\begin{itemize}
			\item QuickCheck
			\item Hea matemaatiliste tingimuste kontrollimiseks
			\item Omadused --- predikaadid
			\item Generaatorid --- juhuslikud % TODO: juhuslikud pole sama analoogia järgi
		\end{itemize}
	\end{column}

	\pause
	\begin{column}{0.5\textwidth}
		Analüsaator Goblint:
		\begin{itemize}
			\item TÜ, TUM
			\item Mitmelõimelised C programmid
			\item Andmejooksud
			\item Kirjutatud OCaml-is
		\end{itemize}
	\end{column}
\end{columns}

\end{frame}

\begin{frame}[fragile]{Goblinti domeeni signatuur}
	\centering
	\begin{bminted}[mathescape]{ocaml}
		module type S =
		sig
		  type t (* domeeni elementide tüüp *)
		  val equal: t -> t -> bool (* seos $=$ *)
		  val leq: t -> t -> bool (* seos $\sqleq$ *)
		  val join: t -> t -> t (* tehe $\sqcup$ *)
		  val meet: t -> t -> t (* tehe $\sqcap$ *)
		  val bot: unit -> t (* element $\bot$ *)
		  val is_bot: t -> bool
		  val top: unit -> t (* element $\top$ *)
		  val is_top: t -> bool
		  val widen: t -> t -> t (* tehe $\widen$ *)
		  val narrow: t -> t -> t (* tehe $\narrow$ *)
		end
	\end{bminted}

\end{frame}

\begin{frame}[fragile]{Goblinti täiendamine}
\begin{itemize}
	\item Domeenidesse generaatorid:
	\begin{minted}{ocaml}
		val arbitrary: unit -> t QCheck.arbitrary
	\end{minted}

	\item Kõik omadused omaduspõhiste testidena
	\begin{itemize}
		\item Näiteks ülemraja kommutatiivsus ($a \sqcup b = b \sqcup a$):
		\begin{minted}{ocaml}
		let join_comm = make ~name:"join comm" (pair arb arb)
		      (fun (a, b) -> D.equal (D.join a b) (D.join b a))
		\end{minted}

		\item \texttt{D} testitav domeen
		\item \texttt{arb} selle generaator
	\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}[fragile]{QCheck'i väljund}
%\centering
\begin{Verbatim}[commandchars=\\\{\}]
generated error fail pass / total  time  test name
...
[\textcolor{green}{✓}]  300    0    0   10 /  100     0.0s trier: leq trans
[\textcolor{green}{✓}]  300    0    0    1 /  100     0.0s trier: leq antisym
[\textcolor{green}{✓}]  100    0    0  100 /  100     0.0s trier: join leq
[\textcolor{red}{✗}]    2    0    1    1 /  100     0.0s trier: join assoc
[\textcolor{green}{✓}]  100    0    0  100 /  100     0.0s trier: join comm
[\textcolor{green}{✓}]  100    0    0  100 /  100     0.0s trier: join idem
[\textcolor{green}{✓}]  100    0    0  100 /  100     0.0s trier: join abs
...
\end{Verbatim}
\begin{Verbatim}[commandchars=\\\{\}]
--- \textcolor{red}{Failure} --------------------------------------------------

Test trier: join assoc failed (91 shrink steps):

(0, 1, Not \{3\}([-63,63]))
\end{Verbatim}
\end{frame}

\section{Testimise tulemused}
\begin{frame}{Ülevaatlikud tulemused}
\begin{center}
	\begin{tabu}{cc|ccc}
	\hline
	& & \multicolumn{3}{c}{Testide arv} \\
	Lähenemine & Võrdlemine & Kokku & Erindi teke & Mittekehtivad \\
	\hline
	\multirow{2}{*}{Alt üles} & \texttt{equal} & 468 & \presim 35 & \presim 75 \\
	%\cline{2-5}
	& \texttt{leq} & 468 & \presim 35 & \presim 69 \\
	\hline
	\multirow{2}{*}{Ülalt alla} & \texttt{equal} & 27 & 0 & \presim 12 \\
	%\cline{2-5}
	& \texttt{leq} & 27 & 0 & \presim 12 \\
	\hline
	\end{tabu}
\end{center}

\vfill
\pause
Erindi tekkimise ja mittekehtimise põhjuseid:
\begin{enumerate}
	\item Viga domeeni implementeerimisel
	\item Mittekehtimine teoreetilisel tasandil
	\item Teadlik ja dokumenteeritud mittekehtimine
	\item Sõltumine teistest probleemsetest omadustest/domeenidest
\end{enumerate}
\end{frame}

\begin{frame}{Trieri domeen}
\begin{itemize}
	\item Goblintis vaikimisi kasutusel
	\item Elemendid:
	\begin{itemize}
		\item Üksikud täisarvud
		\item Välistatud täisarvude hulgad (\ingl{exclusion set})
	\end{itemize}

	\pause
	\item Mittekehtiv ülemraja assotsiatiivsus
	\[
		(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)
	\]
	näiteks argumentidel
	\[
		a = 0,\quad b = 1,\quad c = \texttt{Not \{3\}([-63,63])} % (0, 1, Not {3}([-63,63]))
	\]

	\item \alert{Viga domeeni disainis}
\end{itemize}
\end{frame}

\section{Kokkuvõte}
\begin{frame}{Kokkuvõte}
Tehtud:
\begin{itemize}
	\item Domeenide omaduste komplekt
	\item Goblinti täiendused: omadused ja generaatorid
	\item Goblinti domeenide testimine
	\item Tulemuste esmane analüüs
\end{itemize}

\vfill
\pause
\begin{block}{Järeldus}
	Omaduspõhist testimist on võimalik efektiivselt rakendada abstraktsetest domeenidest vigade leidmiseks.
\end{block}
\end{frame}

\begin{frame}
	\centering
	\Huge
	Aitäh!
\end{frame}

\appendix
\begin{frame}{Domeenide omadused (2)}
\begin{columns}[t]
	\begin{column}{0.4\textwidth}
		Programmianalüüsis:
		\begin{itemize}
			\item Laiendamise tehe $\widen$
			\begin{itemize}
				\item $a \sqcup b \sqleq a \widen b$
			\end{itemize}

			\item Kitsendamise tehe $\narrow$
			\begin{itemize}
				\item $a \sqcap b \sqleq a \narrow b \sqleq a$
			\end{itemize}
		\end{itemize}
	\end{column}

	\begin{column}{0.6\textwidth}
		Abstraktsiooni korrektsus:
		\begin{itemize}
			\item Abstraktsioonifunktsioon $\alpha: \mathbb{D}_1 \to \mathbb{D}_2$
			\item kui $a \sqleq b$, siis $\alpha(a) \sqleq \alpha(b)$
			\item $\alpha (f_1 (x_1)) \sqleq f_2 (\alpha (x_1))$
			\begin{itemize}
				\item $f_1$, $f_2$ vastavad monotoonsed tehted
			\end{itemize}
		\end{itemize}
	\end{column}
\end{columns}

\vfill
\centering
\begin{tikzpicture}[
	on grid
]
	\node (x1) {$x_1$};
	\node [right=4cm of x1] (f1x1) {$f_1(x_1)$};
	\node [below=2.5cm of x1] (ax1) {$\alpha(x_1)$};
	\node [right=4cm of ax1] (f2ax1) {$f_2(\alpha(x_1))$};
	\node [above=1cm of f2ax1] (af1x1) {$\alpha(f_1(x_1))$};

	\path[->]
		(x1) edge node [above] {$f_1$} (f1x1)
    edge node [left,pos=0.2] {$\alpha$} (ax1)
		(f1x1) edge node [right,pos=0.4] {$\alpha$} (af1x1)
		(ax1) edge node [below] {$f_2$} (f2ax1);
	\path (af1x1) -- (f2ax1) node [midway,sloped] {$\sqleq$};

	\path[draw=gray,dashed] ($(x1)+(-3cm,-0.9cm)$) to node [above,pos=0.05] {$\mathbb{D}_1$} node [below,pos=0.05] {$\mathbb{D}_2$} ($(f1x1)+(2cm,-0.9cm)$); % TODO better positioning
\end{tikzpicture}
\end{frame}

\begin{frame}{Testitud täisarvude domeenid Goblintis}
\centering
\begin{tikzpicture}[
	level distance=1.5cm,
	sibling distance=1.75cm,
	edge from parent/.style={draw,-latex},
	on grid=true
	%style={font=\ttfamily}
]
\node (IntDomTuple) {IntDomTuple}
	child { node {Trier}
		child { node {SetDomain}
			child { node (Integers) {Integers} }
		}
		child { node (Interval32) {Interval32} }
	}
	child { node {} edge from parent [draw=none] }
	child { node {CircInterval} }
	child { node (Enums) {Enums} };
\path[-latex] (IntDomTuple) edge (Interval32)
	(Enums) edge (Integers)
			edge (Interval32);
\node[above=3cm of Integers,xshift=-1.75cm] (Flattened) {Flattened}
	child { node (Flat) {Flat} };
\node[left=1.75cm of Flattened] (Lifted) {Lifted}
	child { node (Lift) {Lift} };
\path[-latex] (Flat) edge (Integers)
	(Lift) edge (Integers);
\node[below=3cm of Enums] (Booleans) {Booleans};
\end{tikzpicture}
\end{frame}

\end{document}