利用循环不变式理解和开发程序

本文论述了循环不变式及其开发技术和程序设计的联系，并通过实例说明循环不变式在理解和开发程序中的巨大作用。     

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

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

循环不变式开发技术研究

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

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

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

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

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

基于算法框架的可重用部件设计与实现

对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。     

关于高中新课程算法与程序设计教学的初步探讨

算法与程序设计教学内容是高中信息技术课程的核心和应用基础.此部分教学内容的目标定位是关键.程序设计教学在必修模块教学中要"淡化程序编写,注重算法思维",选修模块要渗透结构化程序设计的思想.要研究教学方法让学生通俗易懂地掌握"算法与程序设计"的基本技能.     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范(程序)的精化.精化演算方法能够通过演算的方式,把规范逐步精化为程序.然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的.形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序.因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索.     

一种自适应的循环不变式生成方法

基于条件赋值转换和自适应模板生成技术,提出一种自适应的的循环不变式生成方法.该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息,有针对性地发现潜在的循环不变式,并在Frama-C平台上实现一个插件looplnv.实验结果表明,与invGen和gin-pink工具相比,loopInv的应用更加有效,可较好地完成多数程序的验证过程.     

基于数据分类的循环不变式自动生成

生成循环不变式是实现程序验证的关键步骤，但人工撰写循环不变式不仅步骤繁琐且容易出错。为此，提出一种基于数据分类的循环不变式生成方法，可直接为C程序的循环语句自动生成循环不变式。该方法生成循环程序的后置条件，并构造其Hoare三元组，通过收集循环程序执行过程中产生的测试数据，并根据其是否满足循环不变式的三个条件进行分类，从而生成循环不变式。所提出的方法在31个基准测试程序上，与目前比较先进的循环不变式生成方法进行比较分析。实验结果表明，所提出的方法不仅能够为C程序自动生成可验证的循环不变式，而且能够为最多的基准测试程序生成有效的循环不变式。