thesis/implementation.tex

\chapter{Implementation}

For the implementation of 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 a \texttt{null} after checking specific set of conditions that forbid such 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. 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 following interface that is either shared by the specific trees or used by them:
\begin{enumerate}
    \item \texttt{\_get\_unwrapped\_graph} that is used to generate DOT format of the tree for purpose of either debugging or sharing.
    \item \texttt{rank}, which returns rank of the root of the tree.
    \item \texttt{is\_correct}, which calls \texttt{is\_correct\_node} on the root of the tree.
    \item \texttt{search} that is used to look up 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 class for representation of nodes that provides quite rich interface that is utilized during rebalancing and also in generic methods on 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 validation of the implemented algorithms was a \textbf{correct} \texttt{is\_correct\_node} method that validates properties of a specific rank-balanced tree and a good set of invariants. List of set invariants follows:
\begin{enumerate}
    \item for insertion we have set 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 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 rudimentary \texttt{insert} and \texttt{delete} interface enriched with \texttt{are\_same} (evaluates isomorphism and ranks) and \texttt{are\_similar} (evaluates just isomorphism) methods.