公理语义-Mann子目标Hoare

1、程序设计形式语义学程序设计形式语义学南京理工大学南京理工大学 计算机系计算机系张琨张琨二二四年八月二日四年八月二日2 公理语义公理语义2.5 程序正确性证明程序正确性证明Manna的子目标断言法的子目标断言法2.5 程序正确性证明程序正确性证明Manna的子目标断言法的子目标断言法n3. 证明验证条件证明验证条件n验证条件验证条件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) 。 n验证条件验证条件2： C2(x,y): x 0 y q(x,y,yf) 即：即： x

2、0 y yf = gcd(y, x) = x 0 y 0 (x 0 y 0 ) = yf = gcd(x,y)n验证条件验证条件3， C3(x,y): x 0 y x q(x,y-x,yf) = q(x,y,yf) 即：即： x 0y xx0y-x 0(x 0 y-x 0 )=yf=gcd(x,y-x) = x 0 y 0 (x 0 y 0 ) = yf = gcd(x,y)n验证条件验证条件4， C4(x,y): x0 0 y0 0 (x0 0 y0 0 ) q(x0,y0,yf) = yf = gcd(x0,y0) BAAAn,212.5 程序正确性证明程序正确性证明Hoare的公理化方法

3、nHoare提出的公理和相应控制语句的证明规则。提出的公理和相应控制语句的证明规则。n4. 并置规则并置规则P S1R,R S2 QP S1;S2 QGoal Goal1 Goal2 Goal Goal1 Goal2 Log1 Goal Goal1 Goal2 Log1 Goal3 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal4 Goal5 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal4 Goal5 Log3 Log4 nR.W.Floyd在在1967年提出来的。设程序

4、年提出来的。设程序P的输入断言为的输入断言为(x)，利用良序集方法证明，利用良序集方法证明P关于关于(x)是终止的可按以下步骤进行：是终止的可按以下步骤进行：n1. 选取一个点集去截断程序的各个循环部分，并且在每一截断点选取一个点集去截断程序的各个循环部分，并且在每一截断点i处建立一个中间断言处建立一个中间断言qi(x,y)。程序就被分解为若干条通路，同时规定每一条通路都不包含有中间截断点；。程序就被分解为若干条通路，同时规定每一条通路都不包含有中间截断点；n2. 选取一个良序集选取一个良序集(W, )，并且在每一截断点，并且在每一截断点i处定义一个终止表达式处定义一个终止表达式Ei(x,y)

5、；n3. 证明所选取的断言是证明所选取的断言是“良断言良断言”。即满足：。即满足：n1）若对于每一个从程序入口到断点）若对于每一个从程序入口到断点i的通路的通路有：有： (x) R(x,y)= qi(x,r(x,y)n2）若对于每一个由断点）若对于每一个由断点i到断点到断点j的通路的通路有：有： qi(x,y)R(x,y)= qj(x,r(x,y)n这里，这里， R和和r分别表示通过通路分别表示通过通路的条件及通过通路的条件及通过通路后变量后变量y的值。的值。n4. 证明终止表达式是证明终止表达式是“良函数良函数”。即对于每个断点。即对于每个断点i有有 qi(x,y)= Ei(x,y) Wn5

6、. 证明终止条件成立。即对每一条从断点证明终止条件成立。即对每一条从断点i到断点到断点j，并且为某个循环的一部分的通路，并且为某个循环的一部分的通路有：有： qi(x,y) R(x,y)= Ei(x,y) Ej(x, r(x,y) ?(W, )是一个偏序集（满足传递、反对称和反自反性），如果不是一个偏序集（满足传递、反对称和反自反性），如果不存在由存在由W中的元素构成的无限递减序列中的元素构成的无限递减序列 a0 a1 a2 则称则称(W, )为良序集。为良序集。?nqB(x,y): y1 0 y2 0nqC(x,y): y1 0 y2 0nEB(x,y): y1nEC(x,y): y1 + 2y2n1. 通路1(AB)(x) = qB(x,y) qB(x, x1,x2,1)即： y1 + 2y2 y1 + 2y2 2.5 程序正确性证明程序正确性证明Kunth的计数器方法2.5 程序正确性证明程序正确性证明Kunth的计数器方法PROGRAM gcd1; VAR x, y, z, s: INTEGER; BEGIN READ(x,y); i := 0;I(x): x0 0 y0 0 (x0 0 y0 0 ) WHILE x 0 DOL(x,y): x 0 y 0 2x + y + i 2x0 + y0 BEGIN IF y x T