| 摘要: |
| Trie结构是一种使用搜索关键字来组织信息的搜索树, 可用于高效地存储和搜索字符串集合. Nipkow等人给出了实现Trie的Isabelle建模与验证, 然而其Trie在存储和操作时存在大量的冗余, 导致空间利用率不高, 且仅考虑英文单模式下查找. 为此, 基于索引即键值的思想提出了Trie+结构, 相较于传统的索引与键值分开存储的结构能减少50%的存储空间, 大大提高了空间利用率. 并且, 对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证, 保证操作的正确性和可靠性. 进一步, 提出一种匹配算法的通用验证规约, 旨在解决一系列的匹配算法正确性验证问题. 最后, 基于Trie+结构与匹配算法通用验证规约, 建模和验证了函数式中英文混合多模式匹配算法, 发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug. 该Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中, 有一定的理论和应用价值. |
| 关键词: Trie+ 函数式建模 机械化验证 多模式匹配算法 |
| DOI：10.13328/j.cnki.jos.007135 |
| 分类号: |
| 基金项目:国家自然科学基金(62262031); 江西省自然科学基金(20232BAB202010); 江西省教育厅科技重点项目(GJJ210307, GJJ2200302); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013) |
|
| Trie+ Structural Functional Modeling, Mechanized Verification and Application |
|
ZUO Zheng-Kang, KE Yu-Han, HUANG Qing, WANG Yue-Kun, ZENG Zhi-Cheng, WANG Chang-Jing
|
|
School of Computer and Information Engineering, Jiangxi Normal University, Nanchang 330022, China
|
| Abstract: |
| A Trie structure is a type of search tree that organizes information by search keywords and can be employed to efficiently store and search a collection of strings. Meanwhile, Nipkow et al. provided Isabelle modeling and verification for Trie implementation. However, there is a significant amount of redundancy in the Trie’s storage and operation, resulting in poor space utilization, and only the English single-mode lookup is considered. Therefore, based on the idea that the index is the key value, this study proposes the Trie+ structure, which can reduce storage space by 50% compared to the traditional structure of storing the index and key value separately, and greatly improve space utilization. Furthermore, the Trie+ structure’s lookup, insertion, and deletion operations are modeled as functions and rigorously mechanized to ensure their correctness and reliability. Additionally, a generalized verification protocol for matching algorithms is proposed to solve the correctness verification and problems of a series of matching algorithms. Finally, a functional Chinese-English hybrid multi-pattern matching algorithm is modeled and verified by the Trie+ structure and the matching algorithm’s universal verification protocol, and the Bug of prefix termination of pattern strings in multi-pattern matching algorithms of existing research based on the full hash Trie is discovered and solved. The proposed Trie+ structure and verification protocol have theoretical and application significance in improving the space utilization of the Trie structure and verifying the matching algorithm. |
| Key words: Trie+ functional modeling mechanized verification multi-pattern matching algorithm |
