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

Trie+Structural Functional Modeling,Mechanized Verification and Application

Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基于索引即键值的思想提出了Trie+结构,相较于传统的索引与键值分开存储的结构能减少50%的存储空间,大大提高了空间利用率.并且,对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证,保证操作的正确性和可靠性.进一步,提出一种匹配算法的通用验证规约,旨在解决一系列的匹配算法正确性验证问题.最后,基于Trie+结构与匹配算法通用验证规约,建模和验证了函数式中英文混合多模式匹配算法,发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug.该Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中,有一定的理论和应用价值.

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.