46 lines
4.3 KiB
TeX
46 lines
4.3 KiB
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.
|