杨庆红[1]2003年在《递归问题循环不变式开发新策略的研究与应用》文中研究表明软件形式化是提高软件可靠性和生产效率、实现软件自动化的有效途径。循环不变式在软件形式化方法中占有十分重要的地位，它是理解、证明和推导算法程序的基础和关键。因此目前许多算法和程序设计的着作和教材中，均广泛地使用了循环不变式的概念和技术。 然而循环不变式的理论和开发技术尚很不完备，这直接影响了循环不变式在算法程序形式化开发中作用的发挥，导致大量复杂算法程序缺乏令人信服的推导和证明，使得许多计算机科学工作者对Dijkstra，Hoare和Gries等着名计算机科学家积极倡导的算法程序形式化开发方法的可行性和实用性产生了怀疑。 为了克服已有循环不变式开发技术存在的局限性，薛锦云教授在两个国家自然科学基金课题“若干新的算法程序设计和证明方法研究”和“实用的软件形式化方法及其开发工具的研究”的资助下，对循环不变式的理论和方法进行了系统的研究，提出了关于循环不变式的新定义和新的开发策略，并在此基础上形成了一种实用的算法程序形式化开发方法(PAR方法)及其开发环境，在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续，也是薛锦云当前主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”的重要研究内容。 本文研究的主要目标是利用薛教授在开发循环不变式的新策略中提出的递归定义思想，探索一类递归定义问题的循环不变式开发技术，并应用于涉及组合数据结构的复杂算法程序的形式化推导和证明。具体研究成果如下： 1．进一步深入研究了循环不变式在算法程序形式化方法中的地位和作用； 2．对现有的循环不变式开发技术进行了分析和比较，剖析了其难以实用的原因； 3．基于现有循环不变式开发技术中的递归定义思想，提出了开发复杂递归问题循环不变式的两种新策略； 4．利用抽象程序设计语言Apla精确描述了6个典型树、图等问题的程序规约和求解算法程序，用上述提出的两种新策略开发了循环不变式，实现了严格的形式化推导或证明，并用PAR方法提供的算法程序自动转换系统将得到的Apla算法程序转换成对应的Delphi和C~(++)程序，均得到了正确的运行结果，大幅度地提高了这类复杂算法程序的可靠性和开发效率。 总之，本文得到的结果可应用于一类复杂算法程序的形式化推导和证明，方法简单，应用方便，为实现算法设计的形式化和自动化作出了有益的贡献。
万松松[2]2008年在《循环不变式开发技术研究》文中认为高可靠性软件是当今软件开发的热点问题.确保算法程序逻辑结构正确最理想途径是算法程序的形式化推导和证明。循环不变式在软件形式化方法中占有十分重要的地位,它是理解、证明和推导算法程序的基础和关键。使用形式化方法来证明或推导算法程序无法回避的一个问题就是给出正确的循环不变式。但是循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。自形式化方法出现以来,众多专家致力于循环不变式的开发,提出了许多循环不变式开发技术,如谓词抽象技术、动态探测技术等。这些技术能探测出较简单问题的循环不变式,但是却无法处理复杂问题。从本质上来说,循环不变式刻画了循环变量的变化规律和循环程序的特征,因此一个循环程序的循环不变式并非轻易就能得到,尤其是对复杂算法的来说,必须在对循环程序的算法本质有充分理解的基础上才能找到。而现有的循环不变式定义不能反映出循环不变式的本质,基于现有循环不变式定义的技术缺乏理论上的指导,在探测循环不变式的过程中具有试探性和盲目性,又因为本身技术上的限制,因而无法得出复杂问题的循环不变式。薛锦云教授及其学术团队分析了大量算法程序的本质特征及其与循环不变式关系[15]~[20],发现现有循环不变式定义的不足,提出了关于循环不变式的新定义和基于新定义之上的循环不变式开发技术,并在此基础上形成了一种实用的算法程序形式化开发方法——PAR方法及其开发环境,在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续,也是薛锦云主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”和973前期预研项目“形式化方法制导的软件自动化研究”的重要研究内容。本文主要的工作是对现有循环不变式定义和现有开发技术进行深入研究,并与PAR方法中的循环不变式开发技术进行比较,指出了现有开发技术的不足之处;同时基于薛锦云教授提出的循环不变式新定义和新开发技术,探讨、研究并初步实现了循环不变式自动开发系统。具体研究成果如下:1.深入研究了循环不变式定义;2.对循环不变式标准开发策略和现有较新的几种循环不变式开发技术进行了分析和比较,剖析了其难以适用的原因;3.详细分析了PAR方法循环不变式新定义和新开发策略,以其作为基础提出了循环不变式开发系统的新模型,并初步实现循环不变式自动开发系统;4.使用Dijkstra最弱前置谓词法对开发出的循环不变式进行正确性证明。
杨黄磊[3]2014年在《单元赋值语句型循环不变式的开发方法研究》文中研究指明“软件危机”的出现，对于软件的可靠性和生产效率提出了更高的要求，形式化开发软件是一个很好的解决办法。而形式化开发软件就是要保证能对算法程序进行正确的推导和证明。而循环不变式是算法程序进行推导和证明的基石。任何一个循环程序都存在一个循环不变式，它在循环执行前和每次迭代后都能成立，当达到循环退出条件时，它产生了循环的最后结果。然而循环不变式无论是手工开发，还是自动构造一直都是一个巨大的挑战。本团队承担了国家自然科学基金重大国际合作项目：若干软件新技术及其在PAR平台中的实验研究。其中研究方向之一就是循环不变式的构造和自动探测。本文首先分析了国内外对循环不变式的定义及其开发方法的研究现状。然后介绍了本团队基于问题求解序列递推关系的循环不变式开发方法。接着介绍单元赋值语句型循环不变式的开发方法：按照PAR方法中的循环不变式开发策略，首先开发出抽象的单元赋值语句型循环程序的循环不变式，即抽象的单元赋值语句型循环不变式，并用Dijkstra最弱前置谓词方法进行了形式化的证明，然后对于具体的单元赋值语句型循环程序，将其对应的抽象的单元赋值语句型循环不变式进行参数实例化即可得到所需的单元赋值语句型循环不变式。最后在本研究团队已有循环不变式自动生成系统中实现了单元赋值语句型循环不变式的自动生成。本文的创新点有如下3个方面：1.对单元赋值语句和单元赋值语句型循环程序进行了抽象，使得该方法具有一定的普遍性和典型性。2.运用Dijkstra最弱前置谓词方法对开发出的抽象的单元赋值语句型循环不变式进行了形式化证明。3.在本研究团队已有的循环不变式自动生成系统上扩充实现了单元赋值语句型循环不变式的自动生成。
王森[4]2004年在《基于PAR方法开发算法程序的研究》文中研究表明软件系统的成功极大依赖软件需求工程的质量，而软件的可靠性难以保证和开发效率低一直是困扰软件产业的两大难题。而用形式化方法开发软件始终被认为是提高软件可靠性和软件生产率的重要途径，是实现软件开发自动化的关键。尽管已经提出了各种各样的软件形式化方法和开发技术，但目前这些技术还远没有广泛的被软件产业界所接受，原因在于许多方法的提倡者并没有真正研究软件开发者面临的实际问题，算法和程序研究脱节，缺乏系统的算法程序设计和证明方法，实际上有些方法以及这些方法为基础而建立的软件开发工具和自动生成系统只能处理和生成一些玩具式程序(toy-style program)。尚没有一种面向实际问题、简单可行、便于广大软件开发者接受的形式化方法及与该方法相配套的一系列配套的辅助工具来切实的解决这两个问题。 PAR方法基于分化、递推、扩充的量词变换规则、循环不变式的新技术和软件转换工具，充分利用数据抽象、功能抽象、软件重用、多态、类属、重载等成熟的程序设计技术，可以用统一的方法开发复杂算法。 本文首先对形式化方法的定义、分类、目前的发展状况等进行了介绍，同时对典型的形式化方法VDM、Z、B方法、RAISE等形式化语言和方法的产生、主要原理及特点作了介绍，并进行了分析比对；其次，本文还对PAR方法也做了较为详尽的介绍，进一步研究了它的特点，阐述了其哲学思想；最后，运用PAR方法开发了正整数素数分解问题、线性代数统一的算法——基准位置法等多个问题的算法程序，进一步验证了PAR方法在很多复杂数值算法中的应用。
万松松, 薛锦云, 谢武平[5]2010年在《循环不变式开发技术研究》文中研究说明高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。
杨晨[6]2010年在《基于PAR平台的最弱前置谓词生成器的设计与实现》文中研究表明从上世纪六十年代起,随着大型软件的快速发展,人们对软件质量的要求起来越高,尤其是对软件的正确性要求。计算机界为确保软件质量尤其是软件的高可靠性方面提出了许多新的理论研究,程序正确性证明就是其中之一,程序正确性证明就是采用严格的数学方法评价一个程序是否达到了预定的性能。但是在证明程序正确的过程中由于要涉及大量的数学符号和数学相关理论知识使得程序验证人员需要花费一定的时间和精力去掌握这些知识。而且由于涉及到数学理论即使验证一个很短的程序也需要比较繁琐的验证过程,造成往往证明过程比要证明的程序要复杂很多的情况,这些种种不利条件使得依靠手工去证明程序正确性就可能产生许多不良的后果。为了克服手工对程序进行正确性验证程序所导致的不良后果,许多计算机科学家开始利用机器去自动验证程序来逐步降低人工干预程序验证的过程,最终的目的是将程序正确性验证走向完全自动化。根据Dijkstra的最弱前置谓词理论,对于程序{Q}S{R},如果能证明:Q ==> WP(“S”,R)则能断定程序正确。正是基于此理论,本文研究作为PAR平台的一个辅助工具部分,目标是开发一个自动计算Apla程序的最弱前置谓词的系统,减少Apla程序正确性验证的人工干预,在已知S,R的情况下自动求解出最弱前置谓词。围绕这个宗旨本文做了如下工作:1、在深刻理解了Dijkstra最弱前置谓词的的基础上提出了自动计算APLA语言最弱前置谓词的算法。2、选取了若干Apla程序进行试验,实验结果表明,系统初步实现了自动计算最弱前置谓词的功能。3、尝试将Dijkstra最弱前置谓词自动生成器整合到PAR平台,使其成为PAR的一个辅助工具;能够有效的支持PAR平台。后期的工作包括完善系统的各项功能;进一步提高系统的可靠性和健壮性;加强对复杂性算法和经典数字问题算法的分析和求解。
钟珞, 管昌生, 赵愚, 潘昊[7]1995年在《逐步求精的一种模型》文中指出提出一种支持程序开发的结构化方法．该方法以一种简单的问题分解策略为基础，比Ｗｉｒｔｈ－Ｄｉｊｋｓｔｒａ的自顶向下逐步求精方法更利于面向目标的程序设计．由该方法可知，一个程序可经一系列求精而开发出来，每一步求精都能为相应的最弱前置条件序列建立后置条件．这种策略使情况分析减少到极限，简化了结构化程序的证明，并保证了程序结构和数据结构之间的对应．
参考文献：
[1]. 递归问题循环不变式开发新策略的研究与应用[D]. 杨庆红. 江西师范大学. 2003
[2]. 循环不变式开发技术研究[D]. 万松松. 江西师范大学. 2008
[3]. 单元赋值语句型循环不变式的开发方法研究[D]. 杨黄磊. 江西师范大学. 2014
[4]. 基于PAR方法开发算法程序的研究[D]. 王森. 江西师范大学. 2004
[5]. 循环不变式开发技术研究[J]. 万松松, 薛锦云, 谢武平. 计算机工程与科学. 2010
[6]. 基于PAR平台的最弱前置谓词生成器的设计与实现[D]. 杨晨. 江西师范大学. 2010
[7]. 逐步求精的一种模型[J]. 钟珞, 管昌生, 赵愚, 潘昊. 武汉工业大学学报. 1995
标签：计算机软件及计算机应用论文; 递归算法论文; 递归论文; 赋值语句论文; 循环语句论文; 形式化方法论文; 算法论文;