软件学报

作者：左正康，柯雨含，黄箐，王玥坤，曾志城，王昌晶

单位：左正康，江西师范大学 计算机信息工程学院, 江西 南昌 33002211,柯雨含，江西师范大学 计算机信息工程学院, 江西 南昌 33002202,黄箐，江西师范大学 计算机信息工程学院, 江西 南昌 33002203,王玥坤，江西师范大学 计算机信息工程学院, 江西 南昌 33002204,曾志城，江西师范大学 计算机信息工程学院, 江西 南昌 33002205,王昌晶，江西师范大学 计算机信息工程学院, 江西 南昌 33002206

关键词：Trie+;函数式建模;机械化验证;多模式匹配算法

基金：国家自然科学基金(62262031); 江西省自然科学基金(20232BAB202010); 江西省教育厅科技重点项目(GJJ210307, GJJ2200302); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013)

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

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期