形式化开发非递归Koch曲线算法

形式化方法是构建可信软件的重要途径。Koch曲线是典型的分形图形。基于形式化方法PAR及循环不变式开发策略,开发了Koch曲线非递归算法,并对其进行了形式化的正确性证明。在得到求解Koch曲线算法的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨。     

形式化开发Hanoi塔问题非递归算法

使用形式化方法PAR及循环不变式开发新策略,开发了Hanoi塔问题非递归算法,并对其进行了形式化地正确性证明。本文直接面向非递归算法,在得到求解Hanoi塔问题的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发新策略开发非递归算法作了较深入的实践和探讨。     

Hanoi塔非递归算法的形式化推导和正确性验证

关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.     

后序遍历二叉树非递归算法的推导及形式化证明

开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。     

一种求解树深度的非递归算法

树是计算机科学中经常用到的一种典型的非线性数据结构。本文介绍一种求解其深度（高度）的非递归算法，同递归算法比较，既易于理解，又解决了某些高级语言因无递归机制而带来的实现上困难。     

Hanoi塔问题非递归的新算法

关于Hanoi塔问题的非递归算法,已有了大量的研究[1￣4]。实验表明,当圆盘数目较少时,现有的非递归算法的执行速度比递归算法要快一些,但是随着圆盘数目的增加,现有的非递归算法的执行速度会逐渐变得比递归算法慢。论文提出了一种基于压缩编码的非递归新算法,在压缩了存储空间的同时,提高了算法的执行速度。实验结果表明,对于任意圆盘数目n,论文所实现的非递归算法的执行速度比现有的递归算法和非递归算法都有成倍的提高。     

0-1背包问题的一种新解法

针对目前求解0-1 背包问题算法的优缺点,开发了一种新的非递归算法。从计算0-1 背包问题最优值的递归方程出发,使用形式推导技术及序列抽象数据类型。在开发出循环不变式的同时,归纳得到用抽象程序设计语言Apla描述的非递归算法,并形式化证明了其正确性,在相关工具及部件库的支持下进一步得到C++程序。理论分析和实验结果表明,该算法的时间耗费受背包容量变化的影响很小,是一种有效的方案。     

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换，形式化推导出可读性好、效率高的递推的最小生成树算法，简化了算法程序设计和正确性证明的过程，有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。     

Hanoi塔问题的一种非递归算法

通过对 Hanoi塔问题的研究 ,给出了 Hanoi塔问题的非递归算法的思想和流程图 ,并用不允许递归调用的 BASIC语言实现了 Hanoi塔问题的非递归算法。该算法的优点在于可一次性求得总移动次数 ,但从程序结构看其编程思路较复杂 ,难于理解 ,算法的时间复杂性和空间复杂性与递归算法无异。     

一种将递归过程转换为非递归过程的方法研究

提出一种把递归过程转换为非递归过程的方法——递归树法,画出递归过程的递归树,然后通过对递归树的后根序遍历实现递归过程的非递归化,最后通过案例说明该方法的可行性和有效性。     

循环不变式开发新策略及其应用

循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。     

循环不变式开发技术研究

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。     

PAR方法在组合游戏上的应用

简述了薛锦云教授所创的PAR方法和组合游戏(Nim)之后,本文运用PAR方法详细推演出解决组合游戏中的一个典型例子(Nim)的算法的数学模型。在此数学模型的基础之上,再次运用PAR方法推演出解决Nim的简短的核心算法。     

PAR平台中若干软件构件形式化验证技术研究

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。     

PAR方法和循环不变式的范畴语义

范畴论对理解程序规约及程序设计和正确性证明十分有用。PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法。循环不变式在循环算法程序的设计中至关重要。使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础。在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程。     

Unified Approach for Developing EfficientAlgorithmic Programs

A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented.An algorithm(represented by recurrence and initiation)is separated from program,and special attention is paid to algorithm manipulation rather than proram calculus.An algorithm is exactly a set of mathematical formulae.It is easier for formal erivation and proof.After getting efficient and correct algorithm,a trivial transformation is used to get a final rogram,The approach covers several known algorithm design techniques,e.g.dynamic programming,greedy,divide-and-conquer and enumeration,etc.The techniques of partition and recurrence are not new.Partition is a general approach for dealing with complicated objects and is typically used in divide-and-conquer approach.Recurrence is used in algorithm analysis,in developing loop invariants and dynamic programming approach.The main contribution is combining two techniques used in typical algorithm development into a unified and systematic approach to develop general efficient algorithmic programs and presenting a new representation of algorithm that is easier for understanding and demonstrating the correctness and ingenuity of algorithmicprograms.