二叉树排序非递归算法推导及形式化证明

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.     

二叉树队列关系问题非递归算法的推导及形式化证明

该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递...     

树非递归遍历统一的新解法及其形式证明

提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义变换公式参数,获得二叉树前序、中序和K叉树前序、后序的递推公式,所得算法比传统算法更简洁直观,表明本解法的有效性和通用性.     

基于有序搜索的攻击图生成算法

为了有效的生成攻击图并且限制攻击图的规模,提出基于有序搜索的攻击图生成方法.该方法采用估价函数作为网络状态节点拓展的依据,估价函数值越小,优先进行扩展.利用该方法降低网络攻击图的规模,减少系统生成攻击图时耗费的资源,生成的攻击图能够用于评估网络的安全性,能够给网络管理员提供有价值的信息用于管理网络,预防入侵.     

3个变形背包问题的形式化推导

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.     

深度优先搜索的非递归算法

深度优先法是图的遍历的一种重要的方法。改方法应用广泛,例如电网拓扑结构、DNA网络等复杂图形分析。在大型网络的分析过程中,深度优先搜索的递归算法效率地下。故本文论证了递归算法的优缺点,并用非递归算法实现了深度优先搜索。     

树的等价定义及其证明

本文给出并证明了树的七种等价定义。     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法;然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式;最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

构造纵横图加边算法的证明

本文首先对Travers的构造纵横图的加边算法给出形式描述和证明,然后又得到一个很自然的推论,使算法从只能构造一个纵横图推广到可以构造一族纵横图。     

复杂算法程序的规范证明和形式推导

能否实现复杂算法程序的规范证明和形式推导是检验某种形式化方法有无生命力的重要标志。本文介绍了这一领域的研究现状,重点综述了作者近年来提出的复杂算法程序形式化技术,以典型实例说明了使用这些技术的方法。     

程序的形式推导方法

阐述了形式推导方法的基本理论和基本思想.程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发与证明同时进行. 以实例说明了程序形式推导方法的使用.     

图的深度优先搜索遍历算法分析及其应用

本文通过具体的示例,详细分析以邻接表为存储结构进行图的深度优先搜索遍历的算法和在vc＋＋环境中实现的完整程序,最后介绍了基于该算法一些应用.     

基于攻击模式的广度搜索攻击图生成算法

网络攻击者一旦发生攻击行为,通常希望攻击行为能危害到最大范围,基于这一前提,依据广度优先搜索策略及属性攻击图模型,提出了基于攻击模式的广度搜索攻击图的生成算法,算法可以很快的生成攻击图并且规模明显减小,最后对该算法的性能进行了分析和实验分析。     

基于遗传和启发式算法的混合顶点着色算法

图的着色问题是一种典型的NP-完全问题.提出了基于遗传算法和启发式算法的新型混合顶点着色算法,该算法在实现过程中涉及到染色体的编码方法、适应度函数的设计以及遗传算子的选择等.实验仿真结果表明此算法改善了求解的时间复杂度,可以获得问题高质量的解.     

一个Z的证明责任产生器

在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求．证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程、完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍。     

基于AND／OR图算法的探讨

讨论了图搜索的ＡＮＤ／ＯＲ图算法,着重分析了它们的复杂性、优缺点及其相互关系,提出了改进要点．此外,探讨了类比搜索方法．