Page 130 - 《软件学报》2025年第8期

左正康 等: 动态顺序统计树类结构的函数式建模及其自动化验证 3553

Proving. Rennes: Springer, 2013. 100–115. [doi: 10.1007/978-3-642-39634-2_10]
[21] Bayer R. Symmetric binary B-trees: Data structure and maintenance algorithms. Acta Informatica, 1972, 1(4): 290–306. [doi: 10.1007/
BF00289509]
[22] Guibas LJ, Sedgewick R. A dichromatic framework for balanced trees. In: Proc. of the 19th Annual Symp. on Foundations of Computer
Science. Ann Arbor: IEEE, 1978. 8–21. [doi: 10.1109/SFCS.1978.3]
[23] Mündler N, Nipkow T. A verified implementation of B+-trees in Isabelle/HOL. In: Proc. of the 19th Int’l Colloquium on Theoretical
Aspects of Computing. Tbilisi: Springer, 2022. 324–341. [doi: 10.1007/978-3-031-17715-6_21]

附中文参考文献:
[16] 左正康, 黄志鹏, 黄箐, 孙欢, 曾志城, 胡颖, 王昌晶. LLRB 算法的函数式建模及其机械化验证. 软件学报, 2024, 35(11): 5016–5039.
http://www.jos.org.cn/1000-9825/7034.htm [doi: 10.13328/j.cnki.jos.007034]
[17] 赵永望. 函数式程序设计与证明. 2021. https://www.yuque.com/zhaoyongwang/fpp/

左正康(1980－), 男, 博士, 教授, CCF 高级会员, 游珍(1982－), 女, 博士, 副教授, CCF 高级会员,
主要研究领域为形式化方法, 智能化软件. 主要研究领域为形式化方法, 分布式虚拟现实,
并发分布式计算.

刘增鑫(1999－), 男, 硕士生, CCF 学生会员, 主 王昌晶(1977－), 男, 博士, 教授, 博士生导师,
要研究领域为定理证明, 形式化方法. CCF 高级会员, 主要研究领域为高可信软件, 智
能化软件.

柯雨含(1998－), 男, 硕士生, 主要研究领域为定
理证明, 形式化方法.