检索结果-内蒙古大学图书馆

软件学报 2024年第9期35卷 4242-4264页

作者：左正康柯雨含黄箐王玥坤曾志城王昌晶江西师范大学计算机信息工程学院江西南昌330022

Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基... 详细信息

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

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

来源：评论

学校读者我要写书评

暂无评论

LLRB算法的函数式建模及其机械化验证

引用

软件学报 2024年第11期35卷 5016-5039页

作者：左正康黄志鹏黄箐孙欢曾志城胡颖王昌晶江西师范大学计算机信息工程学院江西南昌330022 江西师范大学数字产业学院江西上饶334006

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时... 详细信息

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法Isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在Isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少至84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

关键词： LLRB 函数式建模机械化验证 Isabelle定理证明器二叉搜索树

来源：评论

学校读者我要写书评

暂无评论

基于关系闭集的模糊互模拟算法函数式建模及其机械化验证

引用

江西师范大学学报(自然科学版) 2024年第6期48卷 640-645页

作者：吴嘉伟游珍左正康张晗庆程着江西师范大学计算机信息工程学院江西南昌330022 江西师范大学网络化支撑软件国家科技合作基地江西南昌330022

该文在基于关系提升的模糊互模拟算法基础上,设计了一种基于关系闭集的模糊互模拟函数式算法,并使用Isabelle/HOL定理证明器对算法的终止性和正确性进行了机械化证明,为模糊互模拟算法的形式化和自动化验证提供了参考.

关键词：模糊互模拟算法不确定型模糊迁移系统函数式建模机械化验证

来源：评论

学校读者我要写书评

暂无评论

基于最大半环的DP问题函数式建模与验证

引用

江西师范大学学报（自然科学版） 2024年第3期48卷 294-300,310页

作者：王唱唱游珍孙欢王昌晶江西师范大学数字产业学院江西上饶334000 江西师范大学计算机信息工程学院江西南昌330022 江西师范大学网络化支撑软件国家科技合作基地江西南昌330022

针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的... 详细信息

针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的基于最大半环的函数式建模算法与Wimmer定义的递归函数结果进行等价性验证,从而保证了函数式建模算法的正确性;最后通过对lcs问题案例分析,验证了该方法的可行性和有效性.

关键词： DP问题最大半环函数式建模验证

来源：评论

学校读者我要写书评

暂无评论

多维区域匹配算法的通用验证方法

引用

江西师范大学学报(自然科学版) 2024年第6期48卷 646-651页

作者：张晗庆游珍左正康吴嘉伟程着江西师范大学计算机信息工程学院江西南昌330022 江西师范大学网络化支撑软件国家科技合作基地江西南昌330022

区域匹配算法通常用于多维数据空间中快速匹配特定区域或数据集,被广泛应用于数据库系统、数据分发管理系统等.目前大多数区域匹配算法的实现方法效率较低且未得到正确性验证.因此,该文提出了一种多维区域匹配算法的通用验证规约,以威... 详细信息

区域匹配算法通常用于多维数据空间中快速匹配特定区域或数据集,被广泛应用于数据库系统、数据分发管理系统等.目前大多数区域匹配算法的实现方法效率较低且未得到正确性验证.因此,该文提出了一种多维区域匹配算法的通用验证规约,以威胁辐射源匹配算法作为实例,使用Isabelle/HOL定理证明器对其进行函数式建模.将该文实现的通用验证规约通过区域解释应用于威胁辐射源匹配算法,通过严格的机械化验证,确保了威胁辐射源匹配算法的正确性,进而验证了该方法的有效性和可扩展性.

关键词：多维区域匹配算法威胁辐射源匹配算法函数式建模机械化验证

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：