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

摘要:提出一种基于确定的有穷状态自动机(deterministic finite automaton,简称DFA)的正则表达式压缩算法.首先,定义了膨胀率DR(distending rate)来描述正则表达式的膨胀特性.然后基于DR提出一种分片的算法RECCADR (regular expressions cut and combine algorithm based on DR),有效地选择出导致DFA状态膨胀的片段并隔离,降低了单个正则表达式存储需求.同时,基于正则表达式的组合关系提出一种选择性分群算法REGADR(regular expressions group algorithm based on DR),在可以接受的存储需求总量下,通过选择性分群大幅度减少了状态机的个数,有效地降低了匹配算法的复杂性.