公理语义-Mann子目标Hoare

程序设计形式语义学南京理工大学计算机系张琨二○○四年八月二日程序设计形式语义学2公理语义试图通过在程序逻辑的范围内给出证明规则来确定程序设计构造的含义。该方法的代表人物是R.W.Floyd和C.A.R.Hoare。从一开始，公理语义强调的是正确性证明。2.5程序正确性证明－Manna的子目标断言法美国斯坦福大学的Z.Manna教授在Floyd的不变式断言法的基础上，提出了部分正确性证明的子目标法。子目标法与不变式法的主要区别在于：在断言设置中，不变式法的断言描述程序处理过程中的中间变量与初始值之间的关系，而子目标断言中描述的是中间变量与终值间的关系其归纳推理方向不同。不变式断言法沿程序执行方向正向推理，而子目标法沿程序执行的反方向逆向归纳推理。2.5程序正确性证明－Manna的子目标断言法1.建立输入、输出和循环不变式断言 设x，y的初始值为x0，y0，可分别建立输入断言I、输出断言O、子目标断言如下： I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0) O(x,z):z=gcd(x0,y0) 子目标断言q(x,y,yf):x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)q(x,y,yf)的含义是：每当控制以x和y的容许值通过L时，x，y的当前值的最大公约数将等于y的最终值。2.5程序正确性证明－Manna的子目标断言法2.建立验证条件（采用逆向方法）首先证明当控制最后一次通过L时，即控制转出循环时，子目标断言成立。为此，由x=0退出本循环，要证明验证条件1：C1(x,y):x=0=>q(x,y,yf) 即：x=0=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)其次，证明如果再通过循环后，子目标断言再L处成立，那么，再通过循环之前，断言也成立。为此，要证明下面两个验证条件。由x≠0∧y<x可推出验证条件2，即：C2(x,y):x≠0∧y<x∧q(y,x,yf)=>q(x,y,yf)由x≠0∧y≥x可推出验证条件3，即：C3(x,y):x≠0∧y≥x∧q(x,y-x,yf)=>q(x,y,yf)最后，证明如果输入断言为真，且当控制第一次通过L时子目标断言为真，则输出断言为真。当第一次到达L点时，可推出验证条件4，即：C4(x,y):x0≥0∧y0≥0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)=>yf=gcd(x0,y0)2.5程序正确性证明－Manna的子目标断言法3.证明验证条件验证条件1：C1(x,y):x=0=>q(x,y,yf)q(0,yf,yf) 即：x=0=>[0≥0∧yf≥0∧(0≠0∨yf≠0)=>yf=gcd(0,yf)]。验证条件2：C2(x,y):x≠0∧y<x∧q(y,x,yf)=>q(x,y,yf)即：x≠0∧y<x∧[y≥0∧x≥0∧(y≠0∨x≠0)=>yf=gcd(y,x)]=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)]验证条件3，C3(x,y):x≠0∧y≥x∧q(x,y-x,yf)=>q(x,y,yf)即：x≠0∧y≥x∧[x≥0∧y-x≥0∧(x≠0∨y-x≠0)=>yf=gcd(x,y-x)]=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)]验证条件4，C4(x,y):x0≥0∧y0≥0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)=>yf=gcd(x0,y0)]2.5程序正确性证明－Hoare的公理化方法1969年，Hoare在Floyd的不变式断言法基础上，提出了一种证明程序部分正确性的Hoare公理化方法。根据结构化定理，他提出了顺序语句、条件语句、WHILE循环语句三种基本语句证明规则，试图建立一个不变式演绎系统，以达到程序证明自动化之目的。2.5程序正确性证明－Hoare的公理化方法定义2.8不变式语句

称{P}S{Q}是不变式语句。其含义是：如果执行S之前P为真，并且S执行终止，Q为真，称不变式语句为真或称归纳表达式为真。Hoare公理系统的推理规则一般形式为：其中：B为不变式语句，是逻辑表达式或其他不变式语句，其含义是：为了推论B为真，只需证明前提Ai(i=1,2,…,n)为真。为了证明程序P关于输入条件I(x)与输出条件O(x,p(x))是部分正确的，归结为证明不变式语句{I(x)}P{O(x,P(x))}为真。2.5程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。1.赋值语句公理设有赋值语句y←f(x)，则其公理为：{P(x,f(x,y))}y←f(x){P(x,y)}2.5程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。2.条件语句规则 {P∧R}S1{Q},{P∧﹁R}S2{Q} {P}IFRTHENS1ELSES2{Q} 或 {P∧R}S{Q},{P∧﹁R}=>{Q} {P}IFRTHENS{Q}2.5程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。3.循环语句规则 P=>I,{I∧R}S{I},I∧﹁R=>Q {P}WHILERDOS

{Q} 此规则中的逻辑表达式I就是非形式证明中的循环不变式断言。条件P=>I表明，当控制进入循环时，循环不变式I应为真；不变式{I∧R}S{I}表明，如果执行S之前（R为真时才执行S）I为真，且S执行终止，则S执行后I仍为真；条件I∧﹁R=>Q表明，如果控制退出循环，Q应为真。2.5程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。4.并置规则 {P}S1{R},{R}S2{Q} {P}S1;S2{Q}2.5程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。4.结论规则 P=>R,{R}S{Q} {P}S{Q} 或 {P}S{R},R=>Q {P}S{Q}2.5程序正确性证明－Hoare的公理化方法举例：说明公理化证明程序部分正确性的方法。将该例的输入断言，循环不变式断言和输出断言插入程序中相应位置，则程序体为：STARTI(x):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)}/*输入断言*/(x,y)←(x0,y0);/*x:=x0,y:=y0的缩写*/WHILEx≠0DOL(x,y):{x≥0∧y≥0∧(x≠0∨y≠0)=>gcd(x,y)=gcd(x0,y0)}/*循环不变式*/IFy≥xTHENy←y-xELSE(s,x,y)←(x,y,s)z:=y;O(x,z):{z=gcd(x0,y0)}

/*输出断言*/

2.5程序正确性证明－Hoare的公理化方法要证明程序P是部分正确的，则要证明目标Goal是部分正确的。Goal:{x0≥0∧y0≥0∧(x0≠0∨y0≠0)} BodyP /*体为赋值语句与WHILE-DO的并*/ {z=gcd(x0,y0)}2.5程序正确性证明－Hoare的公理化方法1.按并置规则 根据并置规则分解Goal，需证明两个不变式语句

Goal1:{x0≥0∧y0≥0∧(x0≠0∨y0≠0)} (x,y)←(x0,y0) L(x,y):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)=>gcd(x,y)=gcd(x0,y0}

Goal2:L(x,y) WHILEx≠0DOS; O(x,y):{z=gcd(x0,y0)}2.5程序正确性证明－Hoare的公理化方法2.由赋值公理证Goal1，只需证明逻辑表达式

Log1:x0≥0∧y0≥0∧(x0≠0∨y0≠0)=>L(x0,y0)2.5程序正确性证明－Hoare的公理化方法3.使用WHILE-DO规则证明Goal2。根据WHILE规则，可取I为L(x,y)，则显然L(x,y)=>I，于是有：

Goal3:{L(x,y)∧x≠0} IFy≥0THEN...ELSE...{L(x,y)}2.5程序正确性证明－Hoare的公理化方法4.由x=0，执行z←y分支，需证明逻辑表达式：

Log2:L(x,y)∧x=0)=>z=gcd(x0,y0)

2.5程序正确性证明－Hoare的公理化方法5.根据条件规则，为了证明Goal3，则需证明：

Goal4:{L(x,y)∧x≠0∧y≥x}y←y-x{L(x,y)}

Goal5:{L(x,y)∧x≠0∧y<x}(s,x,y)←(x,y,s){L(x,y)}

2.5程序正确性证明－Hoare的公理化方法6.根据赋值公理，为了证明Goal4、Goal5，只需证明表达式：Log3:L(x,y)∧x≠0∧y≥x)=>L(x,y-x)Log4:L(x,y)∧x≠0∧y<x)=>L(y,x)推理演绎树因此，证明Goal归结为证明落及表达式Log1,Log2,Log3,Log4。这四个逻辑表达式正好是Floyd证明方法中的四个验证条件，证明过程省略。讨论：利用Hoare的公理化方法证明下述程序的部分正确性。

2.5程序正确性证明－良序集方法（证明程序终止性）R.W.Floyd在1967年提出来的。设程序P的输入断言为φ(x)，利用良序集方法证明P关于φ(x)是终止的可按以下步骤进行：1.选取一个点集去截断程序的各个循环部分，并且在每一截断点i处建立一个中间断言qi(x,y)。程序就被分解为若干条通路，同时规定每一条通路都不包含有中间截断点；2.选取一个良序集(W,)，并且在每一截断点i处定义一个终止表达式Ei(x,y)；3.证明所选取的断言是“良断言”。即满足：1）若对于每一个从程序入口到断点i的通路α有：φ(x)∧Rα(x,y)=>qi(x,rα(x,y))2）若对于每一个由断点i到断点j的通路α有：qi(x,y)∧Rα(x,y)=>qj(x,rα(x,y))这里，Rα和rα分别表示通过通路α的条件及通过通路α后变量y的值。4.证明终止表达式是“良函数”。即对于每个断点i有qi(x,y)=>Ei(x,y)∈W5.证明终止条件成立。即对每一条从断点i到断点j，并且为某个循环的一部分的通路α有：qi(x,y)∧Rα(x,y)=>[Ei(x,y)Ej(x,rα(x,y))ϒϒ良序集：设(W,)是一个偏序集（满足传递、反对称和反自反性），如果不存在由W中的元素构成的无限递减序列a0a1a2…则称(W,)为良序集。ϒϒϒϒ例：另一个计算两个正整数x1,x2的最大公约数的程序。输入、输出断言为：φ(x):x1>0∧x2>0Ψ(x,z):z=gcd(x1,x2)终止性证明1）在Ｂ，Ｃ点将循环断开，并在这两点分别建立中间断言。2）取良序集为(N,<)，并在Ｂ、Ｃ点分别建立终止表达式。3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）4）证明终止表达式是良函数。5）证明终止条件成立。即对与循环有关的通路展开证明。1）在Ｂ，Ｃ点将循环断开，并在这两点分别建立中间断言。qB(x,y):y1>0∧y2>0qC(x,y):y1>0∧y2>02）取良序集为(N,<)，并在Ｂ、Ｃ点分别建立终止表达式。EB(x,y):y1EC(x,y):y1+2y23）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）1.通路α1(AB)φ(x)=>qB(x,y)qB(x,x1,x2,1)即：x1>0∧x2>0=>x1>0∧x2>0

3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）2.通路α2(BDB)qB(x,y)

∧y1是偶数∧y2是偶数=>qB(x,y)qB(x,y1/2,y2/2,2y3)即：y1>0∧y2>0∧y1是偶数∧y2是偶数=>y1/2>0∧y2/2>0

3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）3.通路α3(BEB)qB(x,y)

∧y1是偶数∧y2是奇数=>qB(x,y)qB(x,y1/2,y2,y3)即：y1>0∧y2>0∧y1是偶数∧y2是奇数=>y1/2>0∧y2>0

3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）4.通路α4(BＣ)qB(x,y)

∧y1是奇数=>qC(x,y)即：y1>0∧y2>0∧y1是奇数=>y1>0∧y2>0

3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）5.通路α5(CKＣ)qC(x,y)

∧y1是奇数∧y2是偶数=>qC(x,y)qC(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是奇数∧y2是偶数=>y1>0∧y2/2

>0

3）证明中间断言是良断言。由于循环由Ｂ，Ｃ点断开后，程序分解为７条通路，因此需分别对前６条通路予以证明。（通路Ｃ－>Ｈ与证明终止性无关）6.通路α6(CGKＣ)qC(x,y)

∧y1是奇数∧y2是奇数∧y1

≠y2

=>qC(x,y)qC(x,y2,|y1-y2|/2,y3)即：y1>0∧y2>0∧y1是奇数∧y2是奇数∧y1

≠y2

=>y2>0∧|y1-y2|/2

>0

以上6个蕴涵式都是显然成立的。这样就证明了qB(x,y)，qC(x,y)是良断言。4）证明终止表达式是良函数。qB(x,y)=>EB(x,y)∈NqC(x,y)=>EC(x,y)∈N即要证y1>0∧y2>0=>y1∈Ny1>0∧y2>0=>y1+2y2∈N由于y1和y2均为整数，所以这两个关系是显然成立的。5）证明终止条件成立。即对与循环有关的通路展开证明。与循环有关的通路是:α2(BDB)α3(BEB)α5(CKＣ)α6(CGKＣ)分别予以证明。5）证明终止条件成立。即对与循环有关的通路展开证明。α2(BDB)qB(x,y)

∧y1是偶数∧y2是偶数=>EB(x,y1,y2,y3)>EB(x,y1/2,y2/2,2y3)即：y1>0∧y2>0∧y1是偶数∧y2是偶数=>y1>y1/25）证明终止条件成立。即对与循环有关的通路展开证明。α3(BEB)qB(x,y)

∧y1是偶数∧y2是奇数=>EB(x,y1,y2,y3)>EB(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是偶数∧y2是奇数=>y1>y1/25）证明终止条件成立。即对与循环有关的通路展开证明。α5(CKＣ)qC(x,y)

∧y1是奇数∧y2是偶数=>EC(x,y1,y2,y3)>EC(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是奇数∧y2是偶数=>y1+2y2>y1+y25）证明终止条件成立。即对与循环有关的通路展开证明。α6(CGKＣ)qC(x,y)

∧y1是奇数∧y2是奇数∧y1

≠y2

=>EC(x,y1,y2,y3)>EC(x,y2,|y1-y2|/2,y3)即：y1>0∧y2>0∧y1是奇数∧y2是奇数∧y1

≠y2

=>y1+2y2>y2+|y1-y2|上述终止条件显然成立。这样，即证明了程序的终止性。讨论：利用良序集方法证明下述程序的终止性。

2.5程序正确性证明－Kunth的计数器方法D.E.Kunth于1968年提出了证明程序终止性的计数器方法。该方法直观易懂，其证明过程分为三步：1.为程序中的每个循环附加一个新的变量（如i，j通常被称为计数器），进入该循环前计数器置0，每执行一次循环计数器累加1；2.为每个循环设置一个中间断言，它表明相应的计数器不会超过某个固定的界限；3.进一步证明第2步设置的中间断言是不变式断言。2.5程序正确性证明－Kunth的计数器方法举例：对前述证明部分正确性z=gcd(x,y)的例子，用计数器方法证明其终止性。证明：输入断言I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0)1.引入计数器i，并根据程序语义设置断言为：

x≥0∧y≥0∧2x+y+i≤2x0+y0

即计数器i不会超过界限2x0+y0。PROGRAMgcd1;VARx,y,z,s:INTEGER;BEGINREAD(x,y);i:=0;I(x):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)}WHILEx≠0DOL(x,y):{x≥0∧y≥0∧2x+y+i≤2x0+y0}BEGIN

IFy≥xTHENy←y-xELSE(s,x,y)←(x,y,s)i←i+1END;z←yEND;2.5程序正确性证明－Kunth的计数器方法证明：输入断言I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0)2.建立验证条件： 第一次到达循环语句Ｌ处，仅执行了赋值语句：x=x0;y=y0;i:=0;

C1(x,y):[x0≥0∧y0≥0∧(x0≠0∨y0≠0)] =>[x0≥0∧y0≥0∧2x0+y0+0≤2