我要投搞

标签云

收藏小站

爱尚经典语录、名言、句子、散文、日志、唯美图片

当前位置:2019跑狗图高清彩图 > 指称语义 >

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

归档日期:09-06       文本归类:指称语义      文章编辑:爱尚语录

  形式化方法--程序的正确性验证-14_计算机软件及应用_IT/计算机_专业资料。第十四讲 形式化方法--程序的正确性验证 一、概述 计算机的程序是一种静态的对象, 但它所描述的问题 (问题的解) 却是一个动态的对象。 所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状

  第十四讲 形式化方法--程序的正确性验证 一、概述 计算机的程序是一种静态的对象, 但它所描述的问题 (问题的解) 却是一个动态的对象。 所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态, 构造所描述问题 的动态行为。 这是不自然的, 程序所描述的动态行为也无法直接用程序本身的静态结构进行 正确性证明。 形式化规约(formal specification)是需求阶段的形式化说明,是用户需求的严格描述, 其一般形式用 Hoare 逻辑描述[1]如下: ├{Φ }P{ } 1 其中Φ 和 分别表示初始和结束断言条件,其含义是: “假如初始状态 dI 满足条件Φ ,那么 程序结束并且终结状态 df 必须满足 ” 。 设 D=D1×??×Dn 为程序 P 的状态空间,其中,Dj(j=1,??,n)表示程序中数据对象 的值域。显然,由Φ 和 断言条件所确定的合法初始和结束状态的集合是 D 的一个子集。 执行函数 E:Φ ×P→ 定义如下: 无定义 对合法的初始状态 di,程序 P 不结束 E(P,dI)= 终结状态 df 对合法的初始状态 di,程序 P 结束 程序的正确性即为: ├{Φ }P{ } iff 2 ?di(├Φ (di)→(├程序 P 结束 and ├ (E(P,di)))) 总地来讲,验证一个程序的正确与否有两种办法,一种是程序的测试,另一种是程序的 正确性证明。 1. 程序的测试与程序的验证 对给定的一个合法的初始状态 di,当程序执行结束时其终结状态为 df,那么,Φ (di)和 (df)都应该被满足。这一点可用下式表示: {di}P{df} 3 所谓程序的测试就是验证测试用例{di}P{df}, 即验证程序对 di 的执行结果是否为 df。 由 于合理的初始状态是无限的,因此,对程序验证来讲,测试不是一个完备的方法。测试被认 为是一种尽量发现错误,但并不能保证程序中没有错误[2]的方法。对大数应用来讲,它是 可满足的;但对有些应用来讲,测试是一种不能满足的验证方法,例如:航空、航天等领域 的软件系统。 显然,对要求绝对正确的软件,测试是一种不能采用的方法。无论白盒测试还是黑盒测 试都是在无限集合{(di,df)?di,?df, di 和 df 满足{di}P{df}中选择有限的一些(di,df)对进行验证, 而各种测试方法只是选择(di,df)的策略不同而已。 因此,验证程序是否完全正确要寻求另外的解决途径。那就是程序的正确性验证。 2. 形式语义与程序的正确性验证 程序的正确性验证应该具有严密的推量过程,以保证程序每步执行结果都是希望的结 果,而与程序执行的某个初始状态无关。程序的正确性证明现有三种方式:操作语义、指称 1 1 语义和公理语义。它们分别用不同的形式化方法,严格地证明一个程序是否正确。尽管这种 方法还不够完善,还不为一般软件人员所掌握,但它确实是保证软件绝对正确的唯一途径。 操作语义(Operational Semantics) 操作语义的根据是, 一种程序设计语言一但在某种计算机系统中实施, 其语义的含义也 就完全确定下来了,因此,自然地就用语言的实施作为语言含义的定义,故称这种语义为操 作语义。 当然,这种实施应该在一种标准的、抽象的机器上进行。英国科学家din 最早提 出这种类型的一个抽象机器,称为“栈-环境-控制-外存” 。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]。另一种方法是自底向上的,根据每个 语言单元定义的前置断言和该成份本身的特征, 推导出其后置断言。 一个语法单元的后置断 2 2 言可作为下一个语法单元的前置断言, 从而揄出整个程序的后置断言, 以此可证明程序应满 足的性质和程序的正确性。 二、公理系统: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,??,Am)表示公理的集合;I=(I1,I2,??,In)表示规则的集合。公理是一个系 统中不用证明、预先承认的事实。如果,S 是系统中一条合法的语句,那么, ├S 表示 S 为真,即 S 是系统中的一个定理。 ├S1 ├S2 ┇ ├SP ├Sr 表示系统中的一条规则,其含义是 if (├S1 and ├S2 and ?? and ├SP) then ├Sr。 演绎系统中, 一个定理的证明就是一个合法的语句序列 (要用公理或规则说明为什么该 语句是合法的) 。下面举一个著名的、最简单的演绎系统及其推理的例子。 设 Dg=(Ag,Ig),其中 Ag=(A1,A2,A3)为: A1:├最少由两个点。 A2:├如果 P 和 Q 是两个不同的点,那么经过 P 和 Q 的线:├假如 L 是一条线,那么存在一个不在 L 上的点。 Ig=(I1,I2)为: I1: ├ P ├ if P then Q ├ Q I2: ├ P ├ Q ├ P and Q 3 3 下面是“├最少有三个点”的证明步骤: 1.├最少由两个点 A1 2.├存在一条线 程序的本质是状态的转换, 程序的执行就是从满足前置条件的状态转换到满足后置条件 的状态,程序的正确性证明即证明<2>。由于结构化程序设计的任何语法单位均为单入口 和单出口的,所以,任何一个结构化的程序设计语言写的程序均可表示为以下的形式: 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)就是证明: ?di(假如├Mi(di),执行语句 si 后,├Mi+1(di+1)) 。 这样, 程序的正确性证明就归结到每条语句的正确性证明。 下面的 Hoare 逻辑为验证程 序中的语句提供了一般性的方法。 Hoare 逻辑是这样的一个演绎系统 Dh=(Ah,Ih),Ah 是 Hoare 逻辑系统中的公理集(这里不 再列出) 。Ih 除了包含一般逻辑系统中的推理规则外,还包括以下与 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 系统中的定理) , 就是用前置条件、逻辑系统中的公理、定理以及上述语言成份所规定的语义规则,按程序的 执行步骤推导出后置条件。 下面是应用 Hoare 逻辑,对归纳命题{n∈N}FAC{x=n!}的证明过程: 1.n?N 前置条件 4 4 2.n?N ? l=1 1,?+ 3.l=x; FAC 的第一条语句 4.n?N ? x=1 2,3,规则(2) 5.n?N ? x=1 ? n=n 4, ?+ 6.n=y; FAC 的第二条语句 7.n?N ? x=1 ? y=n 5,6,规则(2) 8.{?k?N(n?N ? x=1*n*?*(n-(k-1)) ? y=n-k)} 7?8,令 8 为规则 5 的 I 9.{y?0} 6?9,令 9 为规则 5 的 B 10.{?k?N(n?N ? x*y=1*n*?*(n-(k-1))*y ? y=n-k)} 8,9 11.*(x,y)=x; 循环的第一条语句 12.{?k?N(n?N ? x=1*n*?*(n-(k-1))*(n-k) ? y=n-k)} 10,11,规则 2 13.{?k?N(n?N ? x=1*n*?*(n-(k-1))*(n-k) ? y-1=n-(k+))} 12,12?13 14.-(y,1)=y; 循环的第二条语句 15.{?k?N(n?N ? x=1*n*?*(n-(k-1))*(n-k) ? y=n-(k+1))} 13,14,规则 2 16.{?k?N(n?N ? x=1*n*?*(n-(k-1)) ? y=n-k)} 15?16 17.{I ? B}*(x,y)=x; -(y,1)=y; {I} 10,11,13,14,16,规则 3 和 6 18.(while?(y,0) do *(x,y)=x; -(y,1)=y) FAC 的第三条语句 19.{?k?N(n?N ? x=1*n*?*(n-(k-1)) ? y=n-k) ?? (y?0)} 17,18,规则 5 20.x=n! 规则 6,19?20 可见,用 Hoare 逻辑进行推理与一般的逻辑系统的推理是一样的。对 FLOW 语言写的程 序, 用 Hoare 逻辑证明其正确性的难点是 while 语句。 证明 while 语句的办法就是寻找适当 的循环不变量(证明某个循环语句时, 它的循环不变量既要利用前面的推理结果和其它条件, 也要为后续的证明提供必要的前置条件),其数学基础是不动点理论。注意:在证明循环语 句的正确性时, 并不要求循环不变量在循环体内的证明过程中的每一点上都满足, 它只是要 求在循环体的前和后保持不变即可; 另外, 不变量在每次循环前后的形式一样, 但其 “含义” 是不一样的,是要发生变化的。一般情况下,循环不变量的设计是与该循环的循环变量相关 的、与循环体中包含的语句的语义相关。 以 Hoare 逻辑为代表的传统的公理证明方法的弱点是:程序本身描述的行为是动态的, 是随时间变化的对象; 而逻辑本身是一个研究静态对象的数学理论, 它不能表达状态的变化。 由于程序的本质是用语句改变程序变量的状态, 使程序执行前的初始状态一步一步地变为希 望的终结状态的过程,因此,用这种逻辑进行描述程序的性质是不自然的,也是不直观的。 另一个用 Hoare 逻辑进行推理的弱点就是推理的方向性。 用 Hoare 逻辑验证程序的正确 性,就是要构造满足5的 M1,M2,?,Mn:序列。这就像从入口进入迷宫一样(已知 M1) , 要达到出口是很难的(寻找 Mn ) 。由于有规则 6 ,有人提出了最弱前置条件 (weaskest precondition)逆向推理的办法。其基本思想是:设一条语句 S 和一个该语句执行后满足的 断言 Q,那么,能使{R}S{Q}成立的 R 很多,我们把其中最弱的一个 R 记为:wp(S,Q)。这样, 我们就可以根据一个给定的程序的最后一条语句和程序最终的断言 , 倒着一步一步地推出 整个程序唯一的最弱前置条件,记为 wp(S, )。设该程序 P 的归纳命题的前置断言为Φ , 如果Φ →wp(P, ),那么,原命题成立,即它是 Hoare 系统中的一个定理。 按照这一思路,我们也可以设置相对应的最强后置条件 (strongest postcondition): 对给定的语句 S 和一个该语句执行前满足的断言 P,能使{P}S{Q}成立的 Q 很多,我们把其 中最强的一个 Q 记为 sp(P,S)。对程序 P 的 Hoare 逻辑的命题{Φ }P{ },从给定程序的第 一条语句和程序的前置断言Φ 开始,一步一步地推出整个程序最后一条语句的最强后置条 件,记为:sp(Φ ,P)。如果 sp(Φ ,P)→ ,那么,命题{Φ }P{ }亦成立。还有一种办法就 5 5 是,从前向后推出该程序的前缀?P 的最强后置条件 sp(Φ ,?p);同时,从后向前推出该程序 后缀 P?的最弱前置条件 wp(P?, )。 当两个方向的推理交汇时, 如果 sp(Φ ,?p) → wp(P?, ), 则命题得证。 寻求 wp(P, )和 sp(Φ ,P)在理论经上是可行的,但实际操作起来却是相当困难和费时 的。这就使得用 Hoare 逻辑的方法证明程序的正确性有相当的难度,这主要是因为 Hoare 逻辑采用的元语句是命题逻辑, 它本身是研究静态对象的, 而程序变化的本质规律是变量空 间状态的变化,程序的执行是一种动态现象,所以才产生了上述的困难。Hoare 逻辑只能描 述了某一时刻(当前的)状态,而与其它状态无关。 为了能直接描述程序状态变化的本质, 我们需要另一种逻辑体系来描述这种随时间变化 而变化的状态信息。时态逻辑就是能描述变量随时间变化而变化的逻辑系统。显然,用时态 逻辑可描述程序的动态语义,而且比较直观。 时态逻辑是公理语义的程序正确性证明的一个分支。时态逻辑是由以色列科学家 A.Pnueli 和 Z.manna 等人创立的,由于在传统的逻辑中增加了上一时刻、下一时刻等算子, 使它能描述程序的历史和将来的状态, 从而可描述程序的性质, 并进行逻辑推导以验证程序 的正确性。 下面介绍时态逻辑,以及用时态逻辑证明程序正确性的方法。 设有穷变元集合 V={x1,x2,?,xn}构成的变元组的值(x1,x2,?,xn)为状态 s,s(xi)表示 xi 在状态 s 下的值,在一定的上下文中 s(xi)可简写为 xi。同样,s(e)表示表达式 e 在状态 s 下 的 值 ( 对 表 达 式 e(xi1,xi2, ? ,xim), 定 义 s(e(xi1,xi2, ? ,xim) ≡ e(s(xi1),s(xi2), ? , s(xim)))。令σ =(s0,s1,?,sk,?)为模型,s0 表示当前状态,s1 表示下一个状态,等等。 在时态逻辑中,原子、公式和连接词?、?、?、?、?以及作用于非时态变元的?和?与 一般的逻辑系统相同[5]。时态连接词又分为将来(Future)和过去(Past)两大类。将来时态 连接词及其含义为: Next (○): (?,j)╞ ○p iff (?,j+1)╞ p Henceforth(□): (?,j)╞ □p iff ?k,k?j (?,k)╞ p Eventually(◇): (?,j)╞ ◇p iff ?k,k?j (?,k)╞ p Until(?): (?,j)╞ p?q iff ??k,k?j(?,k)╞ q and ?i,k?i?j (?,i)╞ p Unless(?): (?,j)╞ p?q iff (?,j)╞ p?q or (?,j)╞ □p (?,j)╞ ?u:p iff ???,??是?的 u-变体(??,j)╞ p (?,j)╞ ?u:p iff ???,??是?的 u-变体(??,j)╞ p 注: (?,0)╞ p 可简写为?╞ p 其中,最重要的是?和?,其它的时态连接词均可用他们表示,如: □p≡p?f ◇p≡?□?p p?q≡(p?q)?◇q 过去时态连接词也有对应的一组时态公式⊙、?、?、ε 和β 等,详见[6]。 同其它演绎系统一样, 用时态逻辑进行演绎的系统可表示为 Dt=(At,It),At 除包括一般逻 辑系统中的公理外,还包括以下八条将来公理和八条过去公理: FX0:□p→p FX1:○?p??p FX2:○(p→q)? (○p→○q) FX3:□(p→q)? (□p→□q) FX4:□p→□○p FX5:(p?○p) →(p?□p) 6 6 FX6:p?q?(q?(p?○(p?q))) FX7:□p?p?q FX8:p?○⊙p 八条过去公理不再列出,详见[6]。 It 表示时态逻辑演绎系统的规则(P 表示程序,p 表示某个公式或性质) : RX1(GEN): P╠p P╞□p RX2(SPEC): P╞□p P╠p RX3(INST): P╠p P╞□p[α ] RX4(MP): P╞(p1???pn)→q, P╞p1,?,P╞pn P╞q RX5(p-TAU):?P,?p,p 是合法的状态公式 P╠p It 中还包括其它一些推导出的规则、量词规则和一阶谓词规则等,详见[6]。这些均被称为 一般规则,还有一类与程序有关的规则: RX6(INIT): ╠?→p P╞p RX7(STEP): ╠{p}T{q} P╞(p?○q) 由以上两公式还可推出: RX8(S-INV): ╠?→p,╠{p}T{p} P╞□p 令 Xp: ??(□∨taken (?))?diligent?∧just(?)?∧compassionate(?)表示程序 P 时态语义, ??T ??J ??C 则有如下语义公理: RX9(T-SEM): P╞Xp 如果 XP→P,那么: 1. P╞Xp→p RX5 2. P╞Xp RX9 3. P╞p 1,2,RX4 也就是说,只要证明了 P╞XP,以及在时态逻辑系统下的 XP→P,就可论证一程序的性质 P ╞p。即只要论证了一个程序 P 的语义 XP,其它的性质均可推出。 程序的性质可分为若干层次类型, 每种类型可用一个时态逻辑公式模或描述, 该类型的 ω 性质均可用该模式说明,并有一套相关的证明方法。设Σ 为状态的集合,Σ 为所有可能的 ω 状态序列,那么,一个程序的性质 P 就是Σ 的一个子集。一个时态公式?说明了一个程序 的性质,当且仅当,???P,?╞?。时态公式的形式不同可反映不同的程序性质。 安全性(Safety Properties)所有等价于□p 形式的公式被称为安全公式,它描述的性 质被称为安全性。它反映了程序执行中某些不变的性质。其中一种称为条件安全性:p→□ q(等价形式为□(?( p?first)→q)表明,当 p 满足计算模型初态时,该计算模型具有不 变的性质 q。保证性(Guarantee Properties)所有等价于◇p 形式的公式被称为保证公式, 它描述的性质被称为程序的保证性。 它所映了程序执行中一定发生的性质, 例如: ◇termial。 n 责任性(Obligation Properties)所有等价于∧ i=1(□pi?◇qi)形式的公式被称为责任公式, 它描述的性质被称为责任性。响应性(Response Properties)所有等价于□◇p 形式的公式 7 7 被称为响应公式,它描述的性质被称为响应性。它描述了某些性质出现了无数次。持久性 (Persistence Properties)所有等价于◇□p 形式的公式被称为持久公式,它描述的性质 被称为持久性。它描述了程序中某些最终变稳定的性质。反应性(Reactivity Properties) 所有等价于□◇p?◇□p 形式的公式被称为反应公式,它描述的性质被称为反应性。这些性 质之间的关系如下图所示(连线表示包含关系) : Reactivity Response Persistence Obligation Reactivity Safety Safety Guarantee 将非安全性的性质称为进展性。 进展性中都包含◇, 它们之间的不同是初始条件和相应 的性质发生的频率不同。 安全性强调某个要求在计算过程中一直满足, 它可表达某些坏的性 质不发生;而进展性可表示某些好的性质一定会发生。 程序的部分正确性的时态逻辑公式为: Φ →□(程序结束→ ) 它等价于: □(程序结束∧?(first∧Φ )→ ) 〈6〉 可见程序的部分正确性是一个安全性问题。要证明〈6〉 ,即要证明〈6〉在一个程序所能访 问的状态(P_accessible states)中都是可满足的。由于程序的可访问状态均是执行一个程 序的语句而得到的,因此, 〈6〉的证明可归纳于程序的语句的证明。 FLOW 语言中各语句的时诚语义如下: 1.空语句 (1:skip 1’) ?1:move (1,1’)∧Pres(Y) 其中,?1 表示可能的程序状态转换关系,Y 表示程序中的所有变量,Pres(Y)表示集合 Y 的 值保持不变。以下相同。 2.赋值语句 (1:a=x 1’: ) ?1:move (1,1’) ? x’=a ? Pres(Y-x) 3.条件语句 (1:if c then l1:S1 else l2:S2) T F ?1:? 1?? 1 其中, ?T1:move(1,11) ? c ? Pres(Y) ?F1:move(1,12) ?? c ? Pres(Y) 4.循环语句 (1:[while c do [1:S]];1’: ) T F ?1:? 1?? 1 8 8 其中, ?T1:move(1,1) ? c ? Pres(Y) ?F1:move(1,1) ?? c ? Pres(Y) 即对一个程序的语句,按上述规定的语义,验证一个□p 类型的安全性(程序的部分正 确性)在变换后还都满足。即采用如下的规则(INV_B) : ?→? {?}T{?} □? 其它的一些规则也可用于证明程序的正确性,如:MON_I, CON_I 规则等。 但值得一提的是, 一个程序的部分正确性并非总是可归纳的。 例如, [7]中图 1.2 的例子。 为此,可采用一个更强的断言(INV) ,增量式(SV_PSV)证明等策略。 下面用时态逻辑验证 FAC 的□{?k?N((n?N?y=n)→(x=1*n*?*(n-(k-1))?y=n-k))}性 质,令 p 为?k?N((n?N?y=n)→(x=1*n*?*(n-(k-1))?y=n-k)),下面逐一验证 FAC 的语句: 1=x; n=y; (while≠(y,0) do *(x,y)=x; -(y,1)=y)。 1.T→p 前提 2.p 1=x p y=n 不成立,执行后 x=1 3.p n=y p 执行后 y=n,存在 k=n 使 p 成立 4.P*(x,y)=x p 3?y?0,执行循环体的第一条语句,由于 y=n-k 和 x*y=1*n*?*(n-(k-1))*y 所以,执行该语句后 x=1*n*?*(n-(k-1))*(n-k)。又 y=n-k,得 y-1=n-(k+1) 所以 p 成立。 5.p-(y,1)=y p 执行该语句后 y=y-1,由 y-1=n-(k+1)得 y=n-(k+1)所以 p 成立。 6.p(while?(y,0) do *(x,y)=x; -(y,1)=y) p 4,5 7.□p 由规则 INV_B,此时,循环结束=(y,0),那么 k=n,所 以 x=1*n*?*1,即 x=n! 上述的验证方法还没有脱离一般逻辑系统验证程序的思路, 只是验证的具体方式和规则 变了。用时态逻辑还有另一种验证正确性的思路:因为,时态逻辑可以表示状态的变化,我 们可以把一种适合于冯.诺依曼型计算机进行计算的程序设计语言翻译成时态逻辑公式。例 如,令: ;表示顺序算了,即控制自动转向下一个语句的句首。 Ox=a:表法系统中 x 的值下一个时刻为 a,而其它变量的值不变。 LB=y:表示当前执行语句的标号为 y 下面是 FLOW 语言翻译成时态逻辑公式的规则[参见 4]: 1:skip 1’: LB=1→OLB=l’; 1:a=x 1’: LB=1→(OLB=l’?○x=a); l:[if c then l1: S1 else l2: S2]l’:((LB=l?c) →S1)?((LB=l??c) →S2); l:[while c do [l: S]]l’: ((LB=l?c) →S?LB=l)?((LB=l??c) →LB=l’); 对一个用 FLOW 语言写的程序,用上面的规则将其变换为时态逻辑公式的序列。由于 FLOW 的语句变成了时态逻辑公式, 因此可在逻辑系统中, 验证该程序是否和其规范等价 (用 Hoare 逻辑只能验证一个性质, 但不能证明该性质是否与其规范等, 这是因为在 Hoare 逻辑系统中, 一条语句和{P}s{Q}等价,{P}s{Q}不是逻辑公式,它不能参加逻辑推理),从而验证相应的 FLOW 程序的正确性。 设 A 表示一段程序 P 的规范,TL 表示 P 相应的一组时态逻辑公式,现已有成形的、机 9 9 械的方法证明 TL ╞A,但无证明 A╞TL 的自动化方法[参见 4],只能用手工的方法论证。这 种方式总的来讲是先有程序, 然后再根据它的规范来验证该程序的正确性。 唐稚松先生将其 称为“马车置于马的前方” 。他认为应该先有软件的规范,然后根据规范得到软件的实现。 他创立了一套基于时态逻辑的 XYZ/E 系统,软件的规范(用抽象的 XYZ/AE 表示)和软件 的实现(用可执行的 XYZ/EE 表示)都可在同一时态逻辑系统下表达,并且也可表达即含 XYZ/AE,也含 XYZ/EE 的中间形式的混合描述。这样,从最初的规范到最后的可执行程序, 形成了一个逐步细化的时态逻辑描述序列: S1,S2,?,Sn 只要保证 S1 是正确的,且 Si+1╞Si,那么,Sn 就一定是对 S1 的正确实现。这种逐步求精 的思想就是本文最开始提到的自顶向下的方法,它符合软件工程的一般原理和工程化的需 要。 用时态逻辑还可证明更复杂的程序性质,如:并行程序的性质、死锁问题等等。 下面对程序的完全正确性证明作补充说明,程序的完全正确性证明[2],即在证明程序 的部分正确性的同时,也要证明程序能正常结束。由于结构化语言的特殊性,即它只由顺序 语句、 分叉语句和循环语句等三种类型的语句组成, 而顺序语句和分叉语句执行后一定结束, 所以,程序能否结束就是要证明程序中的所有循环语句能否正确结束。Dijkstra 为程序的 循环语句的完全正确性证明定义了下面的规则: (7’) ├{I?B}S{I} ├{I?B?t?t0+1}S{t?t0+1} ├{I?B}→├t?0 ├{I}while B do S {I??B} 其中, 前提条件的第一条语句同 Hoare 逻辑的第七条规则: 第二条语句要求存在一个递减的、 有界的良序集;第三条语句保证,当 t 递减到一个最小数时,循环结束。一般地,t 的设计 与循环变量有关,所不同的是循环变量可以递增,也可以递减,但 t 永远被设计为递减的。 例如,上面用 Hoare 逻辑对 FAC 函数的证明中,令 t(y)=y, S 为(*(x,y)=x; -(y,1)=y), 则 FAC 的完整性证明为(FAC 的 Hoare 逻辑证明续): 21.├t(y-1)?t0 ≡├y-1?t0 ≡├n-y-1?t0 FAC 中的语句-(y,1)=y ≡├n-y?t0+1 ≡├t(y)?t0+1 22.├{t?t0+1}-(y,1)=y {t?t0} 21 23.├{t?t0+1} S {t?t0} 22,循环体中只有-(y,1)=影响 t 24.├{I?B}→├t?0 23,9 25.├{I}while B do S {I??B} 规则(7’) ,17,23,24 26.├FAC 结束 and ├x=n! 20,25,FAC 只有一个循环 三、结束语 程序验证是软件工种中一个非常重要的理论问题,Hoare 逻辑被认为是最有效的程序验 证工具之一。然而,Hoare 逻辑对一段程序(语句、程序段)的描述{P}S{Q}不是逻辑公式, 不能参加逻辑推理。另外,程序的本质是基于冯诺依曼计算机的状态转换,Hoare 逻辑中采 用的传统逻辑系统却无法表达状态转换。 这两点极大地限制了 Hoare 逻辑在程序验证中的地 位和作用。由以色列学者 Z.Manna 和 A.Pnueli 创立的时态逻辑,由于引入了下一时刻(口) 算子, 可表达程序中的状态转换, 并且基于时态逻辑的{P}S{Q}描述也是一个时态逻辑公式, 10 10 它为程序的逻辑系统中的推演奠定了坚实的基础。 参考文献 1.Robert V.Binder. Testing Object-Oriented System: models, pattern, and tools. Addison Wesley Longman, 2000 2.周巢尘。形式语义学引论。计算机研究与发展,1985,22(7,8) 3.H.K.Berg, W.E.Boebert, W.R.Franta, T.G.moher. Formal Methods of Program verification and Specification. Prentice-Hall, 1982 4.唐稚松。时态逻辑程序设计和软件工程(手稿) 。1999 5.胡世华,陆钟万。数理逻辑基础。科学出版社,1982 6.Z.Manna A.Pnueli The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992 7.Z.Manna A.Pnueli Temporal verification of Reactive Systems: Safety. Springer-Verlage, 1995 11 11

本文链接:http://capstonebake.com/zhichenyuyi/490.html