基于Kripke结构的程序正确性证明

为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。     

基于断言的程序正确性检测工具

文章提出了程序断言检测工具设计方案和基于断言的程序正确性检测步骤.该工具的基本原理是Floyd提出的"用断言式方法"证明程序的正确性的方法,通过一个断言发现工兵从程序中发现该程序断言,然后与程序要求满足的断言条件比较,判明其正确性.该工具在复杂条件下对程序正确性判断和大量重复程序检测上能发挥重要的作用.     

程序正确性证明

电子数字计算机的出现,不仅给科学数值计算提供了一种强有力的计算工具,而且也给数学工作者提出了一些新的理论问题.其中,程序正确性的证明问题,就是一个值得人们重视的一个基础理论问题.程序正确性的证明,从理论和实际两方面来看,都是计算机科学中一个十分重要的问题.一般来说,程序正确性的证明可以分     

一个不变式断言生成器

程序正确性证明是软件工程研究中一个很重要的课题。目前,程序正确性证明过程中一个最难解决的问题便是如何找出程序的不变式断言。本文在ELLOZY的基础上,对差分方程的化简公式进行讨论、简化,使得更方便、更有效地生成循环断言。我们在PDF—11机上用UCSD PASCAL语言实现了一个生成器,它能对含有数组的简单循环程序生成循环断言。     

与程序正确性证明有关的当前研究动向

<正> 5.1 引言 关于程序正确性证明这一领域目前已进行了大量的研究。这里,为了便于讨论,我们把这些研究分成如下几方面: 1.关于证明(部分)正确性和终止的证明技术。 2.有关程序正确性的程序设计和语言设计的一些考虑。     

一种基于程序正确性证明理论的程序开发方法

程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发和证明同时进行,程序开发完成的同时其正确性亦得以保 证,以两个问题的程序开发为例说明了程序的形式推导方法的使用。     

一种寻找测试值断言证明程序正确的方法

程序正确性证明采用程序调试虽然有利于检测程序的错误,但不能保证程序是正确的;采用程序验证虽然可以证明程序正确,但困难之处在于用户必须提出一系列的中间断言作为验证条件,而寻找这组中间断言是最困难的,也是程序验证的关键。为此,本文讨论对程序的静态分析产生的解的不变式与动态测试所获得的测试值相符合的方法,以此导出程序正确性的证明。这样既避免了程序验证所须的证明一组验证条件的长而使人腻烦的工作,也避免了程序调试必须选择样品调试数据的较难克服的困难。     

MPI程序的Petri网模型及其验证

利用PVM程序中抽取Petri网的方法实现了MPI程序的部分功能语句的Petri网抽象,并分别针对MPI-1和MPI-2在通信方式上的新特性给出对应的Petri网模型抽象方法,使利用Pertri网模型对MPI程序正确性进行理论验证成为可能.     

调试数据作为证明程序正确性的一种辅助手段

迄今为止,人们验证程序是否正确,无非是采用二种途径:证明和调试。程序正确性证明,理论上虽完美,但由于本身所具有的复杂性,对大型程序很难实现;程序调试做起来并不复杂,但由于调试实例的局限性,不能保证程序正确性。本文提出用调试数据帮助证明程序正确性,这对程序验证理论无疑是有意义的。     

递归Prolog程序的正确性证明

本文提出了一种称为Ｐｒｏ图的图形方法,并用该图形方法进行了递归Ｐｒｏｌｏｇ程序的正确性证明,文中包括Ｐｒｏ图的基本概念及生成规则,Ｐｒｏ图上各节点的的关系,Ｐｒｏ图的激活过程,并给出了着急递归程序正确性证明的公理和定理。     

基于良序集方法的程序终止性证明

在介绍程序正确性的定义和良序集的概念基础上,对良序集证明程序终止性思路和步骤进行了分析,利用实例来证明程序的终止性。     

一个统一的程序验证框架

本文提出了一个简单的方法，其中程序和其性质都由一个逻辑：时序逻辑中的公式表示．文中给出了一个程序的转换模块的定义，提出了时序执行语义的概念．它是一个时序公式，精确地说明了一个程序．将时序逻辑作为规范语言，程序正确性就意味着说明程序的公式蕴含说明性质的公式，其中蕴含即为一般的逻辑蕴含．因此，本文的方法为并发程序的规范及验证提供了一个统一的框架．它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统．一个缓冲系统的简单例子用来说明本文的方法．此例子表明本文的方法是可行的.     

递归动态代数

动态逻辑是研究程序正确性证明、程序推导和程序变换的有力工具.作为动态逻辑代数抽象的动态代数,可以细致刻划程序的性质.本文引入上下文无关无穷代数概念,借助此概念将递归特性引入到动态代数之中,提出了递归动态代数.     

程序正确性证明的形式技术——J.Schwartz教授来华讲演记录

美国纽约大学柯朗数学科学研究所计算机科学部主任 J.Schwartz 教授,应中国科学院计算技术研究所邀请,于一九七七年九月十七日至十月三日偕夫人共同在京讲学。讲学内容之一为“程序正确性证明的形式技术”(Formal Techniques for Proof ofProgram Correctness),共分十讲,每讲约一小时半,写有提纲。要求听讲者事先阅读 Z.Manna 所著《计算的数学理论》(Mathematical Theory of Computation)。及 J.E.Rubin所著《数学家所用的集合论》(Set Theory for Mathematicians).临行前留下他本人所著《关于㊣程序的技术》(On correct-Program Technology)以及和M.Davis合著的《定理验证系统和证明校验系统的元数学可扩充性》(metamathematical Extensibility for Theorem Verifiers and Proof-Checkers).在证明程序正确性的研究中,有若干不同的算什么。其中之一是致力于研究保持程序正确性的加工(manispulation)和组合(Combination)规则,以便从一个正确的程序出发(例如,从一个则高级语言写成的,已被验证为正确的程序出发),经上述规则得到其他正确程序(如目标程序)。Schwartz教授认为这是一个重要的途径。他以SETL语言书写的程序为研究对象,并提出了接近于Hoare系统的形式化验证方法。他认为使用SETL高级语言,不但使程序编写得简短,而且在描述归纳断言(inductive assertion)方面也是自足的。Schwartz教授也研究了程序的加工和组合规则,称这为变形规则(transformation rule).另外,由于人工证明程序正确性的过程中,仍然难免错误,因这提出证明验证系统问题,即建立一个计算机化的系统,自动验证人们给出的证明是否正确,他介绍了自己和Davis在这方面的工作。Schwartz在京讲学期间,还作过两次大型讲演,内容之一为“程序设计的非确定型方法：用途及其实现”(Programming Nodeterminism:Use and implementation).因验证系统的程序语言中允许出现非确定的选择算子,故将讲演附在本文后一起发表。本文根据讲授提纲和听课笔记,并参照两篇专著于1977年底整理而成。其中第三部分变形的形式化由洛阳石油设计院陶志成负责整理,其余各部分则科学院计算所周巢尘整理。整理过程中得到唐稚松、吴允曾同志的关心和帮助。     

精化演算支撑工具PRT的研究

1 引言精化演算是一种数学表示法和若干规则的集合,用于从程序规约推导出命令式程序。精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精化的程序开发方法比对已有程序进行验证以保证程序正确性的方法更有效。通过精化演算中的转换规则可以演算出精化的程序。利用精化演算从规约导出程序的过程由大量步骤构成,非常适合利用机器工具进行辅助。本文对精化工具进行了需求分析和功能分析,研究了一个新的精化工具PRT(Program Refinement Tool)并与现有的一些工具进行了比较。     

子目标归纳法及其应用示例

子目标归纳法是继各种归纳方法之后出现的又一种验证程序的方法。本文从递归和循环两个方面描述这种方法,给出了作者实践过的用子目标归纳法证明程序正确性的例题,揭示了子目标归纳法与归纳断言法的关系。     

序列折半划分问题的形式化推导

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

时序逻辑语言

1.前言时序逻辑语言(temporal logic language)既是一种程序设计语言,也是一种时序逻辑系统。它不仅能用来编写程序,而且能用来表示程序的性质和进行程序正确性证明。程序设计语言的研究对计算机科学的发展起着重要的作用。高级语言的兴起、结构程序语言的出现都说明了这一点。遗憾的     

计算机程序设计的公理基础

这篇文章对计算机程序设计的公理基础作了探索性说明;阐述了程序证明的部分公理和推理规则,并给出了实例;从理论和实践两个方面对采取公理方法证明程序和作形式语言定义可能得到的好处进行了全面评述。这篇文章在程序正确性证明或软件实现方面占有一定地位,自发表以来被广为引用,而且的确产生了许多可喜的结果。     

基于UPPAAL的微内核操作系统程序验证方法研究

随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。