程序设计形式语义学公理语义Floyd课件

程序设计形式语义学二○○四年八月二日2011.9程序设计形式语义学1精选课件ppt2公理语义试图通过在程序逻辑的范围内给出证明规则来确定程序设计构造的含义。该方法的代表人物是R.W.Floyd和C.A.R.Hoare。从一开始，公理语义强调的是正确性证明。2精选课件ppt程序的正确性证明2.1引言2.2FCL/2结构的表示2.3其他控制结构的表示2.4程序的形式描述与证明2.5程序正确性证明2.6计算WP：语言的语义3精选课件ppt2.1引言SMALL语言的控制结构能够表示其他语言，首先引入最小语言（SMALL）。定义：最小语言SMALL定义如下：1.赋值语句右部表达式至多只有一个操作符，没有括号出现；2.控制语句有： GOTO<位置>；IF<简单布尔表达式>THENGOTO<位置>；其中，<简单布尔表达式>是单个布尔变量或两个算术变量的单一关系。<位置>是<标号>或@<变量>3.语句可以带标号，标号L可以看作是标号为L的语句在程序中的位置的名字（在实际的计算机中，#L是存储该语句的存储单元）。语句 x:=#L; 把标号为L的语句的存储单元名存储在变量x中。语句 GOTO@x; 把控制转移到其单元名存储在变量x中的那个语句。4精选课件ppt2.2FCL/2结构的表示1.赋值语句的表示 x:=E1/E2定义该赋值语句的表示为： REP(x:=E1/E2) =REP(t1:=E1);REP(t2:=E2);x:=t1/t2定义记号REP(S)代表语句、短语或值S的表示。5精选课件ppt2.2FCL/2结构的表示2.顺序控制的表示 顺序语句序列 S1;S2;…;Sk定义该顺序语句的表示为： REP(S1;S2;…;Sk) =REP(S1);REP(S2);…;REP(Sk)定义记号REP(S)代表语句、短语或值S的表示。6精选课件ppt2.2FCL/2结构的表示3.IF-THEN-ELSE的表示 定义该语句的表示为： REP(IFBTHENS1ELSES2) =REP(t

:=B);IFtTHENGOTOL1;REP(S2);GOTOL2; L1:REP(S1); L2:定义记号REP(S)代表语句、短语或值S的表示。7精选课件ppt2.2FCL/2结构的表示4.WHILE语句的表示 定义该语句的表示为： REP(WHILEBDOS)= L1:REP(e:=NOTB); IFeTHENGOTOL2; REP(S); GOTOL1; L2:定义记号REP(S)代表语句、短语或值S的表示。8精选课件ppt2.2FCL/2结构的表示举例 IFx>yTHENw:=5ELSEw:=-3;

定义该语句的表示REP(IFx>yTHENw:=5ELSEw:=-3)=t:=x>y;IFtTHENGOTOL1;w:=-3;GOTOL2;L1:w:=5;L2:定义记号REP(S)代表语句、短语或值S的表示。9精选课件ppt2.2FCL/2结构的表示讨论 i:=0;s:=0; WHILEi<100DOs:=s+i; 定义该语句的表示定义记号REP(S)代表语句、短语或值S的表示。10精选课件ppt i:=0;s:=0; WHILEi<100DOs:=s+i;11精选课件ppt2.3其他控制结构的表示5.REPEAT语句的表示 REPEATSUNTILB等价于S;WHILE～BDOS 定义该语句的表示为： REP(REPEATSUNTILB)= REP(S;WHILE～BDOS)= L1:REP(S); REP(t:=NOTB); IFtTHENGOTOL;定义记号REP(S)代表语句、短语或值S的表示。12精选课件ppt2.3其他控制结构的表示6.NumberedCase语句的表示 NumberedCaseEOFS1;S2;…;Sk; 定义该语句的表示为： REP(NumberedCaseEOFS1;S2;…;Sk;OTHERWISESwEND)=定义记号REP(S)代表语句、短语或值S的表示。13精选课件ppt2.3其他控制结构的表示6.NumberedCase语句的表示 NumberedCaseEOFS1;S2;…;Sk; 定义该语句的表示为： REP(NumberedCaseEOFS1;S2;…;Sk;OTHERWISESwEND)= REP(t:=E); IFt<1THENGOTOLw; IFt>nTHENGOTOLw;GOTO@TRV[t]; L1:REP(S1); GOTOLexit; L2:REP(S2); GOTOLexit;… Lk:REP(Sk); GOTOLexit;Lw:REP(Sw);Lexit;定义记号REP(S)代表语句、短语或值S的表示。14精选课件ppt2.4程序的形式描述与证明本节阐述程序的功能描述，证明程序是否能够完成其功能（即程序正确性证明），并讨论如何测试其正确性。功能描述程序证明测试程序设计语言的描述15精选课件ppt2.4程序的形式描述与证明1.功能描述程序功能描述，就是描述程序做什么。一般采用自然语言描述，如ARRAYA描述A是一个数组，这是一种自然语言的表述方式。很多情况下，如程序的正确性证明采用数学形式更有效、更方便。

16精选课件ppt2.4程序的形式描述与证明2.程序证明每一个程序都有一个预定的功能，那么，一个实际的程序是否实现了这个预定的功能呢？为了回答这个问题，一般采用两种方法，即测试和证明。一般而言，对于一个程序的完全测试是不可能的，测试数据可能无限大。一个已经作过测试的程序，也可能还包含错误。所以，必须找到其他的方法，来提高程序正确性的信任度。这个方法就是通过证明，证明程序与其功能是一致的。程序证明技术还有助于读、写程序，以及程序的形式化推理。17精选课件ppt2.4程序的形式描述与证明3.测试很多情况下，程序的完全证明是困难的也是不必要的，同时，程序不能完全测试时往往也不能完全证明。较为有效的方法是把证明和测试结合起来，如设计一个精心测试的方法，而这种方法的制定是在程序证明的推理风格上进行的。以此增强程序正确性的可信度。18精选课件ppt2.4程序的形式描述与证明4.程序设计语言的描述是对程序出现的每个语句在功能上做什么的描述，即必须对程序设计语言的结构语义或意义作精确的描述。19精选课件ppt2.4程序的形式描述与证明－程序的功能描述程序的功能描述：指程序终止时，各个变量的值与程序执行前这些变量的值之间的关系。这个关系可以用一个谓词（或称为后置条件）来表示：程序终止之后应该满足的条件。如一个程序只有一个语句y:=x/k，则它的一个后置条件，可以表示为x=y*k，这个后置条件指出，y是x除以k的商。但以这个后置条件还不能描述其功能正确性。还应包含一个假设，k不能取0值，意味着执行前条件k≠0就应该成立。所以这个条件称为前置条件。20精选课件ppt2.4程序的形式描述与证明－程序的功能描述把前置条件和后置条件结合起来，就可以形成关于程序功能得完整的描述。形式化定义程序的功能描述如下：记号 P{S}Q是一个逻辑语句，其值为真或假，为真时的含义是：若S开始执行前P为真，S的执行将终止，且Q为真。S是一程序或一程序片段，P和Q是谓词。这个记号读作“S关于前置条件P和后置条件Q是强正确的”（或称完全正确的），强正确通常简称为正确。21精选课件ppt2.4程序的形式描述与证明－程序的功能描述y:=x/k→k≠0{y:=x/k}x=y*kx=y→k=1{y:=x/k}x=yx:=x+1→x=x’→{x:=x+1}x=x’+1用一撇表示变量原来的值，仅当执行后值发生了改变的那些变量在前置条件中也出现时才有必要，否则，就无必要。机器字长的限制(x+1)≤2w–1→{x:=x+1}x=x’+122精选课件ppt2.5程序正确性证明一段程序是正确的：对满足一定条件的输入、输出而言，通常把满足这个程序段的输入条件和输出条件分别称为该程序段的输入断言和输出断言（均为逻辑表达式），常用I(x)、O(x,y)表示，其中x，y分别表示输入信息和输出信息（x和y既可以表示单个变量，也可以表示一组变量）。23精选课件ppt2.5程序正确性证明定义2.1（部分正确性）若对每个使得I(i)为真，并且程序计算终止的输入信息i，O(i,P(i))为真，称程序P关于I和O是部分正确的，即

I(i)∧P↓->O(i,P(i))定义2.2（程序终止性）若对每个使得I(i)为真的输入信息i，程序计算都终止，称程序P对I是终止的，即：

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

I(i)

->P↓∧O(i,P(i))P(i)表示与输入信息i相对应的程序P的输入信息，P↓表示程序终止。24精选课件ppt2.5程序正确性证明程序的完全正确等价于该程序是部分正确的且又是终止的。程序的正确性证明通常分为证明部分正确性和终止性两步进行。1.证明部分正确性的方法A.Floyd的不变式断言法B.Manna的子目标断言法C.Hoare的公理化方法2.证明终止性的方法A.Floyd的良序集方法B.Kunth的计数器方法C.Manna等人的不动点方法3.证明完全正确性的方法A.Manna等人对Hoare公理化方法的推广B.Burstall的间发断言法C.Dijkstra的弱谓词变换方法及强验证方法25精选课件ppt2.5程序正确性证明－Floyd的不变式断言法例，设x，y是正整数，求x，y的最大公约数z，即z=gcd(x,y)PROGRAMgcd;VARx,y,z,s:INTEGER;BEGINREAD(x,y);WHILEx<>0doIFy>=xTHENy:=y-xELSEBEGINs:=x;x:=y;y:=s;ENDz:=y;WRITE(z)END;26精选课件ppt2.5程序正确性证明－Floyd的不变式断言法例，设x，y是正整数，求x，y的最大公约数z，即z=gcd(x,y)分析设x，y的初始值为x0，y0，可分别建立输入断言I、输出断言O如下：I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0)O(x,z):z=gcd(x0,y0)27精选课件ppt2.5程序正确性证明－Floyd的不变式断言法1.建立输入、输出断言和循环不变式 设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)28精选课件ppt2.5程序正确性证明－Floyd的不变式断言法2.在每条路径上建立验证条件设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)]29精选课件ppt2.5程序正确性证明－Floyd的不变式断言法2.在每条路径上建立验证条件当y≥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)]30精选课件ppt2.5程序正确性证明－Floyd的不变式断言法2.在每条路径上建立验证条件当y<x时，回到L，可得图中C3处的验证条件3：L(x,y)∧x≠0∧y<x=>L(x,y)C3(x,y):[x≥0∧y≥0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y<x] =>[y≥0∧x≥0∧(y≠0∨x≠0) ∧gcd(y,x)=gcd(x0,y0)]31精选课件ppt2.5程序正确性证明－Floyd的不变式断言法2.在每条路径上建立验证条件当x=0时，退出循环，此时z=y,可得图中C4处的验证条件4：

L(x,y)∧x＝0=>O(x,z)C4(x,y):[x≥0∧y≥0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x＝0] =>z=gcd(x0,y0)]32精选课件ppt2.5程序正确性证明－Floyd的不变式断言法3.证明验证条件（仅证明C2(x,y)和C4(x,y)）C2(x,y)的证明： C2(x,y):[x≥0∧y≥0∧(x≠0∨y≠0)∧gcd