形式化方法--程序的正确性验证-14

1、第14课正式方法-验证程序的正确性一、概述计算机的程序是静态对象，但说明问题的解决方法是动态对象。编程是使用编程语言的语句更改程序中数据对象的状态，并配置所描述问题的动态行为。这是不自然的，程序描述的动态行为也不能通过程序本身的静态结构直接证明其正确性。公式规范是对需求阶段的正式说明，是对用户要求的严格说明，一般形式用Hoare逻辑描述1，如下所示： p 1其中和分别表示初始和结束断言条件，意思是：“如果初始状态dI满足条件，则程序结束，结束状态df必须满足。”D=D1.将dn设置为程序p的状态空间。其中DJ (j=1，n)表示程序中数据对象的范围。和断言条件确定的法律初始状态和终止状态的集合

2、是d的子集。执行函数e: p 定义为：无定义合法初始状态不终止di的程序pE(P，dI)=退出状态df对于合法的初始状态di，程序p退出程序的准确性如下： p Iff 2Di(di)(退出程序p和you(e(p，di)一般来说，验证一个程序正确性的方法有两种。一个是程序的测试，另一个是证明程序的正确性。1.程序测试和程序验证如果程序运行结束时有效的初始状态di为df，则 (di)和 (df)都必须满足。可以用以下表达式表示此点：diPdf 3程序的测试是验证测试用例diPdf。也就是说，检查程序的di运行结果是否为df。合理的初始状态是无限的，因此程序验证中测试不是完整的方法。测试被认为尽可能

3、地发现错误，但不保证程序中没有错误2。您可以在大量应用程序中满意。但是，对于某些应用程序，测试是在航空、宇宙等领域不能满足的验证方法，如软件系统。显然，如果要求绝对准确的软件，测试是不能采用的方法。无论是白盒测试还是黑盒测试，(di，df) | di df，di和df都是从diPdf中选择有限的东西进行验证的，而各种测试方法只有选择(di，df)的策略不同。因此，为了验证程序是否完全正确，必须寻求其他解决方案。这就是程序的正确性验证。2.验证格式语义和程序的正确性程序的正确性验证需要严格的推送过程，以确保程序所有阶段的运行结果都是所需的结果，无论程序运行的初始状态如何。程序的正确性证明了现有的

4、三种方法：运营意义、主张意义和公理意义。他们分别用不同的正式方法严格证明一个程序是否正确。这种方法还不完善，对一般软件人员还不太熟悉，但确实是确保软件确实正确的唯一方法。运营含义(Operational Semantics)操作语义的基础是一种编程语言，但在一种计算机系统内实现，其语义学的意义也完全确定，因此自然将语言的实现作为语言意义的定义，称为操作语义。当然，这种执行必须在一种标准的、抽象的机器上进行。英国科学家P.J.Landin首次提出了一种称为“堆栈-环境-控制-外部存款”的抽象机器。IBM提出了VDL，它是解释编程语言含义的元语言。之后，英国爱丁堡大学提出了在数据结构中使用数学关系

5、构建操作语义解释系统的更一般的方法。该方法的本质是用抽象机器的状态空间和最简单的基本命令定义抽象语言的意义，将抽象语言的程序转换成一系列抽象机器的基本命令序列。这种对应环是固定的，抽象机器的基本指令的意义是固定的，因此一种编程语言的程序具有明确的、不可思议的意义。要验证抽象程序的正确性，相应的基本命令序列必须在抽象计算机上运行。基本命令序列的一次执行只能验证输入集、输出状态之间的关系。因此，用操作语义验证程序的正确性实质上是测试方式的验证方式。参考意义(Denotational Semantics)参考语义学是编程语言的意义由相应语言组件的意义决定的，而编程语言组件的意义独立于编程语言的个别实

6、现，必须是其本身固有的。参考语义学的出发点是语言组件执行的最终结果，不是其执行过程。此执行结果是由隐藏在语言组件形式后面的参考项目决定的，因此此方法也称为参考语义。主张语义学是牛津大学C.Strachey教授创立的。d .斯科特教授很完美。因此，主张的意思也称为牛津意思。IBM还创建了基于参考语义的VDM软件开发方法。参考语义是数学对象，如整数、集合、映射等。嫌疑人的集合称为论权。一种语言的指称意义是识别该语言的相关论着，并将语法成分映射到论着上。抽象编程语言程序的意义是指语义中的数学对象的数学运算，正确性证明是指引用语义的相应数学运算公式的特性(迭代类型语言组件的数学运算公式特性是不动点特性

7、)，这些特性可以严格推导和证明。公理化意义(Axiomatic Semantics)公理语义学是根据数学的公理方法来格式化编程语言相关语法的意义。利用公理语义学的编程语言，可以推断出该编程语言的程序意义，也可以用逻辑推理的方法证明该程序具有什么样的本质。公理语义学是最受欢迎的程序证明方法。这种方法最初由Floyd在“Assigning Meanings to Programs”一书中提出，C.A.Hoare在“an axiomatic basis for computer programming”一文中开发并完善公理意义为编程语言的每个组件(包括整个程序)定义了一对断言：先决条件和后断言。断言

8、是在特定语言组件运行之前满足的谓词，断言是在该语言组件运行后必须满足的谓词。使用公理语义学的方法有两种，一种是所谓的自上而下方法，用前置语和后置语描述用户的需要，然后逐步细化将前置语转换为后置语的步骤，直到每个步骤都用计算机语言实现。只要保证分解阶段正确，最终编程结果也是正确的。这种方法的典型代表是道森老师的XYZ系列语言4。另一种方法是自下而上，根据每个语言单元中定义的预断言及其组件本身的特征导出其后断言。一个语法单元的后断言可以作为对下一个语法单元的前断言，从而对整个程序进行后断言，以证明过程必须满足的特性和过程的正确性。二、公理系统：Hoare逻辑与时间逻辑公理系统是证明和验证最受欢迎程

9、序正确性的方法，Hoare系统是公理系统的典型代表，使用命题 p 表方法程序p的语义。如果在程序运行之前满足断言，那么程序运行结束时必须满足断言。下面是一个经典例子，说明了霍华德的逻辑及其优缺点。请n！的程序FAC(程序FAC的说明使用FLOW语言2，以下其他程式的说明相同):1=x；n=y；(while y，0) do (* (x，y)=x；-(y，1)=y)。如果n是任意自然数时程序运行结束，则x的值为n！此特性可用nNFACx=n！命题表达。也可以使用命题来表示程序FAC的其他特性，例如：ttFACy=0命题的意思是，无论初始值如何，当程序退出时，y的值为零。命令 p 不保证程序p必须终

10、止，因此，此命题也称为程序的部分正确性证明的命题(因为进程是否终止是不可重复的不可判断问题，即图灵机关闭问题)。本文没有深入讨论，下面提到的程序正确性证明都提到了部分正确性证明，文章最后再次提供了正确性证明的补充。)如果这种程序正确性的命题是真的，则称为horer系统的定理。那么，怎样用功利的方法推理呢？D=(a，I)表示a=(a1，A2，Am)是表示公理集合的演绎系统。I=(i1，I2，In)表示规则集。公理在体系中没有得到证明，是事先得到承认的事实。如果s是系统的合法语句，埃塔指示s为true。换句话说，s是系统的定理。 S1 S2 sp Sr表示系统中的规则之一，其含义如下S1 andS

11、2 and.andsp)thenSr在演绎体系中，一个定理的证明是合法的语句序列(试图利用公理或规则解释该语句为什么合法)。让我举一个著名的、最简单的演绎体系及其推理的例子。设定Dg=(Ag，Ig)。其中Ag=(A1，A2，A3)为：A1: 至少由两个点组成。A2:如果p和q是两个不同的点，则只有一条线通过p和q。A3:如果 l是直线，则存在l中没有的点。Ig=(I1，I2)为：I1: p if p then q泽塔qI2: p泽塔q p and q以下是“最低3分”的证明步骤。1.至少由两点A12.有行1、A2、I13.线外有点2、A3、I14.至少由三点1，2，i2程序的本质是状态转换，程

12、序的执行从满足前提条件的状态转换为满足后置条件的状态，程序的正确性证明为。结构化编程使用单个入口和单个出口的所有语法单位，因此以结构化编程语言编写的程序可以用以下形式表示：S1；S2；Sn 4对于D0，存在状态转换序列。D1、D2、dn (di表示si运行后的状态)。为了证明2，我们为每个对(si，si 1)定义断言Mi的谓词。显然，可以按照以下逻辑推理步骤证明(2)。D0 (d0) (d0) m1 (D1) m1 (D1) m2 (D2) Mn-1 (dn-1) (dn)证明mi(di)mi 1(di 1)是证明：I (mi (di)，si(执行语句后)Mi 1(di 1)。这样，程序的正确

13、性证明可以归结为各语句的正确性证明。以下Hoare逻辑提供了验证程序中语句的一般方法：Hoare逻辑是这样的演绎系统DH=(ah，ih)，ah是Hoare逻辑系统的公理集(不再在此列出)。除了一般逻辑系统的推理规则外，Ih还包括以下与FLOW语言相关的语法语义规则(有关公理系统的一般推理规则，请参阅5):(1) r skip r(2) a/x a=x r(3) r S1 o o S2 qS1；S2 Q(4) Rb S1 q Rb S2 q r if b then S1 else S2 q(5) IB s I I while b do s IB(6) r R1 R1 s Q1 Q1 qs q 要

14、使用Hoare逻辑验证程序，即程序的正确性证明(证明Hoare系统的定理)是使用前提条件、逻辑系统的公理、定理和上述语言组件中规定的语义规则，按照过程的执行步骤推导后缀条件。下面应用Hoare逻辑推导命题 n的证明过程：1.nn前提条件2.nn l=1，3 . l=x；FAC的第一个门4.nn x=1 2，3，规则(2)5.nn x=1 n=n 4，6.n=y；FAC的第二扇门7.nn x=1 y=n 5，6，规则(2)8.$ kn (nn x=1 * n *.* (n-(k-1) y=n-k) 78。使8成为规则5的I9.使69，9成为规则5中的b10.$ kn (nn x * y=1 * n *.* (n-(k-1) * y y=n-k) 8，911.* (x，y)=x；循环中的第一个语句12.$ kn (nn x=1 * n *