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

3552 软件学报 2025 年第 36 卷第 8 期

6 总结与展望

本文基于 Isabelle 定理证明器, 建立了动态顺序统计树类结构的函数式建模框架和自动验证框架. 在建模框架
中, 设计了动态顺序统计树类结构的通用结构, 建立了统一建模策略, 并刻画了其 10 种操作的高阶复合函数. 在自
动验证框架中, 构建了自动化验证的辅助引理库, 并给出了具体的验证方案, 以克服构造辅助引理时的盲目性. 基
于函数式建模框架, 可以在不同的具体搜索树结构中进行相应的实例化, 以适用不同的应用场景. 文中考虑了平衡
与不平衡、二叉与多叉两个维度, 选取了不平衡的二叉搜索树、红黑树和 2−3 树做为实例化的案例来展示, 并借
助自动化验证框架, 可自动验证多个实例化案例. 这为复杂数据结构算法功能和结构正确性的自动化验证提供了
参考.
在未来的工作中, 可以考虑将本文中的函数转化为更具可执行性和效率的编程语言, 如 Haskell 或 OCaml. 将
形式化方法的理论应用于实际问题, 将函数式程序建模及其验证投入实际的工业应用中, 探索其在实际应用中的
效果和优势, 使其能够达到工业级的要求.

References:
[1] Cormen TH, Leiserson CE, Rivest RL, Stein C. Introduction to Algorithms. 4th ed., Cambridge: MIT Press, 2022.
[2] Hopcroft JE, Ullman JD. Set merging algorithms. SIAM Journal on Computing, 1973, 2(4): 294–303. [doi: 10.1137/0202024]
[3] Fisher RA. Statistical methods for research workers. In: Kotz S, Johnson NL, eds. Breakthroughs in Statistics: Methodology and
Distribution. New York: Springer, 1992. 66–70. [doi: 10.1007/978-1-4612-4380-9_6]
[4] Ahsanullah M, Nevzorov VB, Shakil M. An Introduction to Order Statistics. Paris: Atlantis Press, 2013. [doi: 10.2991/978-94-91216-83-1]
[5] Nipkow T. Automatic functional correctness proofs for functional search trees. In: Proc. of the 7th Int’l Conf. on Interactive Theorem
Proving. Nancy: Springer, 2016. 307–322. [doi: 10.1007/978-3-319-43144-4_19]
[6] Nipkow T, Klein G. Concrete Semantics: With Isabelle/HOL. Cham: Springer, 2014. [doi: 10.1007/978-3-319-10542-0]
[7] Nipkow T, Paulson LC, Wenzel M. A Proof Assistant for Higher-order Logic. New York: Springer, 2021.
[8] Böhme S, Nipkow T. Sledgehammer: Judgement day. In: Proc. of the 5th Int’l Joint Conf. of Automated Reasoning. Edinburgh: Springer,
2010. 16–19 [doi: 10.1007/978-3-642-14203-1_9]
[9] Eberl M, Haslbeck MW, Nipkow T. Verified analysis of random binary tree structures. Journal of Automated Reasoning, 2020, 64(5):
879–910. [doi: 10.1007/s10817-020-09545-0]
[10] Nipkow T, Sewell T. Proof pearl: Braun trees. In: Proc. of the 9th ACM SIGPLAN Int’l Conf. on Certified Programs and Proofs. New
Orleans: ACM, 2020. 18–31. [doi: 10.1145/3372885.3373834]
[11] Nipkow T. Verified root-balanced trees. In: Proc. of the 15th Asian Symp. on Programming Languages and Systems. Suzhou: Springer,
2017. 255–272. [doi: 10.1007/978-3-319-71237-6_13]
[12] Nipkow T, Brinkop H. Amortized complexity verified. Journal of Automated Reasoning, 2019, 62(3): 367–391. [doi: 10.1007/s10817-
018-9459-3]
[13] Hinze R, Paterson R. Finger trees: A simple general-purpose data structure. Journal of Functional Programming, 2006, 16(2): 197–217.
[doi: 10.1017/S0956796805005769]
[14] Hirai Y, Yamamoto K. Balancing weight-balanced trees. Journal of Functional Programming, 2011, 21(3): 287–307. [doi: 10.1017/
S0956796811000104]
[15] Ammer T, Lammich P. van Emde boas trees. 2024. https://www.isa-afp.org/browser_info/current/AFP/Van_Emde_Boas_Trees/document.
pdf
[16] Zuo ZK, Huang ZP, Huang Q, Sun H, Zeng ZC, Hu Y, Wang CJ. Functional modeling and mechanized verification of LLRB algorithm.
Ruan Jian Xue Bao/Journal of Software, 2024, 35(11): 5016–5039 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/
7034.htm [doi: 10.13328/j.cnki.jos.007034]
[17] Zhao YW. Functional programming and proof. 2021 (in Chinese). https://www.yuque.com/zhaoyongwang/fpp/
[18] Back RJ. Invariant based programming: Basic approach and teaching experiences. Formal Aspects of Computing, 2009, 21(3): 227–244.
[doi: 10.1007/s00165-008-0070-y]
[19] Nipkow T. Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? In: Proc. of
the 4th Annual Symp. on Theoretical Aspects of Computer Science. Passau: Springer, 1987. 260–271. [doi: 10.1007/BFb0039611]
[20] Haftmann F, Krauss A, Kunčar O, Nipkow T. Data refinement in Isabelle/HOL. In: Proc. of the 4th Int’l Conf. of Interactive Theorem