【教学课件】第5章命令式程序的语义.ppt

第5章 命令式程序的语义,函数式程序不含赋值或其它形式的改变变量值的操作命令式程序赋值语句是典型的构造本章围绕一个叫做Kernel的简单的命令式语言来讨论语义,5.1 引 言,Kernel语言的结构由下面的文法概括P:=x:=M|P;P|if B then P else P|while B do P odx和M都有适当的类型valB的类型是bool没有显式的输入、输出，也没有局部变量声明例求对数 x:=1;y:=0;while x z do x:=x+x;y:=y+1 od,5.1 引 言,本章主要内容围绕Kernel来讨论命令式语言的语义 基于一组重写规则的结构化操作语义使用类型化演算和论域（CPO）来表示的指称语义把Kernel程序翻译成类型化演算的表达式利用类型化演算的指称语义基于Floyd-Hoare逻辑的公理语义,5.2 Kernel语言,5.2.1 存储单元Kernel的变量可赋值与函数式语言let子句引入的变量有很大区别可赋值变量指称存储单元变量的左值和右值左值是变量的存储单元的地址右值是该存储单元存放的内容为方便讨论，修改语言显式区分左值和右值，例x和cont x,5.2 Kernel语言,例1 求对数 x:=1;y:=0;while cont x z do x:=cont x+cont x;y:=cont y+1od例2：计算m除以n的商q和余数r q:=0;r:=m;while cont r n doq:=cont q+1;r:=cont r n;od,5.2 Kernel语言,5.2.2 表达式的解释在文法中，M和B分别代表val和bool表达式 P:=x:=M|P;P|if B then P else P|while B do P od不深入表达式的内部细节为方便起见，把val看作nat允许普通的数值和布尔运算,5.2 Kernel语言,用4类别代数A来建立Kernel的抽象机器模型作为介绍操作语义和指称语义的共同基础便于比较操作语义和指称语义本小节先介绍相应代数规范的三个类别基调包含3类别val、bool和loc仅关心loc类别有一个取存储单元内容的函数符号 cont:loc val环境把变量从 loc val bool映射到A的元素loc：程序中的变量；val和bool：程序中的常量Abool的解释是布尔值集合true,false,5.2 Kernel语言,5.2.3 程序状态操作语义和指称语义都涉及“状态”数据结构,5.2 Kernel语言,基调的第4个类别stateinit:stateupdate:state loc val statelookup:state loc val代数公理 lookup(update s l v)l=(lookup)if Eq?l l then v else(lookup s l)update s l(lookup s l)=s(update)1 update(update s l u)l v=if Eq?l l(update)2 then update s l v else update(update s l v)l u,5.2 Kernel语言,四类别代数A Aloc是任意的可数集合，Astate是从Aloc到Aval的所有函数的集合 initA是任意的常函数 lookupA(s,l)=s(l)updateA(s,l,v)是函数s，除了s(l)=v以外，s等同于s为了记号上的方便，下面用init，lookup和update代替initA，lookupA和updateA,5.2 Kernel语言,两个问题为什么不在前三个类别的基础上引入作为状态的函数state=loc val，而要引入第4个类别state若那样，则lookup和update成了高阶的函数符号为什么不用一个函数直接从变量映射到值，而要分离出环境和状态直观上讲，环境和状态在概念上有区别，它们分别对应到实际语言实现的不同机制从技术角度说，Kernel没有提供声明常量的值的方式，只能将程序中常量的取值交给环境来确定,5.3 操作语义,5.3.1 表达式的求值操作语义分成两部分表达式的计算语句的执行表达式的语义表达式、环境、状态和表达式的语义值之间的一个四元关系：M,s eval v环境下标在下面将省略eval由一个证明系统来给出,5.3 操作语义,eval公理x,s eval(x)c,s eval cAeval推理规则 fA(v1,vk)=vlookupA(s,l)=v,5.3 操作语义,5.3.2 命令的执行命令的执行可以用关系exec来刻画updateA(s,(x),v)=s,5.3 操作语义,5.3 操作语义,如果想证明P,s exec s,需要观察P的语法形式,考察哪条规则是完成该证明的最后一条规则例p:=0;m:=0;while(cont m)n dop:=cont m;m:=(cont m)+1;od,5.3 操作语义,p:=0;s1=updateA s lp 0 m:=0;while(cont m)n dop:=cont m;m:=(cont m)+1;od,5.3 操作语义,p:=0;s1=updateA s lp 0 m:=0;s2=updateA s1 lm 0 while(cont m)n dop:=cont m;m:=(cont m)+1;od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n dop:=cont m;m:=(cont m)+1;od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n do(cont m)n,s2 eval true p:=cont m;m:=(cont m)+1;od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n dop:=cont m;m:=(cont m)+1;(p:=cont m;m:=(cont m)+1),s2 exec s3od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n dop:=cont m;m:=(cont m)+1;lookupA s3 lp=0&lookupA s3 lm=1od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n do(cont m)n,s3 eval true p:=cont m;m:=(cont m)+1;lookupA s3 lp=0&lookupA s3 lm=1od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n dop:=cont m;m:=(cont m)+1;lookupA s3 lp=0 m:=(cont m)+1),s3 exec s4 od,5.3 操作语义,p:=0;m:=0;lookupA s2 lm=lookupA s2 lp=0while(cont m)n dop:=cont m;m:=(cont m)+1;lookupA s4 lp=1 m:=(cont m)+1),s3 exec s4 od,5.4 指称语义,带状态的类型化演算前两章已经给出了类型化演算的指称语义只要给出从Kernel语言到类型化演算的翻译即可把Kernel程序翻译成类型化演算state,fix,该演算有类型常量val,bool,loc,state和statestate,fix,演算还增加的运算Eq?:loc loc bool在state上的运算init,update和lookup,5.4 指称语义,每个类型都有条件运算ifthenelse还有提升运算（在下面描述），抽象，应用和不动点算子 fixstate:(state state)(state state)(state state)state,fix,的CPO模型A是四类别代数A的一个拓展val,bool,loc和state的解释同A的解释一样state被解释成提升集合Astate=(Astate)这种解释延伸到函数类型,Astate state 有最小元，该类型有最小不动点算子,5.4 指称语义,提升运算:state state如果M:state,让M和M有同样的指称但不同的类型中缀算符(state Elim)M=:state M N=MN:state 函数合成的严格形式美化成M N s:state.M(N s),5.4 指称语义,5.4.2 语义函数指称语义由两部分组成表达式和命令到state,fix,项的语法翻译这个演算在模型A中的标准解释语法翻译部分函数V:把布尔表达式和值表达式分别翻译成类型为state bool和state val的项函数C:把命令翻译成类型为state state的项,5.4 指称语义,语义函数把这些语法翻译和从state,fix,的项到模型A的标准含义函数组合起来:expressions environments Astate Avalues:commands environments Astate Astate,5.4 指称语义,表达式的语法翻译 Vx=s:state.x Vcont x=s:state.lookup s x V f M1 Mk=s:state.f VM1s VMks表达式M在环境中的含义 M=AVM M s=(M)s,5.4 指称语义,命令的语法翻译 Cx:=M=s:state.update s x(VMs)CP1;P2=CP2 CP1 Cif B then P1 else P2=s:state.if VBs then CP1s else CP2s Cwhile B do P od=fix(f:state state.s:state.if VBs then(f CP)s else s)程序P在环境下的含义 P=ACP P s=(P)s,5.4 指称语义,例 一个简单的程序skip x:=cont xCskip=s:state.update s x(Vcont xs)=s:state.update s x(lookup s x)=s:state.s skip s=(ACskip)(s)=(As:state.s)(s)=s,5.4 指称语义,指称语义可用来证明简单程序之间的等价证明while B do P od=if B then(P;while B do P od)else skipCwhile B do P od=fix(f:state state.s:state.if VBs then(f CP)s else s)=s:state.if VBs then(Cwhile B do P od CP)s else s=Cif B then(P;while B do P od)else skip,5.4 指称语义,6.4.3 操作语义和指称语义的等价引理5.1 令是环境并且sAstate不是底元。对任何类型为loc、val或bool的表达式M，以及Aloc、Aval或Abool中的a，有M,s eval a 当且仅当 M s=a对M的结构进行归纳来证明该引理x,s eval(x)=x s cont x,s eval lookupA s(x)=cont x sf M1 Mk,s eval fA(a1,ak)=f M1 Mk s,5.4 指称语义,引理5.2 令F是函数F f:state state.s:state.if Bs then f(Ps)else s 这是把while循环翻译到state,fix,所得的形式，其中B:statebool并且P:statestate令s:state是区别于state的状态。对任何自然数n，若(Fn s)=s，则存在某个m n，使得s=Pm s，Bs=false，且对所有的km，有Pk s=sk且Bsk=true注：对P:statestate，用Pk s表示把P的k次严格合成作用到s，也就是Pk s P(P(Ps),5.4 指称语义,定理5.3 令是一个环境，并且s,s Astate是任意的“非底元”状态。对任何程序P有P,s exec s当且仅当 P s=s,5.5 Kernel程序的前后断言,5.5.1 一阶逻辑和部分正确性证明证明Kernel程序的性质用类型化项上的一般证明系统使用更适合于Kernel程序语法的逻辑后一种方式的优点不需要学习类型化演算和最小不动点概念程序正确与否的大部分直观理由都关联到程序的结构如果证明系统以一种自然的方式反映程序设计语言的结构，它可能对程序设计风格产生直接的影响,5.5 Kernel程序的前后断言,Kernel程序的部分正确性断言的形式F P GF和G是一阶公式，用三类别（val,bool和loc）语言来写，但不可以含抽象或状态变量P是一段程序例(x y cont x=3)y:=1(cont y=1 cont x=3),5.5 Kernel程序的前后断言,一阶公式的语言上一阶项的定义（项的类别是loc,val或bool）M:=x|f M M|cont y|Eq?y z|if B then M else M一阶逻辑公式的定义F:=M=N|F F|F|locx.F|valx.F|boolx.F一些缩写 M N(M=N)F1 F2(F1 F2)F1 F2 F1 F2bx.F(bx.F)对于b bool,val,loc,5.5 Kernel程序的前后断言,对模型A来说，一阶公式的可满足性可以归纳定义如下：,s M=N当且仅当 M s=N s,s F1 F2当且仅当,s F1 并且,s F2,s F当且仅当不是,s F,s bx.F当且仅当对所有的a Ab，xa,s F,5.5 Kernel程序的前后断言,部分正确性(1)在环境和状态s state下，如果下面的蕴涵 若,s F且 P s=s，则,s G成立，就说部分正确性断言F P G 在环境和状态sstate下可满足(2)如果 P s=state，则认为F P G在s上也得到满足(3)如果在任何环境和状态s state下，部分正确性断言F P G都可满足，则说F P G是可满足的(4)F P G可满足不代表程序执行一定终止,5.5 Kernel程序的前后断言,5.5.2 证明规则逻辑推论规则(conseq)顺序推理规则(seq)条件推理规则(cond),5.5 Kernel程序的前后断言,赋值公理(asg)Mcont xF x:=M F在赋值x:=M后对cont x为真的东西，在赋值前必定已对M为真例 y z x:=y cont x z cont w z x:=cont w cont x z ycont v x:=y cont xcont v/假定没有别名赋值公理为什么不是正向的F x:=y(cont x)/yF,5.5 Kernel程序的前后断言,while规则(while)F叫做循环不变式,5.5 Kernel程序的前后断言,例 考虑下面计算x-y的简单程序，假定y xd:=0;P0while(cont d)+y x doBd:=(cont d)+1;P1od证明 y x P0;while B do P1 od(cont d)+y=x,5.5 Kernel程序的前后断言,d:=0;while(cont d)+y x doBd:=(cont d)+1;od(a)y x d:=0(cont d)+y x(b)(cont d)+y x)Bd:=(cont d)+1(cont d)+y x(cont d)+y x)B(cont d)+y x(cont d)+y x d:=(cont d)+1(cont d)+y x(cont d)+y x是循环不变式(c)(cont d)+y x)B(cont d)+y=x,5.5 Kernel程序的前后断言,5.5.3 可靠性使用程序的指称语义来证明可靠性断言语言的证明系统对指称模型可靠断言语言上的证明系统用的就是经典逻辑的公理和推理规则，它们的可靠性证明比较简单Hoare逻辑的公理和推理规则对指称模型可靠,5.5 Kernel程序的前后断言,5.5.3 可靠性使用程序的指称语义来证明可靠性定理5.4假定部分正确性规范FPG可证，那么FP G在模型A中有效只要证明该公理语义中的公理和推理规则对模型A中都可靠就可以了,习 题,第一次：5.2，5.6,5.15(a),(b),(c),