论文标题
在Isabelle/HOL中验证的B+树的实现
A Verified Implementation of B+-Trees in Isabelle/HOL
论文作者
论文摘要
在本文中，我们介绍了在交互式定理供剂iSabelle/hol中无处不在的B+树数据结构的命令验证。该实现支持会员资格测试，插入和范围查询，并通过有效的二进制搜索节点导航。命令性实现将通过两个步骤进行验证：抽象集接口将完善到可执行但效力低下的纯粹功能实现，这进一步完善了有效的命令实现。
In this paper we present the verification of an imperative implementation of the ubiquitous B+-tree data structure in the interactive theorem prover Isabelle/HOL. The implementation supports membership test, insertion and range queries with efficient binary search for intra-node navigation. The imperative implementation is verified in two steps: an abstract set interface is refined to an executable but inefficient purely functional implementation which is further refined to the efficient imperative implementation.
