用daikon发现循环不变式

随着软件行业的深入发展,软件存在的问题与日俱增,程序正确性受到了广泛的关注,形式化方法是解决程序正确性的基本途径,而发现程序循环不变式是证明程序正确性的关键。本文介绍了循环不变式的基本概念以及计算不变式的基本方法;用JAVA重写了Siemens的replace C程序,并以JAVA和C两种语言的replace程序为例,对不变式动态探测工具daikon进行了深入的实验研究,试验结果揭示了daikon在探测循环语句不变式方面的不足,依此提出了改进daikon探测循环不变式的措施。     

2类数列问题循环不变式开发策略研究与应用

该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.     

关于循环与循环不变式的讨论

讨论程序设计中的循环与循环不变式的应用 .利用循环不变式可以方便地设计循环程序 ,并可证明程序的正确性 .     

算法归纳设计策略与循环不变式

分析了算法归纳设计策略与循环不变式之间的关系,提出把算法设计与循环不变式的构建相结合的思想,并通过实例说明其有效性和重要性.     

一重循环结构的分类及其循环不变性质的讨论

分析了一般一重循环结构的组成要素，按组成要素给出了一重循环结构的初步分类及其程序函数，并且利用不变式状态定理讨论了 样分类下的循环不变式。     

试论循环不变式和囿界函数在循环研制中的地位和作用

详尽分析了循环不变式和囿界函数在循环研制中的地位和作用,并讨论了其构造方法。     

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

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

程序正确性证明中逻辑公式的可满足性

采用Herbrand定理及归结原理证明在程序证明中遇到的逻辑公式是可满足的。并给出了相应的算法;同时讨论了已知循环程序中循环不变式的求解方法。     

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

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

关于求已知do循环不变式的一个方法及for循环的WP的定义

对确定性do循环,利用其WP求出循环不变式.给出了for循环的话义定义.     

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

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

Perturbation to Noether Symmetry and Adiabatic Invariants for Dynamical Systems with Nonstandard Lagrangians

The perturbation to Noether symmetry and adiabatic invariants for dynamical systems with nonstandard Lagrangians are studied. Based on two kinds of nonstandard Lagrangians( i. e.exponential Lagrangians and power-law Lagrangians),the exact invariants of Noether type are given. Based on the definition of highorder adiabatic invariants,the relationship between the perturbation of Noether symmetry and the adiabatic invariants of the system under a small disturbance is studied,and then the corresponding theorems of adiabatic invariants are established. Finally, two examples are given to illustrate the methods and results appear in this paper.     

矩在面部表情识别中的应用

将Zernike矩和小波矩运用于面部表情识别问题,分别计算了面部图像的Hu矩、Zernike矩、Haar矩、Shannon矩和B样条矩,以模式识别中常用的类间距作为依据,提取了面部图像的各种矩的最好特征和次好特征,并对Zernike矩和B样条矩的识别能力和抗噪性进行了比较.实验证明:用Zernike矩作为面部表情特征,其识别率在特征数取5个时能达到95%,B样条矩在特征数取2个以上时识别率能达到100%.     

基于局部色彩不变量的图像篡改检测方法

针对基于分块的图像区域复制篡改检测方法通常面临的图像特征提取计算量大、维度高、识别率低等问题,提出一种基于局部色彩不变量特征的图像区域复制篡改检测方法,将RGB彩色图像转换到对立色彩空间,通过分析和提取图像各通道上的局部密度分布特征,构建k-d树进行相似分块特征匹配以实现图像区域复制篡改检测.提出的局部色彩不变量密度特征具有维度低、计算简单等特点.实验结果表明,本文方法与其他几种典型的基于分块的方法相比,具有较低的时间复杂度和较高的检测率,且对图像篡改区域的旋转、缩放攻击具有较好的鲁棒性,特别是当图像篡改区域进行大角度旋转时与其他几种方法相比具有明显优势.     

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

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

MATLAB5.2版的Simulink在仿真中的应用

介绍了ＭＡＴＬＡＢ５ ．２ 版仿真软件的主要功能及Ｓｉｍｕｌｉｎｋ 的主要特点;用Ｍａｔｌａｂ／Ｓｉｍｕｌｉｎｋ 建立双闭环直流调速系统的Ｓｉｍｕｌｉｎｋ 模型对系统进行仿真,指出了Ｍａｔｌａｂ／Ｓｉｍｕｋｉｎｋ 内部还有很多值得探索和研究的地方有待进一步去开发和完善