首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到20条相似文献,搜索用时 143 毫秒
1.
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。  相似文献   

2.
算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.  相似文献   

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

4.
荷兰国旗问题的形式化推导及其多态性实现   总被引:1,自引:0,他引:1  
讨论了程序功能规约变换和算法程序的形式化技术,通过功能规约变换,可以较自然地获得问题求解的递推关系,对荷兰国旗问题的求解过程显示了形式化推导在获得高效和正确的算法程序中的作用。最后,给出了问题求解的多态性实现。  相似文献   

5.
PAR平台从规约出发的算法推导与自动生成   总被引:1,自引:0,他引:1  
简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。  相似文献   

6.
基于PAR的算法形式化开发   总被引:6,自引:0,他引:6  
形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.  相似文献   

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

8.
提出了一种求解命令式程序中循环执行和终止条件的方法.该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导.现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序.提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正.  相似文献   

9.
介绍了Dijkstra的形式化推导方法的主要思想、步骤及要点。该方法主张程序开发和程序证明同时进行,先确定好描述程序功能的断言,再通过形式化方法推导出正确的程序。选择具有代表性的循环结构的实例进行推导证明,并对循环结构的形式化推导进行阐述说明。  相似文献   

10.
本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,并以之为核心近乎机械地构造出非递归算法。树和图的两个算法实例说明了本方法的有效性。  相似文献   

11.
背包问题是算法设计分析中的经典问题,本文采用贪婪法、动态规划法及递归法三种方法分别对背包问题、0-1背包问题及简单0-1背包问题进行算法设计和时间复杂度分析,给出具体算法设计和实现过程,并以具体实例详细描述不同方法求解问题解时算法基本思想,总结三种方法实现的优缺点并得出结论。  相似文献   

12.
背包问题是算法设计分析中的经典问题,本文采用贪婪法、动态规划法及递归法三种方法分别对背包问题、0-1背包问题及简单0-1背包问题进行算法设计和时间复杂度分析,给出具体算法设计和实现过程,并以具体实例详细描述不同方法求解问题解时算法基本思想,总结三种方法实现的优缺点并得出结论。  相似文献   

13.
基于四叉树的三维地形模拟的LOD算法   总被引:4,自引:0,他引:4  
荆涛 《计算机仿真》2005,22(11):123-126
细节层次显示和简化技术(LOD技术)是实时真实感图形学技术中应用比较多的一个技术,通过这种技术可以较好地简化场景的复杂度,同时对图形真实度损失很少,并满足一定的实时性.在众多文献所提到的LOD算法中,一种比较常用的算法就是基于四叉树的LOD算法,这种算法的基本思想极为简单,即利用一个距离的阈值来控制四叉树递归运算的深度,当这个阈值比较大时,得到较少的三角面片数量,反之则得到较多的三角面片.文中实验也是采用了这种方法进行LOD的计算.文中还讲述了LOD技术的原理以及算法实现,探讨了LOD算法的实现中的问题和改进的方法,研究了节点评价系统的改进方法,最后展望了LOD技术的进一步发展.  相似文献   

14.
数字滤波器和快速傅氏变换算法是数字信号处理的两大基石。在DSP芯片上实现数字滤波器算法的传统做法是用汇编语占编写软件来实现。用汇编语言编写的DSP程序具有最好的执行效率,但DSP汇编语言的编程效率较低。该文主要研究如何使用基于交互的方框仿真和自动代码生成快速原型的方法进行滤波器设计。实现了从顶层的系统仿真到底层的芯片算法的设计。这个方法大大地缩短了算法的开发周期。  相似文献   

15.
计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。  相似文献   

16.
基于模拟退火遗传算法的控制系统优化设计   总被引:2,自引:0,他引:2  
提出了一种基于模拟退火遗传算法的线性系统优化设计方法。该方法以控制系统的性能指标,包括瞬态指标和稳态指标及其组合为目标函数,实现了由传递函数描述的控制器的自动设计,而不必预选择特定的控制方案。遗传算法使用十进制数编码,配合使用模拟退火技术来得到更精细的调整。使用这种方法,不需要手工计算,就可以获得控制系统的最优性能。该设计方法还可以应用于非线性对象。  相似文献   

17.
最优化设计的程序实现方法决定了优化算法的执行效率及代码可读性,进而影响到优化设计在工程中的应用前景.最优化设计算法中常涉及到复杂的矩阵运算.通过分析比较几类实现矩阵运算的常用方法的优缺点,提出了基于C 表达式模板的最优化设计程序实现方法.最后,以DFP变尺度优化程序为实例,从程序可读性及执行效率上将几类方法进行了对比.结果表明,基于C 表达式模板实现的最优化设计程序在保证程序执行效率的基础上,能够提高程序的可重用性及可读性.  相似文献   

18.
递归算法设计及效率分析   总被引:1,自引:0,他引:1  
递归算法是非常常用和实用的程序设计方法,递归算法的效率问题值得去研究,给出针对递归算法的一般性分析方法:递推式计算法和递归调用树法,并通过实例加以说明。  相似文献   

19.
L. Carlucci 《Calcolo》1971,8(3):161-183
This paper presents an algorithmic interpretation of a method for the formal definition of programming lauguages which holds for languages having an ALGOL-like or PL/1-like structure. This algorithm is a Generalized Markov Algorithm (GMA) and models the behaviour of the abstract machine defined by the IBM Vienna Laboratory group for the formal definition of PL/1. The paper provides two extensions of the GMA method: The GMA here defined is nondeterministic and handles tree structured objects. The paper provides a set of rules defining the algorithm along with a technique for generating linear representations of objects having tree structures. The subject of this paper was first developed in a master thesis in mathematics at the University of Pisa (october 1968).  相似文献   

20.
讨论了递归算法的基本概念和原理,使用VB,给出了设计编写递归程序的方法。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号