Sciweavers

Share
ENTCS
2008

Reasoning about B+ Trees with Operational Semantics and Separation Logic

8 years 3 months ago
Reasoning about B+ Trees with Operational Semantics and Separation Logic
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, orm 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 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 a...
Alan P. Sexton, Hayo Thielecke
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Alan P. Sexton, Hayo Thielecke
Comments (0)
books