\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 while \texttt{null}-checking is enforced, since, 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 of 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} is used to check whether node and its subtrees satisfy rank rules
    \item \texttt{\_insert\_rebalance} rebalances the tree from the given node after insertion
    \item \texttt{\_delete\_rebalance} rebalances the tree from the given nodes (deleted node and parent) after deletion
\end{enumerate}

Apart from the abstract methods there is provided 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} returns rank of the root of the tree
    \item \texttt{is\_correct} calls \texttt{is\_correct\_node} on the root of the tree
    \item \texttt{search} is used to look up keys in the tree
    \item \texttt{insert} implements generic insertion into the tree followed by a call to tree-specific rebalance function
    \item \texttt{delete} 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.

\section{Testing and validation}

From the beginning we have employed the techniques of property-based testing (done manually during C\# implementation and uses Hypothesis~\cite{hypothesis} for Python implementation). The elementary requirement for testing and validation of 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 also admit abuse of property-based testing to find a \textit{minimal} sequence of operations when WAVL tree relaxation manifests. 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. While trying to find minimal counter-example, we have also discovered a bug in rebalance after deletion of WAVL tree that caused enforcement of the AVL rank rules.