IntervalTree+结构的函数式建模、机械化验证及其应用

左正康; 张晗庆; 王昌晶; 游珍

doi:10.12263/DZXB.20240427

您当前的位置：

首页 >

文章列表页 >

IntervalTree+结构的函数式建模、机械化验证及其应用

学术论文 | 更新时间：2025-12-08

- IntervalTree+结构的函数式建模、机械化验证及其应用
- Functional Modeling, Mechanized Verification and Application of IntervalTree+
- 电子学报 2025年53卷第2期页码：474-482
- 作者机构：
  
  1.江西师范大学计算机信息工程学院，江西南昌 330022
  2.江西师范大学网络化支撑软件国家科技合作基地，江西南昌 330022
  3.江西师范大学高性能计算江西省重点实验室，江西南昌 330022
- 作者简介：
  
  [ "左正康　男，1980年3月生于江西抚州.现为江西师范大学计算机信息工程学院教授、硕士生导师.主要研究方向为高可信与智能化软件." ]
  [ "张晗庆　男，2000年12月生于江西抚州.现为江西师范大学计算机信息工程学院硕士研究生.主要研究方向为形式化方法." ]
  [ "王昌晶　男，1977年10月生于江西丰城.现为江西师范大学计算机信息工程学院教授、博士生导师.主要研究方向为高可信软件，智能化软件." ]
  [ "游　珍　女，1982年6月生于江西高安.现为江西师范大学计算机信息工程学院副教授、硕士生导师.主要研究方向为形式化方法、分布式虚拟现实、并发分布式计算." ]
- 基金信息：
  
  国家自然科学基金(62462036;62462037);江西省自然科学基金(20242BAB26017;20232BAB202010);江西省主要学科学术与技术带头人培养项目(20232BCJ22013)
- DOI：10.12263/DZXB.20240427
  中图分类号： TP311
- 收稿：2024-05-09，
  
  修回：2025-01-13，
  
  纸质出版：2025-02-25
- 稿件说明：
移动端阅览
左正康, 张晗庆, 王昌晶, 等. IntervalTree+结构的函数式建模、机械化验证及其应用[J]. 电子学报, 2025, 53(02): 474-482.

ZUO Zheng-kang, ZHANG Han-qing, WANG Chang-jing, et al. Functional Modeling, Mechanized Verification and Application of IntervalTree+[J]. Acta Electronica Sinica, 2025, 53(02): 474-482.
左正康, 张晗庆, 王昌晶, 等. IntervalTree+结构的函数式建模、机械化验证及其应用[J]. 电子学报, 2025, 53(02): 474-482. DOI：10.12263/DZXB.20240427

ZUO Zheng-kang, ZHANG Han-qing, WANG Chang-jing, et al. Functional Modeling, Mechanized Verification and Application of IntervalTree+[J]. Acta Electronica Sinica, 2025, 53(02): 474-482. DOI：10.12263/DZXB.20240427

摘要

区间树（IntervalTree）是一种对动态集合进行维护的搜索树，可用于高效地存储和搜索区间集合.当前实现了IntervalTree在Isabelle/HOL的建模与验证，其区间信息是在二叉搜索树上进行扩充的，IntervalTree结构支持的基本操作时间复杂度较高.为此，本文对IntervalTree结构的节点附加额外颜色信息且保证树的平衡，提出了IntervalTree+结构，相较于IntervalTree结构的实现，插入和删除等操作最坏时间复杂度

（

）改进到

（log

）.然后使用Isabelle定理证明器对IntervalTree+结构及其操作函数进行了函数式建模，对其不变量进行了机械化验证，保证了IntervalTree+结构操作函数的正确性和可靠性.进一步，首次提出一种区域匹配算法的通用验证规约，旨在解决一系列的区域匹配算法正确性验证问题.提出的IntervalTree+结构通过严格的机械化验证，且操作最坏时间复杂度相较于IntervalTree结构由

（

）优化到

（log

），可应用于区域匹配、视觉日志和评估模型等相关算法优化.

Abstract

IntervalTree is a search tree used for maintaining dynamic sets

specifically designed for efficient storage and retrieval of interval collections. The current implementation of IntervalTree involves modeling and verification in Isabelle/HOL

where interval information is expanded upon a binary search tree. However

the time complexity of the basic operations supported by the IntervalTree structure is relatively high. To address this issue

this paper proposes the IntervalTree+ structure

augmenting nodes of the IntervalTree with additional color information to ensure tree balance. As compared to the original IntervalTree structure

the worst-case time complexity for operations such as insertion and deletion is improved from

(

) to

(log

) in the IntervalTree+ implementation. Subsequently

functional modeling of the IntervalTree+ structure and its operations is performed using the Isabelle theorem prover. Mechanical verification of invariants is conducted to ensure the correctness and reliability of IntervalTree+ structure operations. Additionally

for the first time

a generic verification specification for region matching algorithms is proposed to address correctness verification issues across a series of such algorithms. The proposed IntervalTree+ structure has been rigorously verified through formal mechanization. Compared to IntervalTree structure

its worst-case time complexity is optimized from

(

) to

(log

). This optimization makes it applicable to algorithmic enhancements in areas such as region matching

visual logging

and model evaluation.

关键词

Keywords

references

MEHTA D P , SAHNI S . Handbook of Data Structures and Applications [M ] . New York : Chapman and Hall/CRC , 2004 .

NIPKOW T , BLANCHETTE J , EBERL M . Functional algorithms, verified! [EB/OL ] . [ 2024-05-09 ] . https://functional-algorithms-verified.org https://functional-algorithms-verified.org .

GRAEFE G . B-tree indexes for high update rates [J ] . ACM Sigmod Record , 2006 , 35 ( 1 ): 39 - 44 .

GYTING R H , BEHR T . SECONDO: A platform for moving objects database research and for publishing and integrating research implementations [EB/OL ] . [ 2024-05-09 ] . https://secondodatabase.github.io/files/papers/PaperPlugin-s.pdf https://secondodatabase.github.io/files/papers/PaperPlugin-s.pdf .

KAUSHIK R , NAUGHTON J F , BOHANNON P , et al . Updates for structure indexes [C ] // VLDB'02: Proceedings of the 28th International Conference on Very Large Databases . Amsterdam : Elsevier , 2002 : 239 - 250 .

LEE M L , HSU W , JENSEN C S , et al . Supporting frequent updates in R-Trees: A bottom-up approach [C ] // Proceedings 2003 VLDB Conference . Amsterdam : Elsevier , 2003 : 608 - 619 .

XU J Q , WEI J H . Efficiently update disk-resident interval tree [C ] // Spatial Data and Intelligence . Cham : Springer International Publishing , 2021 : 198 - 207 .

PHAM V A , HOANG D H , CHUNG-NGUYEN H H , et al . Privacy preserving visual log service with temporal interval query using interval tree-based searchable symmetric encryption [C ] // Proceedings of the 10th International Symposium on Information and Communication Technology . New York : ACM , 2019 : 425 - 432 .

XIONG Z Y , WANG Y J . New document scoring model based on interval tree [J ] . Journal of Visual Languages & Computing , 2018 , 45 : 39 - 43 .

PAULSON L C , NIPKOW T , WENZEL M . From LCF to isabelle/HOL [J ] . Formal Aspects of Computing , 2019 , 31 ( 6 ): 675 - 698 .

赵永望 . 函数式程序设计与证明 [EB/OL ] . [ 2024-05-09 ] . https://www.yuque.com/zhaoyongwang/fpp/ https://www.yuque.com/zhaoyongwang/fpp/ .

CORMEN T H . Introduction to Algorithms [M ] . 4th edition . Cambridge : MIT Press , 2022 .

BERTINO E , ATZENI P , TAN K L , et al . Boosting the accuracy of differentially-private histograms through consistency [J ] . Proceedings of the VLDB Endowment , 2010 , 3 ( 1-2 ): 1021 - 1032 .

李丽 , 张琳 , 王汝传 . 基于动态区间树的差分隐私数据发布算法 [J ] . 南京邮电大学学报(自然科学版) , 2017 , 37 ( 4 ): 103 - 112 .

LI L , ZHANG L , WANG R C . Differential privacy data publishing algorithm based on dynamic interval tree [J ] . Journal of Nanjing University of Posts and Telecommunications (Na-tural Science Edition) , 2017 , 37 ( 4 ): 103 - 112 . (in Chinese)

DROUIN A , HOCKING TD , LAVIOLETTE F . Maximum margin interval trees [C ] // 31st Conference on Neural Information Processing Systems . New York : Curran Associates , 2017 : 4947 - 4956 .

ZHAN B H . Verifying imperative programs using Auto2 [EB/OL ] . [ 2024-05-09 ] . https://www.isa-afp.org/brow-ser_ info/current/AFP/Auto2_Imperative_HOL/document.pdf https://www.isa-afp.org/brow-ser_info/current/AFP/Auto2_Imperative_HOL/document.pdf .

左正康 , 黄志鹏 , 黄箐 , 等 . LLRB算法的函数式建模及其机械化验证 [J ] . 软件学报 , 2024 , 35 ( 11 ): 5016 - 5039 .

ZUO Z K , HUANG Z P , HUANG Q , et al . Functional modeling and mechanized verification of LLRB algorit-hm [J ] . Journal of Software , 2024 , 35 ( 11 ): 5016 - 5039 . (in Chinese)

左正康 , 柯雨含 , 黄箐 , 等 . Trie+结构函数式建模、机械化验证及其应用 [J ] . 软件学报 , 2024 , 35 ( 9 ): 4242 - 4264 .

ZUO Z K , KE Y H , HUANG Q , et al . Trie+ structural functional modeling, mechanized verification and application [J ] . Journal of Software , 2024 , 35 ( 9 ): 4242 - 4264 . (in Chinese)

BACK R J . Invariant based programming: Basic approach and teaching experiences [J ] . Formal Aspects of Computing , 2009 , 21 ( 3 ): 227 - 244 .

BOUKERCHE A , LU K Y . A novel approach to real-time RTI based distributed simulation system [C ] // 38th Annual Simulation Symposium . Piscataway : IEEE , 2005 : 267 - 274 .

AYANI R , MORADI F , TAN G . Optimizing cell-size in grid-based DDM [C ] // Proceedings Fourteenth Workshop on Parallel and Distributed Simulation . Piscataway : IEEE , 2000 : 93 - 100 .

PAN K , TURNER S J , CAI W T , et al . An efficient sort-based DDM matching algorithm for HLA applications with a large spatial environment [C ] // 21st International Workshop on Principles of Advanced and Distributed Simulation . Piscataway : IEEE , 2007 : 70 - 82 .

尚福华 , 张海波 , 解红涛 . 区间树在DDM区域匹配中的应用 [J ] . 计算机工程与应用 , 2013 , 49 ( 11 ): 110 - 113, 165 .

SHANG F H , ZHANG H B , XIE H T . Application of interval-tree in region matching for DDM [J ] . Computer Engineering and Applications , 2013 , 49 ( 11 ): 110 - 113, 165 . (in Chinese)

王磊 , 张慧慧 , 李开生 , 等 . 基于动态R-树结构的DDM区域匹配算法 [J ] . 计算机工程 , 2008 , 34 ( 3 ): 56 - 58 .

WANG L , ZHANG H H , LI K S , et al . Region matching algorithm for DDM based on dynamic R-tree [J ] . Computer Engineering , 2008 , 34 ( 3 ): 56 - 58 . (in Chinese)

NIPKOW T . Automatic functional correctness proofs for functional search trees [C ] // International Conference on Interactive Theorem Proving . Cham : Springer International Publishing , 2016 : 307 - 322 .

HAFTMANN F , BULWAHN L , NIPKOW T . Code generation from Isabelle/HOL theories [EB/OL ] . [ 2024-05-09 ] . https://isabelle.in.tum.de/dist/Isabelle2023/doc/ codegen.pdf https://isabelle.in.tum.de/dist/Isabelle2023/doc/codegen.pdf .

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

暂无数据