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

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

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

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

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

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

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

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

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

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

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

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

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

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

梯形电阻网络与结点电压的研究

由递推关系推导出梯形电阻网络的等效电阻,并证得当级数满足一定的条件时,等效电阻的值在一定误差范围之内才能接近一个定值,并且由递推关系推导出梯形电阻网络的结点电压公式,这种分析方法可以应用在复杂电路网络及算法分析中.     

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.     

对Wirth一个不变式的修正

With在《算法 数据结构=程序》一书中关于“对半检索”程序中给出了一个不变式,但该不变式是不完善的。本文对此予以了修正,并通过一 系列定理及其证明进行了完整的论证,在论证过程中,也揭示出程序作为一种对象,其整体的一些性质;程序的这些特性,在一般测试时未能被认识,因而程序中“不变式”及对“不变式”的论证,也应是程序中最有价值的资料。     

飞向Halo轨道的太阳帆航天器轨迹优化设计

研究太阳帆航天器从地球同步轨道飞向日-地第2Lagrange(L2)点Halo轨道时其转移并入轨的轨迹优化设计问题。提出了分3阶段优化设计的方法:首先调整航天器逃离地球的飞行轨迹,使其比较接近目标Halo轨道的不变流形;再借助不变流形,用遗传算法求解相应的最优控制,使其转移到目标Halo轨道的不变流形上;最后航天器将沿流形飞行完成入轨。数值仿真结果表明,提出的方法可以得到相当好的转移轨道。由此显示,将转移轨道分为若干阶段,借助不变流形,用遗传算法求解最优控制问题的轨道优化设计方法对于此类小推力变轨问题是切实可行的。     

飞向Halo轨道的太阳帆航天器轨迹优化设计

研究了太阳帆航天器从地球同步轨道飞向日-地第2Lagrange(L2)点Halo轨道时其转移并入轨的轨迹优化设计问题。提出了分3阶段优化设计的方法:首先调整航天器逃离地球的飞行轨迹,使其比较接近目标Halo轨道的不变流形;再借助不变流形,用遗传算法求解相应的最优控制,使其转移到目标Halo轨道的不变流形上;最后航天器将沿流形飞行完成入轨。数值仿真结果表明,提出的方法可以得到相当好的转移轨道。由此显示:将转移轨道分为若干阶段,借助不变流形,用遗传算法求解最优控制问题的轨道优化设计方法对于此类小推力变轨问题是切实可行的。     

一个可用于Web数据库系统的分配调度通用算法

分配调度问题是一种困难问题,有些甚至是NP完全类问题.因而解决此类问题的技术难度较大,一般采用与或图搜索技术来求解.这就给当前许多Web数据库系统中的分配调度程序的编制造成困难,笔者以毕业设计任务分配算法为例,给出了一个能解决一类约束条件为双向选择的分配调度问题的通用算法.该算法不涉及复杂数据结构和搜索过程,仅用关系数据库的表操作描述,并可用任一支持Web数据库的语言编程实现.     

C 语言源程序函数列表和函数调用树的自动生成

文档是编程工作的一个非常重要的环节，它一般包括规格化程序清单、函数调用关系、变量参访表和程序结构等等。本文介绍了用ＢｏｒｌａｎｄＣ＋＋编程实现函数列表和函数调用树的自动生成方法，并详细分析了有关的数据结构和主要算法及技巧。     

开发视频、音频数据管理函数的新方法

多媒体数据管理中，对视频、音频数据的管理，是用户程序设计中的难点，本文讨论了利用ＢｏｒｌａｎｄＣ＋＋Ｗｉｎｄｏｗ应用程序集成开发平台提供的ＭＣＩＷｎｄ的ＭＣＩ（多媒体控制接口）函数类，开发用户在Ｆｏｘｐｒｏ数据库系统下的视频、音频接口函数的方法     

COC++ 编译器面向对象技术的实现

ＣＯＣ＋＋编译器的功能是将Ｃ＋＋源程序转换为等价的Ｃ程序。ＣＯＣ＋＋编译器不是使用传统的构造方法而是采用面向对象的设计技术，将相应成分如符号表，语法分析等模块封装为类，并以Ｃ＋＋语言实现。符号表类封装符号表及其建立、登录、查找等操作。基于Ｃ＋＋的作用域规则，ＣＯＣ＋＋编译器为每个作用域中的符号建立一个符合表，利用指针链指明嵌套关系和继承关系。语法分析的模块设计为一个抽象类，定义所有语法成分类的公共特性和公共接口。实际的分析工作和语义处理工作通过Ｃ＋＋语言的多态机制由相应的派生类各自的成员函数实现。这样类化的编译结构不会因为增加某些语言成分而做很大的改动。阐述了面向对象的技术用于编译系统的设计和开发的特点。     

一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法

形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.