第十四讲形式化方法--程序的正确性验证一、概述计算机的程序是一种静态的对象，但它所描述的问题（问题的解）却是一个动态的对象。
所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态，构造所描述问题的动态行为。
这是不自然的，程序所描述的动态行为也无法直接用程序本身的静态结构进行正确性证明。
形式化规约（formal specification）是需求阶段的形式化说明，是用户需求的严格描述，其一般形式用Hoare逻辑描述[1]如下：├{Φ}P{Ψ} <1>其中Φ和Ψ分别表示初始和结束断言条件，其含义是：“假如初始状态d I满足条件Φ，那么程序结束并且终结状态d f必须满足Ψ”。
设D＝D1×……×D n为程序P的状态空间，其中，D j(j=1,……,n)表示程序中数据对象的值域。
显然，由Φ和Ψ断言条件所确定的合法初始和结束状态的集合是D的一个子集。
执行函数E：Φ×P→Ψ定义如下：无定义对合法的初始状态d i，程序P不结束E（P,d I）=终结状态d f对合法的初始状态d i，程序P结束程序的正确性即为：├{Φ}P{Ψ}iff <2>∀d i(├Φ(d i)→(├程序P结束 and ├Ψ(E(P,d i))))总地来讲，验证一个程序的正确与否有两种办法，一种是程序的测试，另一种是程序的正确性证明。
1．程序的测试与程序的验证对给定的一个合法的初始状态d i，当程序执行结束时其终结状态为d f，那么，Φ(d i)和Ψ(d f)都应该被满足。
这一点可用下式表示：{d i}P{d f} <3>所谓程序的测试就是验证测试用例{d i}P{d f}，即验证程序对d i的执行结果是否为d f。
由于合理的初始状态是无限的，因此，对程序验证来讲，测试不是一个完备的方法。
测试被认为是一种尽量发现错误，但并不能保证程序中没有错误[2]的方法。
对大数应用来讲，它是可满足的；但对有些应用来讲，测试是一种不能满足的验证方法，例如：航空、航天等领域的软件系统。
显然，对要求绝对正确的软件，测试是一种不能采用的方法。
无论白盒测试还是黑盒测试都是在无限集合{(d i,d f)|∀d i,∀d f, d i和d f满足{d i}P{d f}中选择有限的一些(d i,d f)对进行验证，而各种测试方法只是选择(d i,d f)的策略不同而已。
因此，验证程序是否完全正确要寻求另外的解决途径。
那就是程序的正确性验证。
2．形式语义与程序的正确性验证程序的正确性验证应该具有严密的推量过程，以保证程序每步执行结果都是希望的结果，而与程序执行的某个初始状态无关。
程序的正确性证明现有三种方式：操作语义、指称语义和公理语义。
它们分别用不同的形式化方法，严格地证明一个程序是否正确。
尽管这种方法还不够完善，还不为一般软件人员所掌握，但它确实是保证软件绝对正确的唯一途径。
操作语义（Operational Semantics）操作语义的根据是，一种程序设计语言一但在某种计算机系统中实施，其语义的含义也就完全确定下来了，因此，自然地就用语言的实施作为语言含义的定义，故称这种语义为操作语义。
当然，这种实施应该在一种标准的、抽象的机器上进行。
英国科学家ndin最早提出这种类型的一个抽象机器，称为“栈-环境-控制-外存”。
IBM公司提出了一种可描述程序设计语言语义的元语言：VDL。
后来，英国的爱丁堡大学提出了更一般的方法：在数据结构上用数学关系建立操作语义的解释系统。
这种方法的本质就是，用抽象机器的状态空间和最简单的基本指令来定义抽象语言的语义，将抽象语言的程序转换为一系列抽象机器的基本指令序列。
这种对应关是固定的，而且抽象机器的基本指令的含义是固定的，这样一个程序设计语言的程序就有了一个明确的、无二义的语义。
为了验证一个抽象程序的正确性，就必须在抽象计算机上执行其相应的基本指令序列。
基本指令序列的一次执行只能验证一组输入、输出状态之间的关系。
因此，用操作语义验证一个程序的正确性实质上是一种测试型的验证方式。
指称语义（Denotational Semantics）指称语义学认为，程序设计语言的语义是由其语言成份的语义决定的，而程序设计语言成份的语义应该是其本身固有的，与程序设计语言的个体实现无关。
指称语义的出发点是语言成份执行的最终结果，而不是其执行过程。
这种执行结果是由语言成份形式后面隐藏的所指物决定的，故这种方式也称为指称语义。
指称语义是由牛津大学的C.Strachey教授创立，D.Scott教授完善的，故指称语义也称为牛津语义。
IBM公司也创立了基于指称语义的VDM软件开发方法。
指称语义的指称物均为数学对象，如整数、集合和映射等。
指称物的集合称为论域。
一个语言的指称语义就是确定该语言的相关论域，并给出语法成份到论域上的语义映射。
一个抽象的程序设计语言程序的语义就是指称语义所指的数学对象在论域上的数学运算，其正确性证明就是指称语义相应的数学运算公式的特性（递归类型语言成份的数学运算公式特征就是其不动点的特征），这些性质是可严格推理和证明的。
公理语义（Axiomatic Semantics）公理语义是根据数学中的公理化方法形式化程序设计语言相关语法的语义。
赋以公理语义的程序设计语言，可推理出该程序设计语言的程序语义，也可用逻辑推理的方法证明该程序是否具有某种性质。
公理语义是最流行的程序证明方法。
这种方法最早是由Floyd在他的“Assigning Meanings to Programs”一文中提出的，后经C.A.Hoare在它的“An Axiomatic Basis for Computer Programming”一文中发展和完善的。
公理语义对程序设计语言中的每个成份（包括整个程序）定义了一对断言（assertoin）：前置断言（Precondition）和后置断言(Postcondition)。
前置断言是某个语言成份在执行前满足的谓词，而后置断言则是该语言成份执行后应该满足的谓词。
有两种使用公理语义的方式，一种是所谓的自顶向下的方法，用前置和后置断言描述用户的需求，然后，将前置断言向后置断言转化的步骤逐步细化，直到每一步都能用计算机语言进行实施为止。
只要保证分解的步骤是正确的，那么最终的程序设计结果也是正确的。
这种方法的典型代表是唐稚松先生的XYZ系列语言[4]。
另一种方法是自底向上的，根据每个语言单元定义的前置断言和该成份本身的特征，推导出其后置断言。
一个语法单元的后置断言可作为下一个语法单元的前置断言，从而揄出整个程序的后置断言，以此可证明程序应满足的性质和程序的正确性。
二、公理系统：Hoare逻辑和时态逻辑公理系统是最流行的程序正确性证明和验证的方法，Hoare系统是公理系统中的典型代表，它用命题{Φ}P{Ψ}表法程序P的语义：如果程序执行前满足断言Φ，则当程序执行终止后，它一定满足断言Ψ。
下面通过一个经典的例子说明Hoare逻辑表述和其优缺点。
求n!的程序FAC（程序FAC的描述采用FLOW语言[2]，以下其它程序的描述相同）：1=>x; n=>y; (while≠(y,0) do (*(x,y)=>x; -(y,1)=>y))。
表示当n为任意自然数时，如果该程序执行终止，x的值为n!，这一性质可用{n N}FAC{x=n!}命题表示。
用命题还可表示程序FAC的其它性质，如:{tt}FAC{y=0}命题表示无论初值如何，当程序终止时，y的值为0。
由于命{Φ}P{Ψ}不能保证程序P一定能终止，因此，这种命题也称为程序的部分正确性证明的命题（因为证明程序是否结束是一个递归不可判定问题，即图灵机停机问题。
本文不深入讨论，以下所说的程序正确性证明均指部分正确性证明，在文章的最后再给出正确性证明的补充）。
这种程序正确性的命题如果为真，就称其为Hoare系统中的定理。
那么，如何用公理的方法进行推理呢？设D＝（A，I）是一个演绎系统，其中，A＝（A1，A2，……，A m）表示公理的集合；I＝（I1，I2，……，I n）表示规则的集合。
公理是一个系统中不用证明、预先承认的事实。
如果，S是系统中一条合法的语句，那么，├S表示S为真，即S是系统中的一个定理。
├S1├S2┇├S P├S r表示系统中的一条规则，其含义是if (├S1 and ├S2 and …… and ├S P) then ├S r。
演绎系统中，一个定理的证明就是一个合法的语句序列（要用公理或规则说明为什么该语句是合法的）。
下面举一个著名的、最简单的演绎系统及其推理的例子。
设D g=(A g,I g)，其中A g=(A1,A2,A3)为：A1：├最少由两个点。
A2：├如果P和Q是两个不同的点，那么经过P和Q的线只有一条。
A3：├假如L是一条线，那么存在一个不在L上的点。
I g=(I1,I2)为：I1：├ P├ if P then Q├ QI2：├ P├ Q├ P and Q下面是“├最少有三个点”的证明步骤：1．├最少由两个点 A12．├存在一条线 1，A2，I13．├在线外有一个点 2，A3，I14．├最少由三个点 1，2，I2程序的本质是状态的转换，程序的执行就是从满足前置条件的状态转换到满足后置条件的状态，程序的正确性证明即证明＜2＞。
由于结构化程序设计的任何语法单位均为单入口和单出口的，所以，任何一个结构化的程序设计语言写的程序均可表示为以下的形式：s1；s2；…；s n <4>对∀d0，存在一个状态转换序列：d1,d2,…,d n（d i表示执行语句s i后的状态）。
为了证明<2>，对每一对（s i, s i+1）定义一个谓词断言M i。
显然，可按下面的逻辑推理步骤证明（2）：∀d0├Φ(d0)├Φ(d0)→M1(d1)├M1(d1)→M2(d2)┇├M n-1(d n-1)→Ψ(d n)而证明├M i(d i)→M i+1(d i+1)就是证明：∀d i（假如├M i(d i)，执行语句s i后，├M i+1(d i+1)）。
这样，程序的正确性证明就归结到每条语句的正确性证明。
下面的Hoare逻辑为验证程序中的语句提供了一般性的方法。
Hoare逻辑是这样的一个演绎系统D h=(A h,I h),A h是Hoare逻辑系统中的公理集（这里不再列出）。
I h除了包含一般逻辑系统中的推理规则外，还包括以下与FLOW语言有关的语法语义规则（公理系统中的一般推理规则详见[5]）：(1)├{R} skip {R}(2)├{R[a/x]}a=>x {R}(3)├{R} S1 {O}├{O} S2 {Q}├{R}S1；S2{Q}(4)├{R∧B} S1 {Q}├{R∧⌝B} S2 {Q}├{R} if B then S1 else S2 {Q}(5)├{I∧B} S {I}├{I} while B do S {I∧⌝B}(6)├R→R1├{R1} S {Q1}├Q1→Q├{R} S {Q}要用Hoare逻辑验证一个程序，即所谓的程序正确性证明（证明Hoare系统中的定理），就是用前置条件、逻辑系统中的公理、定理以及上述语言成份所规定的语义规则，按程序的执行步骤推导出后置条件。
