Affordable Access

Publisher Website

Reasoning about B+ Trees with Operational Semantics and Separation Logic

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
218
Identifiers
DOI: 10.1016/j.entcs.2008.10.021
Keywords
  • B+ Trees
  • Separation Logic
  • Abstract Machines
  • Data Structure
  • Invariant
Disciplines
  • Computer Science
  • Linguistics

Abstract

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.