The Theory and Verification of B+ Tree Cursor Relations

Abstract

In this thesis, I make progress toward a fully verified functional B+ tree program in the Coq proof assistant. A verified functional B+ tree would serve as the basis for the future verification of an imperative B+ tree program through proving equivalence, which would have applications in databases and other systems. The primary focus of the properties and abstractions covered in this thesis is to examine and describe the theory of the B+ tree cursor, which is central to the operations of a B+ tree both functionally and imperatively. The functional implementation presented here covers the essential cursor operations as well as B+ tree lookups and insertions, but does not include a delete function. The progress made toward verification includes the development of a complete abstract specification, the structural correctness of cursor creation and positioning, and the relation of cursors and B+\,tree operations to an element-list abstract cursor representation.