公理语义-Floyd

1、程序设计形式语义学程序设计形式语义学南京理工大学南京理工大学 计算机系计算机系张琨张琨二二四年八月二日四年八月二日南京理工大学南京理工大学 计算机系计算机系2006.11.212006.11.21主讲：张琨主讲：张琨2 公理语义公理语义n试图通过在程序逻辑的范围内给出证明规试图通过在程序逻辑的范围内给出证明规则来确定程序设计构造的含义。该方法的则来确定程序设计构造的含义。该方法的代表人物是代表人物是R.W.Floyd和和C.A.R.Hoare。n从一开始，公理语义强调的是正确性证明。从一开始，公理语义强调的是正确性证明。程序的正确性证明程序的正确性证明n2.1 引言引言n2.2 FCL/2结构

2、的表示结构的表示n2.3 其他控制结构的表示其他控制结构的表示n2.4 程序的形式描述与证明程序的形式描述与证明n2.5 程序正确性证明程序正确性证明n2.6 计算计算WP：语言的语义：语言的语义2.1 引言引言nSMALL语言的控制结构能够表示其他语言，首先引入最小语言（语言的控制结构能够表示其他语言，首先引入最小语言（SMALL）。）。n定义：最小语言定义：最小语言SMALL定义如下：定义如下：1.赋值语句右部表达式至多只有一个操作符，没有括号出现；赋值语句右部表达式至多只有一个操作符，没有括号出现；2.控制语句有：控制语句有：GOTO ； IF THEN GOTO ； 其中，其中，是单个

3、布尔变量或两个算术变量的单一关系。是单个布尔变量或两个算术变量的单一关系。是是或或 3.语句可以带标号，标号语句可以带标号，标号L可以看作是标号为可以看作是标号为L的语句在程序中的位置的名字（在实际的语句在程序中的位置的名字（在实际的计算机中，的计算机中，#L是存储该语句的存储单元）。语句是存储该语句的存储单元）。语句 x := #L;把标号为把标号为L的语句的存储单元名存储在变量的语句的存储单元名存储在变量x中。语句中。语句 GOTO x;x;把控制把控制转转移到其移到其单单元名存元名存储储在在变变量量x x中的那中的那个语个语句。句。2.2 FCL/2结构的表示结构的表示2.2 FCL/2

4、结构的表示结构的表示2.2 FCL/2结构的表示结构的表示n3.IF-THEN-ELSE3.IF-THEN-ELSE的表示的表示定定义该语义该语句的表示句的表示为为：REP(IF B THEN SREP(IF B THEN S1 1 ELSE S ELSE S2 2) )= REP(t= REP(t := B);IF t THEN GOTO L:= B);IF t THEN GOTO L1 1;REP(S;REP(S2 2);GOTO L);GOTO L2 2; ;L L1 1:REP(S:REP(S1 1););L L2 2: :2.2 FCL/2结构的表示结构的表示n4.WHILE4.WH

5、ILE语语句的表示句的表示定定义该语义该语句的表示句的表示为为：REP(WHILE B DO S) =REP(WHILE B DO S) =L L1 1:REP(e := NOT B);:REP(e := NOT B);IF e THEN GOTO LIF e THEN GOTO L2 2; ;REP(S);REP(S);GOTO LGOTO L1 1; ;L L2 2: :2.2 FCL/2结构的表示结构的表示n举举例例IF xy THEN w := 5 ELSE w := -3;IF xy THEN w := 5 ELSE w := -3;定定义该语义该语句的表示句的表示 REP(IF x

6、y THEN w := 5 ELSE w := -3)=REP(IF xy THEN w := 5 ELSE w := -3)= t := xy; t := xy; IF t THEN GOTO L IF t THEN GOTO L1 1; ; w := -3; GOTO L w := -3; GOTO L2 2; ; L L1 1: w := 5;: w := 5; L L2 2: :2.2 FCL/2结构的表示结构的表示n讨论讨论i := 0; s := 0;i := 0; s := 0;WHILE i100 DO s := s + i;WHILE i100 DO s := s + i;定

7、定义该语义该语句的表示句的表示i := 0; s := 0;i := 0; s := 0;WHILE i100 DO s := s + i;WHILE i100 DO s := s + i;2.3 其他控制结构的表示其他控制结构的表示2.3 其他控制结构的表示其他控制结构的表示n6.NumberedCase6.NumberedCase语语句的表示句的表示NumberedCaseNumberedCase E OF S E OF S1 1; S; S2 2;S;Sk k; ; 定定义该语义该语句的表示句的表示为为：REP(NumberedCaseREP(NumberedCase E OF S E

8、OF S1 1; S; S2 2;S;Sk k;OTHERWISE S;OTHERWISE Sw w END) = END) =2.3 其他控制结构的表示其他控制结构的表示n6.NumberedCase6.NumberedCase语语句的表示句的表示NumberedCaseNumberedCase E OF S E OF S1 1; S; S2 2;S;Sk k; ; 定定义该语义该语句的表示句的表示为为：REP(NumberedCaseREP(NumberedCase E OF S E OF S1 1; S; S2 2;S;Sk k;OTHERWISE S;OTHERWISE Sw w EN

9、D) = END) = REP(t REP(t := E); := E); IF t1 THEN GOTO L IF tn THEN GOTO L IF tn THEN GOTO Lw w; ; GOTO TRVt GOTO TRVt;L L1 1:REP(S:REP(S1 1););GOTO LexitGOTO Lexit; ;L L2 2:REP(S:REP(S2 2););GOTO LexitGOTO Lexit; ; L Lk k:REP(S:REP(Sk k););GOTO LexitGOTO Lexit; ; L Lw w:REP(S:REP(Sw w);); Lexit Lexi

10、t; ;2.4 程序的形式描述与证明程序的形式描述与证明n本节阐述程序的功能描述，证明程序是本节阐述程序的功能描述，证明程序是否能够完成其功能（即程序正确性证否能够完成其功能（即程序正确性证明），并讨论如何测试其正确性。明），并讨论如何测试其正确性。n功能描述功能描述n程序证明程序证明n测试测试n程序设计语言的描述程序设计语言的描述2.4 程序的形式描述与证明程序的形式描述与证明n1. 功能描述功能描述 程序功能描述，就是描述程序做什么。程序功能描述，就是描述程序做什么。一般采用自然语言描述，如一般采用自然语言描述，如ARRAY A描述描述A是一个数组，这是一种自然语言是一个数组，这是一种自然

11、语言的表述方式。很多情况下，如程序的正的表述方式。很多情况下，如程序的正确性证明采用数学形式更有效、更方便。确性证明采用数学形式更有效、更方便。 2.4 程序的形式描述与证明程序的形式描述与证明n2. 程序证明程序证明 每一个程序都有一个预定的功能，那么，每一个程序都有一个预定的功能，那么，一个实际的程序是否实现了这个预定的功能呢？一个实际的程序是否实现了这个预定的功能呢？为了回答这个问题，一般采用两种方法，即测为了回答这个问题，一般采用两种方法，即测试和证明。一般而言，对于一个程序的完全测试和证明。一般而言，对于一个程序的完全测试是不可能的，测试数据可能无限大。一个已试是不可能的，测试数据可

12、能无限大。一个已经作过测试的程序，也可能还包含错误。所以，经作过测试的程序，也可能还包含错误。所以，必须找到其他的方法，来提高程序正确性的信必须找到其他的方法，来提高程序正确性的信任度。这个方法就是通过证明，证明程序与其任度。这个方法就是通过证明，证明程序与其功能是一致的。程序证明技术还有助于读、写功能是一致的。程序证明技术还有助于读、写程序，以及程序的形式化推理程序，以及程序的形式化推理。2.4 程序的形式描述与证明程序的形式描述与证明n3. 测试测试 很多情况下，程序的完全证明是困难很多情况下，程序的完全证明是困难的也是不必要的，同时，程序不能完全的也是不必要的，同时，程序不能完全测试时往

13、往也不能完全证明。较为有效测试时往往也不能完全证明。较为有效的方法是把证明和测试结合起来，如设的方法是把证明和测试结合起来，如设计一个精心测试的方法，而这种方法的计一个精心测试的方法，而这种方法的制定是在程序证明的推理风格上进行的。制定是在程序证明的推理风格上进行的。以此增强程序正确性的可信度。以此增强程序正确性的可信度。2.4 程序的形式描述与证明程序的形式描述与证明n4. 程序设计语言的描述程序设计语言的描述 是对程序出现的每个语句在功能上做是对程序出现的每个语句在功能上做什么的描述，即必须对程序设计语言的什么的描述，即必须对程序设计语言的结构语义或意义作精确的描述。结构语义或意义作精确的

14、描述。2.4 程序的形式描述与证明程程序的形式描述与证明程序的功能描述序的功能描述n程序的功能描述：指程序终止时，各个变量的程序的功能描述：指程序终止时，各个变量的值与程序执行前这些变量的值之间的值与程序执行前这些变量的值之间的关系关系。n这个关系可以用一个谓词（或称为这个关系可以用一个谓词（或称为后置条件后置条件）来表示：来表示：程序终止之后应该满足的条件。程序终止之后应该满足的条件。n如一个程序只有一个语句如一个程序只有一个语句y:=x/k，则它的一，则它的一个后置条件，可以表示为个后置条件，可以表示为x=y*k，这个后置，这个后置条件指出，条件指出，y是是x除以除以k的商。的商。n但以这

15、个后置条件还不能描述其功能正确性。但以这个后置条件还不能描述其功能正确性。还应包含一个假设，还应包含一个假设，k不能取不能取0值，意味着执值，意味着执行前条件行前条件k0就应该成立。所以这个条件称为就应该成立。所以这个条件称为前置条件前置条件。2.4 程序的形式描述与证明程程序的形式描述与证明程序的功能描述序的功能描述n把前置条件和后置条件结合起来，就可以形成把前置条件和后置条件结合起来，就可以形成关于程序功能得完整的描述。形式化定义程序关于程序功能得完整的描述。形式化定义程序的功能描述如下：的功能描述如下：n记号记号PSQn是一个逻辑语句，其值为真或假，为真时的含是一个逻辑语句，其值为真或假

16、，为真时的含义是：若义是：若S开始执行前开始执行前P为真，为真，S的执行将的执行将终止终止，且且Q为真。为真。nS是一程序或一程序片段，是一程序或一程序片段，P和和Q是谓词。是谓词。n这个记号读作这个记号读作“S关于前置条件关于前置条件P和后置条件和后置条件Q是强正确的是强正确的” （或称完全正确的），强正确（或称完全正确的），强正确通常简称为正确通常简称为正确 。2.4 程序的形式描述与证明程序的形式描述与证明程序的功能描述程序的功能描述2.5 程序正确性证明程序正确性证明2.5 程序正确性证明程序正确性证明n定义定义2.1 （部分正确性）若对每个使得（部分正确性）若对每个使得I(i)为真，

17、为真，并且程序计算终止的输入信息并且程序计算终止的输入信息i，O(i,P(i)为真，称为真，称程序程序P关于关于I和和O是部分正确的是部分正确的，即，即I(i) P- O(i,P(i)n定义定义2.2 （程序终止性）若对每个使得（程序终止性）若对每个使得I(i)为真的为真的输入信息输入信息i，程序计算都终止，称，程序计算都终止，称程序程序P对对I是终止的是终止的，即：即：I(i) - Pn定义定义2.3 （完全正确性）若对每个使得（完全正确性）若对每个使得I(i)为真的为真的输入输入i，程序计算都终止，并且，程序计算都终止，并且O(i,P(i)为真，称为真，称程程序序P关于关于I和和O是完全正

18、确的是完全正确的，即：，即：I(i) - P O(i,P(i)P(i)表示与输入信息表示与输入信息i相对应的程序相对应的程序P的输入信息，的输入信息，P表示程序终止。表示程序终止。2.5 程序正确性证明程序正确性证明n程序的完全正确等价于该程序是部分正确的且又是终止的。程序的完全正确等价于该程序是部分正确的且又是终止的。n程序的正确性证明通常分为证明部分正确性和终止性两步进行。程序的正确性证明通常分为证明部分正确性和终止性两步进行。n1. 证明部分正确性的方法证明部分正确性的方法nA. Floyd的不变式断言法的不变式断言法nB. Manna的子目标断言法的子目标断言法nC. Hoare的公理

19、化方法的公理化方法n2. 证明终止性的方法证明终止性的方法nA. Floyd的良序集方法的良序集方法nB. Kunth的计数器方法的计数器方法nC. Manna等人的不动点方法等人的不动点方法n3. 证明完全正确性的方法证明完全正确性的方法nA. Manna等人对等人对Hoare公理化方法的推广公理化方法的推广nB. Burstall的间发断言法的间发断言法nC. Dijkstra的弱谓词变换方法及强验证方法的弱谓词变换方法及强验证方法2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n例，设例，设x，y是正整数，求是正整数，求x，y的最大公约数的最大公约数z，即，即z

20、=gcd(x,y)PROGRAM gcd; VAR x, y, z, s: INTEGER; BEGIN READ(x,y); WHILE x 0 do IF y = x THEN y := y-x ELSE BEGIN s := x; x := y; y := s; END z := y; WRITE(z)END;2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n例，设例，设x，y是正整数，求是正整数，求x，y的最大公约数的最大公约数z，即，即z=gcd(x,y)设设x，y的初始值为的初始值为x0，y0，可分，可分别建立输入断言别建立输入断言I、输出断言、输出断言O

21、如如下：下：I(x): x0 0 y0 0 (x0 0 y0 0 )O(x,z): z = gcd(x0,y0)2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n1. 建立输入、输出断言和循环不变式建立输入、输出断言和循环不变式设设x，y的初始值为的初始值为x0，y0，可分别建立输入断言，可分别建立输入断言I、输出断言、输出断言O、不变式、不变式L如如下：下：I(x): x0 0 y0 0 (x0 0 y0 0 )O(x,z): z = gcd(x0,y0)L(x,y): x 0 y 0 (x 0 y 0 ) gcd(x,y) = gcd(x0,y0)2.5 程序正确

22、性证明程序正确性证明Floyd的不变式断言法的不变式断言法n2. 在每条路径上建立验证条件在每条路径上建立验证条件n设设I(x)成立，当第一次到达成立，当第一次到达L处时，处时，L(x,y)成立，此时成立，此时x= x0,y= y0。得。得C1处处的验证条件的验证条件1： I(x) = L(x,y)C1(x,y) : x0 0 y0 0 (x0 0 y0 0 ) = x0 0 y0 0 (x0 0 y0 0 ) gcd(x0,y0) = gcd(x0,y0)2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n2. 在每条路径上建立验证条件在每条路径上建立验证条件n当当y

23、 x时，回到时，回到L，可得图中，可得图中C2处的验证条件处的验证条件2： L(x,y) x 0 y x = L(x,y)C2(x,y) : x 0 y 0 (x 0 y 0 ) gcd(x,y) = gcd(x0,y0) x 0 y x = x 0 y-x 0 (x 0 y-x 0 ) gcd(x,y-x) = gcd(x0,y0)2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n2. 在每条路径上建立验证条件在每条路径上建立验证条件n当当yx时，回到时，回到L，可得图中，可得图中C3处的验证条件处的验证条件3： L(x,y) x 0 y L(x,y)C3(x,y) : x 0 y 0 (x 0 y 0 ) gcd(x,y) = gcd(x0,y0) x 0 y y 0 x 0 (y 0 x 0 ) gcd(y,x) = gcd(x0,y0)2.5 程序正确性证明程序正确性证明Floyd的不变式断言法的不变式断言法n2. 在每条路径上建立验证条件在每条路径上建立验证条件n当当x=0时，退出循环，此时时，退出循环，此时z=y,可得图中可得图中C4处的验证条件处的验证条件4： L(x,y) x 0 = O(x,z