THE SPECIFICATION OF ABSTRACT MAPPINGS AND THEIR IMPLEMENTATION AS B+ TREES
Elizabeth Fielding
Abstract
Cliff Jones's rigorous approach to software development is used to develop an implementation of a type of B-tree as a structure for storing mappings from keys to data. A B-tree is a generalised binary tree, for which there exist algorithms for inserting and deleting keys while keeping the tree balanced. The particular type of B-tree specified, known as a B+ tree, was chosen because it allows random access to any key as well as sequential access to keys; this is possible because all keys reside in the nodes. An abstract specification is given of a mapping from keys to data; then a development follows in which the specification is successively refined into more and more concrete forms. Each refinement stage is shown to be a correct implementation of the preceeding stage. The final stage is Pascal code, including assertions as annotations.