sample text for example

report/src/figures/simple_graph_example.tex

@@ -12,18 +12,18 @@
     \node [circle, draw] (qt6) at (1.7,-8.4) {$q_{t6}$};
     \node [circle, draw] (end) at (-1.7,-8.4) {$q_\blackpointerleft$};
 
-    \draw (qd) edge[bend left] node[above]{$I_5$} (q0);
-    \draw (q0) edge[bend left] node[above]{$I_4$} (qd);
-    \draw (qi) edge[bend left] node[above]{$I_1;I_2$} (q0);
-    \draw (q0) edge[bend left] node[above]{$I_3$} (qi);
+    \draw [arrow, ->](qd) edge[bend left] node[above]{$I_5$} (q0);
+    \draw [arrow, ->](q0) edge[bend left] node[above]{$I_4$} (qd);
+    \draw [arrow, ->](qi) edge[bend left] node[above]{$I_1;I_2$} (q0);
+    \draw [arrow, ->](q0) edge[bend left] node[above]{$I_3$} (qi);
 
-    \draw(q0) -- node[right, yshift=-17]{$I_6;I_7;I_8$} (qt1);
-    \draw(qt1) -- node[right]{$I_9$} (qt2);
-    \draw(qt2) -- node[right]{$I_{10}$} (qt3);
-    \draw(qt3) -- node[left, xshift=2, yshift=5]{b} (qt4);
-    \draw(qt3) -- node[right, xshift=-5, yshift=5]{$\neg$b} (qt5);
-    \draw(qt5) -- node[left]{$I_{11}$} (qt6);
+    \draw [arrow, ->](q0) -- node[right, yshift=-17]{$I_6;I_7;I_8$} (qt1);
+    \draw [arrow, ->](qt1) -- node[right]{$I_9$} (qt2);
+    \draw [arrow, ->](qt2) -- node[right]{$I_{10}$} (qt3);
+    \draw [arrow, ->](qt3) -- node[left, xshift=2, yshift=5]{b} (qt4);
+    \draw [arrow, ->](qt3) -- node[right, xshift=-5, yshift=5]{$\neg$b} (qt5);
+    \draw [arrow, ->](qt5) -- node[left]{$I_{11}$} (qt6);
 
-    \draw (qt4) edge[bend left] node[right]{skip} (q0);
-    \draw (qt6) edge[bend right] node[right]{$I_{12}$} (q0);
+    \draw [arrow, ->](qt4) edge[bend left] node[right]{skip} (q0);
+    \draw [arrow, ->](qt6) edge[bend right] node[right]{$I_{12}$} (q0);
 \end{tikzpicture}

report/src/sections/04-theory/07-example.tex

@@ -1,109 +1,3 @@
-\section{Example}\label{sec:example}
+\section{Examples}\label{sec:example}
 
-\begin{align}\label{eq:exaple equation}
-    \begin{split}
-    A(q_\whitepointerright)=A(q_\whitepointerright) &\cup \hat E_\whitepointerright \\&\cup \mathcal{\hat S} \lBrack skip \rBrack(A(q_{t4}))\\&\cup \mathcal{\hat S} \lBrack I_{12} \rBrack (A(q_{t6})) \\&\cup \mathcal{\hat S} \lBrack I_3 \rBrack (A(q_i)) \\&\cup \mathcal{\hat S} \lBrack I_5 \rBrack (A(q_d))
-    \end{split}\\
-    A(q_i)=A(q_i)&\cup \mathcal{\hat S} \lBrack I_1;I_2 \rBrack (A(q_\whitepointerright ))\\
-    A(q_d)=A(q_d)&\cup \mathcal{\hat S} \lBrack I_4 \rBrack (A(q_\whitepointerright ))\\
-    A(q_{t1})=A(q_{t1})&\cup \mathcal{\hat S} \lBrack I_6;I_7;I_8 \rBrack (A(q_\whitepointerright))\\
-    A(q_{t2})=A(q_{t2})&\cup \mathcal{\hat S} \lBrack I_9 \rBrack (A(q_{t1}))\\
-    A(q_{t3})=A(q_{t3})&\cup \mathcal{\hat S} \lBrack I_{10} \rBrack (A(q_{t2}))\\
-    A(q_{t4})=A(q_{t4})&\cup \mathcal{\hat S} \lBrack b \rBrack (A(q_{t3}))\\
-    A(q_{t5})=A(q_{t5})&\cup \mathcal{\hat S} \lBrack \neg b \rBrack (A(q_{t3}))\\
-    A(q_{t6})=A(q_{t6})&\cup \mathcal{\hat S} \lBrack I_{11} \rBrack (A(q_{t5}))\\
-    A(q_\blackpointerleft)=A(q_\blackpointerleft)
-\end{align}
-
-\begin{figure}
-    \begin{minted}[frame=lines, linenos, escapeinside=||, mathescape=true]{text}
-while true do(
-    vName := [A-Z][a-z]* [A-Z][a-z]*;
-    vBalance := |$\top$|;
-    (Insert(account, <Name, Balance>, <vName, vBalance>), true)
-)[](
-    vName := |$\top$|;
-    (delete(account), name = vName)
-)[](
-    vName := [A-Z][a-z]* [A-Z][a-z]*;
-    toName := [A-Z][a-z]* [A-Z][a-z]*;
-    amount := [0,+|$\infty$|];
-    (select (vBalance, account, <name>), name = vName)
-    (select (toBalance, account, <name>), name = toName)
-    if(vBalance - amount) < 0
-        then skip
-    else(
-        (update(account, <balance>, <vBalance - amount>), name = vName);
-        (update(account, <balance>, <toBalance + amount>), name = toName);
-    )
-)
-    \end{minted}
-    \caption{Code for the program example}
-    \label{fig:program-code}
-\end{figure}
-
-\begin{align}
-    \begin{split}
-    vName := [A-Z][a-z]* [A-Z][a-z]*;
-    \end{split}
-    & I_1\\
-    \begin{split}
-        vBalance := \top; 
-    \end{split}
-    & I_2\\
-    \begin{split}
-        &(Insert(account, <Name, Balance>, \\
-        &<vName, vBalance>), true)
-    \end{split} 
-    & I_3\\
-    \begin{split}
-        vName := \top;
-    \end{split} 
-    & I_4\\
-    \begin{split}
-        (delete(account), name = vName)
-    \end{split} 
-    & I_5\\
-    \begin{split}
-        vName := [A-Z][a-z]* [A-Z][a-z]*;
-    \end{split} 
-    & I_6\\
-    \begin{split}
-        toName := [A-Z][a-z]* [A-Z][a-z]*;
-    \end{split} 
-    & I_7\\
-    \begin{split}
-        amount := [0,+ \infty];
-    \end{split} 
-    & I_8\\
-    \begin{split}
-        &(select (vBalance, account, <name>), \\
-        &name = vName)
-    \end{split} 
-    & I_9\\
-    \begin{split}
-        &(select (toBalance, account, <name>), \\
-        &name = toName)
-    \end{split} 
-    & I_{10}\\
-    \begin{split}
-        &(update(account, <balance>, \\
-        &<vBalance - amount>), name = vName);
-    \end{split} 
-    & I_{11}\\
-    \begin{split}
-        &(update(account, <balance>, \\
-        &<toBalance + vBalance>), name = toName);
-    \end{split}
-    & I_{12}
-\end{align}
-
-
-% \begin{align}
-%     \begin{split}
-%         vName := [A-Z][a-z]* [A-Z][a-z]*;
-%     \end{split}
-%     & I_1\\
-% \end{align}
-
-\input{sections/04-theory/example-equations}
+\input{sections/04-theory/07.1-big-example}

report/src/sections/04-theory/07.1-big-example.tex

@@ -0,0 +1,133 @@
+\subsection{Big Example}\label{subsec:big-example}
+This section will present an example of a program that can be analyzed using the abstract interpretation presented in this paper.
+
+The program in~\autoref{fig:program-code} is a simple program that simulates a bank system With delete, input, select, and update operations.
+\begin{figure}
+    \begin{minted}[frame=lines, linenos, escapeinside=||, mathescape=true]{text}
+while true do(
+    vName := [A-Z][a-z]* [A-Z][a-z]*;
+    vBalance := |$\top$|;
+    (Insert(account, <Name, Balance>, <vName, vBalance>), true)
+)[](
+    vName := |$\top$|;
+    (delete(account), name = vName)
+)[](
+    vName := [A-Z][a-z]* [A-Z][a-z]*;
+    toName := [A-Z][a-z]* [A-Z][a-z]*;
+    amount := [0,+|$\infty$|];
+    (select (vBalance, account, <name>), name = vName)
+    (select (toBalance, account, <name>), name = toName)
+    if(vBalance - amount) < 0
+        then skip
+    else(
+        (update(account, <balance>, <vBalance - amount>), name = vName);
+        (update(account, <balance>, <toBalance + amount>), name = toName);
+    )
+)
+    \end{minted}
+    \caption{Code for the program example}
+    \label{fig:program-code}
+\end{figure}
+
+The program in~\autoref{fig:program-code} can be broken up into the following set of instructions, seen in~\autoref{eq:example-instructions-1} through~\autoref{eq:example-instructions-12}.
+
+\begin{align} \label{eq:example-instructions-1}
+    \begin{split}
+    vName := [A-Z][a-z]* [A-Z][a-z]*;
+    \end{split}
+    & I_1\\
+    \begin{split}
+        vBalance := \top; 
+    \end{split}
+    & I_2\\
+    \begin{split}
+        &(Insert(account, <Name, Balance>, \\
+        &<vName, vBalance>), true)
+    \end{split} 
+    & I_3\\
+    \begin{split}
+        vName := \top;
+    \end{split} 
+    & I_4\\
+    \begin{split}
+        (delete(account), name = vName)
+    \end{split} 
+    & I_5\\
+    \begin{split}
+        vName := [A-Z][a-z]* [A-Z][a-z]*;
+    \end{split} 
+    & I_6\\
+    \begin{split}
+        toName := [A-Z][a-z]* [A-Z][a-z]*;
+    \end{split} 
+    & I_7\\
+    \begin{split}
+        amount := [0,+ \infty];
+    \end{split} 
+    & I_8\\
+    \begin{split}
+        &(select (vBalance, account, <name>), \\
+        &name = vName)
+    \end{split} 
+    & I_9\\
+    \begin{split}
+        &(select (toBalance, account, <name>), \\
+        &name = toName)
+    \end{split} 
+    & I_{10}\\
+    \begin{split}
+        &(update(account, <balance>, \\
+        &<vBalance - amount>), name = vName);
+    \end{split} 
+    & I_{11}\\
+    \begin{split}
+        \label{eq:example-instructions-12}
+        &(update(account, <balance>, \\
+        &<toBalance + vBalance>), name = toName);
+    \end{split}
+    & I_{12}
+\end{align}
+
+A program graph, seen in~\autoref{fig:full-graph-example} is then made from the program in~\autoref{fig:program-code} using the abstract interpretation.
+
+\begin{figure}
+    \centering
+    \input{figures/graph_example.tex}
+    \caption[short]{Full program graph example}
+    \label{fig:full-graph-example}
+\end{figure}
+
+
+The program graph can then be simplified to the following program graph~\autoref{fig:simple-graph-example}.
+
+\begin{figure}
+    \centering
+    \input{figures/simple_graph_example.tex}
+    \caption[short]{Simple program graph example}
+    \label{fig:simple-graph-example}
+\end{figure}
+
+From the states of the program graph we get the following equations~\autoref{eq:example-equation-1} through~\autoref{eq:example-equation-12}.
+
+\begin{align}
+    \begin{split} \label{eq:example-equation-1}
+        A(q_\whitepointerright)=A(q_\whitepointerright) &\cup \hat E_\whitepointerright \\&\cup \mathcal{\hat S} \lBrack skip \rBrack(A(q_{t4}))\\&\cup \mathcal{\hat S} \lBrack I_{12} \rBrack (A(q_{t6})) \\&\cup \mathcal{\hat S} \lBrack I_3 \rBrack (A(q_i)) \\&\cup \mathcal{\hat S} \lBrack I_5 \rBrack (A(q_d))
+    \end{split}\\
+    A(q_i)=A(q_i)&\cup \mathcal{\hat S} \lBrack I_1;I_2 \rBrack (A(q_\whitepointerright ))\\
+    A(q_d)=A(q_d)&\cup \mathcal{\hat S} \lBrack I_4 \rBrack (A(q_\whitepointerright ))\\
+    A(q_{t1})=A(q_{t1})&\cup \mathcal{\hat S} \lBrack I_6;I_7;I_8 \rBrack (A(q_\whitepointerright))\\
+    A(q_{t2})=A(q_{t2})&\cup \mathcal{\hat S} \lBrack I_9 \rBrack (A(q_{t1}))\\
+    A(q_{t3})=A(q_{t3})&\cup \mathcal{\hat S} \lBrack I_{10} \rBrack (A(q_{t2}))\\
+    A(q_{t4})=A(q_{t4})&\cup \mathcal{\hat S} \lBrack b \rBrack (A(q_{t3}))\\
+    A(q_{t5})=A(q_{t5})&\cup \mathcal{\hat S} \lBrack \neg b \rBrack (A(q_{t3}))\\
+    A(q_{t6})=A(q_{t6})&\cup \mathcal{\hat S} \lBrack I_{11} \rBrack (A(q_{t5}))\\
+    A(q_\blackpointerleft)=A(q_\blackpointerleft) \label{eq:example-equation-12}
+\end{align}
+
+When solving the equations seen in~\autoref{eq:example-equation-1} through ~\autoref{eq:example-equation-12} using the semantics in this paper, we get the following fixpoint~\autoref{eq:example-fixed-point-1} through~\autoref{eq:example-fixed-point-7}.
+
+\input{sections/04-theory/example-equations}
+
+By using this, it is possible to analyze the program and check for some requested properties.
+In this case one of the properties could be to check if it is possible to have accounts with a negative balance, which in this case would be possible.
+Another case could be checking if it is possible to have accounts with names that are not in the format of the regular expression $[A-Z][a-z]* [A-Z][a-z]*$, which in this case would hold.

report/src/sections/04-theory/example-equations.tex

@@ -1,5 +1,5 @@
-Fixed point:
 \begin{align}
+    \label{eq:example-fixed-point-1}
     A(q_{\whitepointerright})=
     \begin{split}
         &\left\{\begin{matrix}
@@ -277,6 +277,7 @@
 \end{align}
 
 \begin{align}
+    \label{eq:example-fixed-point-7}
     A(q_{t_5})=\left\{\begin{matrix}
                           \left.\begin{matrix*}[l]
                                     \texttt{vName}\\

report/src/sections/09-acknowledgements.tex

@@ -1,4 +1,4 @@
 \section{Acknowledgements}\label{sec:acknowledgements}
 We want to express our sincere gratitude to our supervisor Gabriella Montoya for her invaluable supervision and guidance throughout this project.
 
-Also, we acknowledge that AI tools, namely Bing AI, GitHub Copilot, ChatGPT, and Grammarly, have been used as an aid to produce this paper by helping with thing like revision of the paper and speeding up the production of latex code.
+Also, we acknowledge that AI tools, namely Bing AI, GitHub Copilot, ChatGPT, and Grammarly, have been used as an aid to produce this paper by helping with things like revision of the paper and speeding up the production of latex code.