Isabelle/HOL 中 B+ 树的验证实现
计算机科学中的逻辑
2022-08-22 v1 数据结构与算法
摘要
本文介绍了在交互式定理证明器 Isabelle/HOL 中对 ubiquitous B+ 树数据结构的一种命令式实现的验证。该实现支持成员测试、插入和范围查询，并在节点内导航中使用高效的二分搜索。该命令式实现的验证分两步进行：首先将抽象集合接口精化为一个可执行但低效的纯函数式实现，进而将其进一步精化为高效的命令式实现。
引用
@article{arxiv.2208.09066,
title = {A Verified Implementation of B+-Trees in Isabelle/HOL},
author = {Niels Mündler and Tobias Nipkow},
journal= {arXiv preprint arXiv:2208.09066},
year = {2022}
}
备注
Submitted at ICTAC 2022