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

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

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

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

循环界函数的应用及求取方法

讨论了循环界函数在程序正确性证明和程序推导技术中的应用问题，提出了求取几类已知循环程序的界函数和面向目标的程序推导中循环界函数的方法．     

二分查找树插入和删除算法的综合推导

程序综合是根据程序规范,推导出满足此规范的程序,推导的过程就是证明的过程,从而保证了最终程序的正确性.程序规范是对程序所要完成的任务的数学描述,表明了程序的目的和应满足的性质. 我们这里借助类似于函数程序语言Miranda的一种函数语言,这种语言曾作为英国牛津     

基于GEP的线性指数函数型程序不变量动态发现方法

不变量是用来描述程序运行时保持不变性质的逻辑断言.根据关系数据理论,程序不变量可分函数依赖型和非函数依赖型程序不变量.着眼于函数依赖型程序不变量,借助GEP的函数发现特点和Daikon对线性程序不变量的发现能力,重点对线性指数函数型程序不变量动态发现方法进行研究,通过实验证明了GEP对线性指数形式的函数有较高的发现效率,可以扩展Daikon在线性指数函数型程序不变量方面的预置形式以达到从程序轨迹数据中发现该类程序不变量的目的.     

图搜索问题算法推导及形式化证明

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.     

基于GEP-RNC的指数对数型程序不变量发现方法

程序不变量的发现是一种提高软件质量的有效方法.不变量发现工具Daikon可以发现程序中蕴含的简单不变量形式,但不包括复杂的函数型不变量.本文基于GEP-RNC算法对指数对数型不变量发现方法进行研究,通过实验证明GEP-RNC算法可以有效的发现指数对数形式的不变量,解决了基因表达式编程算法在复杂函数形式发现中稳定性不佳,精度不高的问题,扩展了Daikon不变量测试库中程序不变量的类型.     

用积分离散法解三维弹塑性力学问题

本文叙述了积分离散有限元法的基本理论,推导出该方法解决三维弹塑性力学问题的计算公式,并编制了程序.利用该程序对五龙矿东风井歪斜问题进行了空间弹塑性计算和分析,结果表明该方法编制的程序有很大的优点.     

用无网格法分析功能梯度材料圆板的自由振动

采用一种新的方法研究了变厚度功能梯度材料圆板的自由振动问题。首先用能量法获得了自然频率的基本方程,通过无网格法构造形函数;然后采用伽辽金弱形式公式求解偏微分方程,得到关于频率和振型的矩阵方程。最后根据以上推导编写MATLAB程序,计算简支和固支两种边界条件的变厚度功能梯度材料圆板无量纲自然频率及振型;并探讨相关参数对结果的影响及提高计算精度的因素。结果表明无网格法求解得到的系统自然频率与已知的解析解基本一致,证明这种方法的理论推导和程序编写是正确的,可以应用于变厚度功能梯度材料板的自由振动分析;且其具有理论简单、计算量小等优点。     

完全矩阵形式的牛顿潮流计算

在极坐标形式的潮流方程的基础上,推导出该潮流方程的矩阵形式,并给出了牛顿法潮流计算的修正方程式以及支路功率计算公式的矩阵形式.这组公式可以简化利用Matlab编写潮流计算的程序.并且通过算例证明,提出的矩阵形式潮流计算公式是正确的.     

形式化开发若干组合数学问题的算法

计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用.     

网络图上的分段线性分式规划模型及有效算法

为了得到网络图上分段线性分式规划问题的有效算法，借助于线性规划问题的单纯形方法及网络图上修改支撑树的迭代方法，论证了一个基本可行解是否最优解的判别准则，并给出了网络图上分段线性分式规划问题的一个有效算法。为进一步解决网络图上非线性目标函数的优化问题提供了依据。     

九参数拟协调离散Kirchhoff薄板单元

用多变量拟协调法推导出九参数拟协调离散Ｋｉｒｃｈｈｏｆｆ薄板单元（ＱＤＫＴ－９）， 并证明了ＱＤＫＴ－９单元与 ＤＫＴ－９单元（九参数离散 Ｋｉｒｃｈｈｏｆｆ 薄板单元）的一 致性。基于拟协调元方法的理论和公式，人们将易于理解和认识这一类单元，ＤＫＴ 单元仅是一种放松了直法线假设的拟协调薄板元。不难看出：拟协调元方法是一种非 常基本的有限元方法。     

晶体对称性定律的一种证明

本文介绍了一种根据完全相同的正多边形在二维空间并置堆砌应严格遵循的规律来证明“晶体对称性定律”的新方法。这种方法不仅数学依据严密,而且将晶体的对称性质与堆砌理论初步结合了起来。     

基于因果关系复合的结构化并行程序设计

基于有关因果关系复合的ＣｏｍｍｕｎｉｃａｔｉｏｎＣｌｏｓｅｄＬａｙｅｒ理论，提出了一种结构化并行程序设计方法，以支持不同并行平台的“通用”并行程序设计方法．因果关系复合的范式定理的证明在理论上保证了采用“ＳＥＱＯＦＰＡＲ”形式进行结构化并行秩序设计的可行性；良好的代数性质也使得在这一模型中可采用代数方法的程序变换来进行并行程序设计、优化和验证．与其他并行程序设计模型和方法相比，提供了一种非常自然地综合描述数据并行和控制并行的途径；特别是基于代数变换的程序变换技术，提供了一种既独立于具体的体系结构又可高效实现的可能性．     

平面有限元网格自动剖分法

提出了一套新的完整的平面有限元网络自动剖分方法，着重介绍网格自动剖分的基本原理、推导过程、程序设计思路以及其它计算数据的前处理。     

CLAUS工艺复杂化学反应平衡计算的新方法——原子自由能贡献法

本文根据最小自由能法原理推导了复杂气相反应平衡的原子自由能贡献法的计算模型,提出了用此法计算Claus工艺复杂化学反应平衡,获得了满意的效果,为精确及优化设计提供了理论依据和手段。本文还给出了再热炉设计时天然气和空气配比对出口燃烧产物组成更正确的平衡关系。文中的方法不必涉及具体的反应,通用性强且计算速度快。     

并发计算的元模型Ⅰ.图模型

借鉴证明论中的一些思想 ,提出了并发计算的一个图模型 .在此模型中 ,计算对象表示为图 ,计算过程表示为图重写 ,重写规则将通信过程视为证明的等价变换过程 .为便于形式化研究图模型 ,提出了模型的形式对应物——图演算 ,该演算类似于进程代数演算 ,与其他进程代数演算的不同之处在于本演算是对称的 .文中用证明论方法研究并行理论 ,为进程代数演算开辟了一条新的研究途径