Affordable Access

Publisher Website

Reasoning about B+ Trees with Operational Semantics and Separation Logic

Electronic Notes in Theoretical Computer Science
Publication Date
DOI: 10.1016/j.entcs.2008.10.021
  • B+ Trees
  • Separation Logic
  • Abstract Machines
  • Data Structure
  • Invariant
  • Computer Science
  • Linguistics


Abstract The B+ tree is an ordered tree structure with a fringe list. It is the most widely used data structure for data organisation and searching in database systems specifically, and, probably, computing in general. In this paper, we apply two techniques from programming language theory to B+ trees: operational semantics, in the form of an abstract machine, and separation logic. We use an abstract machine to give a precise and tractable formalisation of the operations on B+ trees. Separation logic is then used to formalise a data structure invariant for B+ trees and to establish correctness by showing that the invariant is preserved by the operations. As usual in separation logic, a frame property is essential for keeping the reasoning local. In our setting, that means that we concentrate on the subtree reached from the top of the stack of the abstract machine, while the remainder of the B+ tree stays invariant. A particularly attractive feature of this approach is the smooth way that proofs can cope with algorithms that begin with a tree descent and switch to fringe list traversal.

There are no comments yet on this publication. Be the first to share your thoughts.