thesis/implementation.tex

\chapter{Implementation}

To implement rank-balanced trees, we have used two programming languages: C\# and Python. C\# implementation has not been finished and therefore is not part of the submitted attachments. However, it has given a valuable insight into the role of preconditions and invariants in algorithms when \texttt{null}-checking is enforced. For example, static type control cannot be aware of a node \textbf{not} being \texttt{null} after checking a specific set of conditions that forbid such a scenario.

Python has been chosen as the \textit{go-to} language since it is used for teaching foundations of programming~\cite{ib111} and also introductory course to algorithms and data structures~\cite{ib002} at our faculty.

We have started by implementing a general idea of a rank-balanced tree. The rank-balanced tree is an abstract class that \textbf{does not} implement methods specific to different kinds of trees, such as:
\begin{enumerate}
    \item \texttt{is\_correct\_node} that is used to check whether node and its subtrees satisfy rank rules.
    \item \texttt{\_insert\_rebalance} that rebalances the tree from the given node after insertion.
    \item \texttt{\_delete\_rebalance} that rebalances the tree from the given nodes (deleted node and parent) after deletion.
\end{enumerate}

Apart from the abstract methods, \texttt{RankedTree} provides the following interface that is either shared by the specific trees or used by them:
\begin{enumerate}
    \item \texttt{\_get\_unwrapped\_graph}, which is used to generate the tree's DOT format for either debugging or sharing.
    \item \texttt{rank}, which returns the rank of the tree's root.
    \item \texttt{is\_correct}, which calls \texttt{is\_correct\_node} on the root of the tree.
    \item \texttt{search} that is used to lookup keys in the tree.
    \item \texttt{insert}, which implements generic insertion into the tree followed by a call to tree-specific rebalance function.
    \item \texttt{delete}, which is identical to \texttt{insert}, but for the deletion from the tree.
\end{enumerate}

Apart from that, we have also implemented a class for the representation of nodes that provides quite a rich interface that is utilized during rebalancing and also in generic methods on the generic tree.

Implementation includes AVL (as described by \textit{Adelson-Velskij and Landis}~\cite{avl}), WAVL (as described by \textit{Haeupler et al.}~\cite{wavl}) and rAVL (as described by \textit{Sen et al.}~\cite{ravl}).

\section{Testing and validation}~\label{chap:testing}

From the beginning, we have employed the techniques of property-based testing (done manually during the C\# implementation and via Hypothesis~\cite{hypothesis} for the Python implementation). The elementary requirement for testing and validating the implemented algorithms was a \textbf{correct} \texttt{is\_correct\_node} method that validates the properties of a specific rank-balanced tree and a good set of invariants. The list of set invariants follows:
\begin{enumerate}
    \item for insertion, we have set the following invariants
        \begin{itemize}
            \item Rank rules have not been broken after the insertion.
            \item Inserted value can be found in the tree after the insertion.
            \item All previously inserted values can still be found in the tree.
        \end{itemize}
    \item for deletion, we have set the following invariants
        \begin{itemize}
            \item Rank rules have not been broken after the deletion.
            \item Deleted node can no longer be found in the tree after the deletion.
            \item All other values can still be found in the tree.
        \end{itemize}
\end{enumerate}

We have also used property-based testing to find a \textit{minimal} sequence of operations when WAVL tree relaxation manifests.~\footnote{While trying to find minimal counter-example, we have also discovered a bug in rebalance after deletion in the WAVL tree that caused enforcement of the AVL rank rule.} For that purpose, we have implemented a \textit{comparator} class that takes two different instances of rank-balanced trees and provides a rudimentary \texttt{insert} and \texttt{delete} interface enriched with \texttt{are\_same} (evaluates isomorphism and ranks) and \texttt{are\_similar} (evaluates just isomorphism) methods.