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

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

一种形式化开发非递归算法的方法*

提出了一种简单、统一的形式化开发非递归算法的方法.该方法直接面向非递归算法,在形式化方法PAR的指导下,使用循环不变式的开发新策略,在得到求解递归问题的循环不变式的同时,能直接得到易读、高效且可靠的非递归算法,并通过一个具体实例进行了阐述.对使用形式化方法及循环不变式开发新策略开发非递归算法的方法作了较深入的实践和探讨.     

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

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

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

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

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

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

用VB编写Hanoi塔问题动态演示程序

递归技术是算法设计过程中的一个重要技术,Hanoi塔问题是一个典型的适合用递归技术求解的问题.将Hanoi塔问题的递归执行过程利用编程方法动态演示出来,有助于人们结合Hanoi塔问题加深对递归技术的理解.     

用VB编写Hanoi塔问题动态演示程序

递归技术是算法设计过程中的一个重要技术,Hanoi塔问题是一个典型的适合用递归技术求解的问题。将Hanoi塔问题的递归执行过程利用编程方法动态演示出来,有助于人们结合Hanoi塔问题加深对递归技术的理解。     

对Hanoi塔问题非递归算法的改进

通过对前一非递归算法的分析，给出了Hanoi塔问题改进的非递归算法的思想和程序执行步骤，并用C语言实现了该算法。该算法优点在于能一次求出移动步骤，并且其时间复杂性有较大的改善。     

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

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

Hanoi塔问题非递归的新算法

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

分划递推法及其应用

分划递推法是一种新的算法设计技术。在分划递推法中使用逻辑符号和扩充的量词表示功能规约。分划是处理复杂问题的一般方法,而递推可用于循环不变式和算法设计开发。文中给出的三个实例呈现了使用分划递推法进行算法设计和开发的步骤和要点。     

使用队列生成二叉链表树的非递归算法实现

讨论了利用队列来生成二叉链表树的非递归算法,通过借助了二叉树的顺序存储方法以及构建一个临时的队列来实现这个算法,该算法的提出丰富了由递归算法转换成非递归算法的方法。     

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。     

形式化方法在高中算法教学中的应用研究

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR（Partition And Recur）方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。     

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.