第第5章章 命令式程序的语义命令式程序的语义函数式程序函数式程序不含赋值或其它形式的改变变量值的操作不含赋值或其它形式的改变变量值的操作命令式程序命令式程序赋值语句是典型的构造赋值语句是典型的构造本章围绕一个叫做本章围绕一个叫做Kernel的简单的命令式语的简单的命令式语言来讨论语义言来讨论语义醚佰狮聊盆汪烽硷帝壶遇否垄藉斑溪嘉茧斑加饲五挟棕脑筷悟藏疆掇外津第5部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义第5部分命令式程序的语义5.1 引引 言言本章主要内容本章主要内容围绕围绕Kernel来讨论命令式语言的语义来讨论命令式语言的语义 基于一组重写规则的基于一组重写规则的结构化结构化操作语义操作语义使用类型化使用类型化 演算和论域（演算和论域（CPO）来表示的指）来表示的指称语义称语义把把Kernel程序翻译成类型化程序翻译成类型化 演算的表达式演算的表达式利用利用类型化类型化 演算的指称语义演算的指称语义基于基于Floyd-Hoare逻辑的公理语义逻辑的公理语义展粮梭玩品吐沤羊徽限拌牟活铀鼻蚤猪陈挡傅呆露蹈俐黄卵方刹透竹坠摊第5部分命令式程序的语义第5部分命令式程序的语义5.2 Kernel语言语言5.2.1 存储单元存储单元Kernel的变量可赋值的变量可赋值与函数式语言与函数式语言let子句引入的变量有很大区别子句引入的变量有很大区别可赋值变量指称存储单元可赋值变量指称存储单元变量的左值和右值变量的左值和右值左值是变量的存储单元的地址左值是变量的存储单元的地址右值是该存储单元存放的内容右值是该存储单元存放的内容为方便讨论，修改语言为方便讨论，修改语言显式区分左值和右值，例显式区分左值和右值，例x和和cont x近夸肝酞街怒换宝吏钝张沁孵若孤革肪影裔戊嗣囤涡犹孵莲川跟惧趴语隐第5部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义第5部分命令式程序的语义5.2 Kernel语言语言用用4类别代数类别代数A A来建立来建立Kernel的抽象机器模型的抽象机器模型作为介绍操作语义和指称语义的共同基础作为介绍操作语义和指称语义的共同基础便于比较操作语义和指称语义便于比较操作语义和指称语义本小节先介绍相应代数规范的三个类别本小节先介绍相应代数规范的三个类别基调基调 包含包含3类别类别val、bool和和loc仅关心仅关心loc类别有一个取存储单元内容的函数符号类别有一个取存储单元内容的函数符号 cont : loc val环境环境 把变量从把变量从 loc val bool映射到映射到A A的元素的元素 loc：程序中的变量；：程序中的变量； val和和 bool ：程序中的常量：程序中的常量Abool的解释是布尔值集合的解释是布尔值集合true, false洱措戍昭突砌涅撤迎艳驹屿惜墒望浇兜撒屠践伶胀蛙退扳兄乔迟辰柏夹坞第5部分命令式程序的语义第5部分命令式程序的语义5.2 Kernel语言语言5.2.3 程序状态程序状态操作语义和指称语义都涉及操作语义和指称语义都涉及“状态状态”数据结构数据结构名字名字存储单元存储单元状态状态值值环境环境从名字到值的两步映射从名字到值的两步映射趾渭讲恼恤港热帛奖隶惰替怠惺煎渗之奶沂搭犯毋诽综跪寒蹭沙脾独晶龚第5部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义第5部分命令式程序的语义5.2 Kernel语言语言四类别代数四类别代数A A Aloc是是任任意意的的可可数数集集合合，Astate是是从从Aloc到到Aval的的所所有函数的集合有函数的集合 initA A是任意的常函数是任意的常函数 lookupA A(s, l) = s(l)updateA A(s, l, v)是是函函数数s ，除除了了s (l) = v以以外外，s 等同于等同于s为为了了记记号号上上的的方方便便，下下面面用用init，lookup和和update代替代替initA A，lookupA A和和updateA A 朵泳泡已雷要榔块悼块酶旱册闷挪园晚化洋鳖呻泻匝荆背僚别霄玲柜短值第5部分命令式程序的语义第5部分命令式程序的语义5.2 Kernel语言语言两个问题两个问题为为什什么么不不在在前前三三个个类类别别的的基基础础上上引引入入作作为为状状态态的的函数函数state = loc val，而要引入第，而要引入第4个类别个类别state若那样，则若那样，则lookup和和update成了高阶的函数符号成了高阶的函数符号为为什什么么不不用用一一个个函函数数直直接接从从变变量量映映射射到到值值，而而要要分离出环境和状态分离出环境和状态直直观观上上讲讲，环环境境和和状状态态在在概概念念上上有有区区别别，它它们们分分别对应到实际语言实现的不同机制别对应到实际语言实现的不同机制从从技技术术角角度度说说，Kernel没没有有提提供供声声明明常常量量的的值值的的方式，只能将程序中常量的取值交给环境来确定方式，只能将程序中常量的取值交给环境来确定 算截炊崭徽掂痢辉妓玖脱傣澳坍杀时炎谴堕造共赐态率库配驰冒鞘清碾全第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义5.3.1 表达式的求值表达式的求值操作语义分成两部分操作语义分成两部分表达式的计算表达式的计算语句的执行语句的执行表达式的语义表达式的语义表达式、环境、状态和表达式的语义值之间的一表达式、环境、状态和表达式的语义值之间的一个四元关系个四元关系： M, s eval v环境下标在下面将省略环境下标在下面将省略eval由一个证明系统来给出由一个证明系统来给出欲因扩吭闹丛垒铬院矽生炒成儒烦凰掐擎嘿苯件酚镍矽灌懈编蛮虞吸罗究第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义eval公理公理 x, s eval (x) c, s eval cA Aeval推理规则推理规则 fA A(v1, vk)=vlookupA A(s, l)=v M1, s eval v1 Mk, s eval vk f M1 Mk, s eval v x, s eval l cont x, s eval v惠灼菜删固奢卧税酸醚郡栗能役学艳沈候挚谊毕爸鳖妨仲魂娥辗龚陨恰冒第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义5.3.2 命令的执行命令的执行命令的执行可以用关系命令的执行可以用关系exec来刻画来刻画updateA(s, (x), v)=s M, s eval v x := M, s exec s P1, s exec s P2, s exec s P1;P2, s exec s B, s eval true P1, s exec s if B then P1elseP2, s exec s 牲磅豁嘎秀迈梆意卵史夕秒闸审辽筏榜乍谢伯盔痔荆改勾专礁恐玫趾独张第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义 B, s eval false P2, s exec s if B then P1elseP2, s exec s B, s eval false while B do P od, s exec s B, s eval true P, s exec s while B do P od, s exec s while B do P od, s exec s 派影躁影乱佯搐栗虾傻陋绥旅秦缄芝爸争郸滤巾身涝滤惜闽虽丈彤嗽富燕第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义如果想证明如果想证明 P, s exec s , ,需要观察需要观察P的语法形式的语法形式, ,考察哪条规则是完成该证明的最后一条规则考察哪条规则是完成该证明的最后一条规则例例p := 0;m := 0;while (cont m) n dop := cont m;m := (cont m) +1;od旗岩次捂谐虞麦诀迎细鸡炯尚服诀攻助嘿贴揪兼葱鸭竹详骚觅鞠劣淤婚矿第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;s1 = updateA A s lp 0 m := 0;while (cont m) n dop := cont m;m := (cont m) +1;od诊搜社跟衔罩逐铝帕纷罕泼氰栋茶耙径掐仁攻柒弧伸刨秤铲庆乳痪镇钎英第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;s1 = updateA A s lp 0 m := 0;s2 = updateA A s1 lm 0 while (cont m) n dop := cont m;m := (cont m) +1;od氯告煌酮疮白诱剃拐逞台赵汝探拿乱谢哦庆稼喧焉希愉钳嗓帜寂罗囱紊擎第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n dop := cont m;m := (cont m) +1;od讼腺跋啡何嚏寡钨誉塘颓迫之硒穗颐惊徒辜霜执贤收碟匝设谈盎章审透吞第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n do (cont m) n, s2 eval true p := cont m;m := (cont m) +1;od闪喇纤矩稼狙醛纹诅北订瑟乘眶暑句每揖丁端钉芦酉曙歉愈钢挥私怖程瘴第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n dop := cont m;m := (cont m) +1; (p := cont m; m := (cont m) +1), s2 exec s3od恨奔故哈勺艾捎肛嫌磺涨啮本锐诸俱滁叶撩券棒架瓢影程庞兑硼淡瑚心膘第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n dop := cont m;m := (cont m) +1; lookupA A s3 lp = 0 & & lookupA A s3 lm = 1od附鞭塔瞪窄捆丑掘浪蜗伙胖痢尘瘁桔蜒栏捣茅棘趣低魏吓妹仍哪翁羔灶几第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n do (cont m) n, s3 eval true p := cont m;m := (cont m) +1; lookupA A s3 lp = 0 & & lookupA A s3 lm = 1od虚钢陋捅邹栋瓜聋鬼陪符凹挨冕半断狭沽撼朽士亏韭祷案联悔诧西迫去恫第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n dop := cont m;m := (cont m) +1; lookupA A s3 lp = 0 & & lookupA A s3 lm = 1 (p := cont m; m := (cont m) +1), s3 exec s4 od尼爵憨衰醉彬签暂映书涧覆呵橇善槽冻泪追摈破瓷拼哼昨纳颗阉帽瑞牧蕾第5部分命令式程序的语义第5部分命令式程序的语义5.3 操作语义操作语义p := 0;m := 0;lookupA A s2 lm = lookupA A s2 lp = 0while (cont m) n dop := cont m;m := (cont m) +1; lookupA A s4 lp = 1 & & lookupA A s4 lm = 2 (p := cont m; m := (cont m) +1), s3 exec s4 od猩四硕瘦剁根珠颧调俱盂龟钧疙杀来孜犬捏卒后很鄂勉圃套奏滩拂卞帮座第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义5.4.1带状态的类型化带状态的类型化 演算演算前两章已经给出了类型化前两章已经给出了类型化 演算的指称语义演算的指称语义只只要要给给出出从从Kernel语语言言到到类类型型化化 演演算算的的翻翻译译即可即可把把Kernel程序翻译成程序翻译成类型化类型化 演算演算 state, fix, 该演算有类型常量该演算有类型常量val, bool, loc, state和和state state, fix, 演算还增加的运算演算还增加的运算Eq? : loc loc bool在在state上的运算上的运算init, update和和lookup健炙锻坪召窿沮人孪憨嘛负仙重迅蜕庸话眨譬灼膳轰凶甲阂酋男厢输柠菱第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义每个类型都有条件运算每个类型都有条件运算ifthenelse还还有有提提升升运运算算（在在下下面面描描述述）， 抽抽象象， 应应用用和和不动点算子不动点算子 fixstate : (state state ) (state state ) (state state ) state, fix, 的的CPO模模型型A 是是四四类类别别代代数数A A的的一一个个拓拓展展val, bool, loc和和state的解释同的解释同A A的解释一样的解释一样state 被解释成提升集合被解释成提升集合Astate = (Astate) 这这种种解解释释延延伸伸到到函函数数类类型型, ,Astate state 有有最最小小元元，该该类型有最小不动点算子类型有最小不动点算子 摇椽妓乃瞻触奉哀让还壮尹碗抗绢疲柞鸥茹厚踌侨型见授疮拾宿懂狙卜超第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义提升运算提升运算 : :state state 如果如果M:state, ,让让 M 和和M有同样的有同样的指称但不同的类型指称但不同的类型中中缀算符缀算符 (state Elim) M = : state M N = MN : state 函数合成的严格形式美化成函数合成的严格形式美化成M N s : state. M (N s) M: state state N: state M N: state 千卜昏脉成烦墒泛们晴颓绢呼程捐巷烫绣困树党卜淄颁吱鞭柿坎潭着漱评第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义5.4.2 语义函数语义函数指称语义由两部分组成指称语义由两部分组成表达式和命令表达式和命令到到 state, fix, 项的语法翻译项的语法翻译这个这个 演算演算在模型在模型A 中的标准解释中的标准解释语法翻译部分语法翻译部分函函数数V V : 把把布布尔尔表表达达式式和和值值表表达达式式分分别别翻翻译译成成类型为类型为state bool和和state val的的 项项函函数数C C : : 把把命命令令翻翻译译成成类类型型为为state state 的的 项项柿冒人胰袜纫粳宴夷煤同纺曹安彻寒射禽别囱岗札万沿糠呕幕纫丢除拎轿第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义语义函数语义函数把把这这些些语语法法翻翻译译和和从从 state, fix, 的的项项到到模模型型A 的的标标准含义函数组合起来准含义函数组合起来 : expressions environments Astate Avalues : commands environments Astate Astate 浪榆挪廷糊爆复纱腥巷厅陕处明同吃荷苹撞泊囊把刮贱迈发有问幸耐天函第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义表达式的语法翻译表达式的语法翻译 V V x= s: state. x V V cont x= s: state. lookup s x V V f M1 Mk = s: state. f V V M1s V V Mks表达式表达式M在环境在环境 中的含义中的含义 M = A V V M M s = ( M )s韵议闪纲咀匠脂窜鸵埋咋设尸锰俗你候孺扔棘首示氛绵荔捅厩革血葱诣蚤第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义命令的语法翻译命令的语法翻译 C C x := M = s: state. update s x (V V Ms) C C P1; P2 = C C P2 C C P1 C C if B then P1 else P2 = s: state. if V V Bs then C C P1s else C C P2s C C while B do P od = fix( f : state state . s: state. if V V Bs then (f C C P)s else s ) 程序程序P在环境在环境 下的含义下的含义 P = A C C P P s = ( P ) s驰诈哪按咐仿览谦伸察依攫申友另忽鼠拐绕叮已症柜裂宁咬态枣邯铃孟纹第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义例例 一个简单的程序一个简单的程序skip x := cont xC C skip = s: state. update s x (V V cont xs) = s: state. update s x (lookup s x) = s: state. s skip s = (A C C skip )(s) = (A s: state. s )(s) = s 澈桃常梅桑樟纠入侥兹毡芬窒灰质琶椭怔钓老能玲纷均棉揩目刘潮瀑望徊第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义指称语义可用来证明简单程序之间的等价指称语义可用来证明简单程序之间的等价证明证明while B do P od = if B then (P; while B do P od) else skipC C while B do P od= fix ( f : state state . s: state. if V V Bs then (f C C P)s else s )= s: state. if V V Bs then (C C while B do P od C C P)s else s = C C if B then (P; while B do P od) else skip弥庆哭墒窒站脱脚戳苯采胰搐狱筋斡礁岗子棚谤丁凯墩驯缕正触瘫寺线超第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义6.4.3 操作语义和指称语义的等价操作语义和指称语义的等价引引理理5.1 令令 是是环环境境并并且且s Astate不不是是底底元元。对对任任何何类类型型为为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 A s (x) = cont x s f M1 Mk , s eval fA A(a1, , ak) = f M1 Mk s推滋煎涝铣滑获炳涌当韭嚷弹造映擦遥糊掂躬西孺獭务滇锰坯纹羡景奄寿第5部分命令式程序的语义第5部分命令式程序的语义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 = P m s，Bs = false，且且对对所所有有的的k m，有有P k s = sk 且且Bsk =true注：对注：对P : statestate ，用，用P k s表示把表示把P的的k次严格次严格合成作用到合成作用到s，也就是，也就是P k s P ( (P ( (Ps) ) 爹焊钎殉长郎万涩骏蚀藤续候芬绩话骸情脱憨押啃牧慎椎伍账佑蠢租铱誉第5部分命令式程序的语义第5部分命令式程序的语义5.4 指称语义指称语义定定理理5.3 令令 是是一一个个环环境境，并并且且s, s Astate是任意的是任意的“非底元非底元”状态。状态。对任何程序对任何程序P有有 P, s exec s 当且仅当当且仅当 P s = s 畏剁惑框现臼妇厉腹弄夹鬼触汕叛挂颗突孵瑟氧琢呈柬鸳馁详斯傲啥裹交第5部分命令式程序的语义第5部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言5.5.1 一阶逻辑和部分正确性证明一阶逻辑和部分正确性证明证明证明Kernel程序的性质程序的性质用类型化用类型化 项上的一般证明系统项上的一般证明系统使用更适合于使用更适合于Kernel程序语法的逻辑程序语法的逻辑后一种方式的优点后一种方式的优点不需要学习类型化不需要学习类型化 演算和最小不动点概念演算和最小不动点概念程程序序正正确确与与否否的的大大部部分分直直观观理理由由都都关关联联到到程程序序的的结构结构如如果果证证明明系系统统以以一一种种自自然然的的方方式式反反映映程程序序设设计计语语言言的的结结构构，它它可可能能对对程程序序设设计计风风格格产产生生直直接接的的影影响响筋憋骗涂仁呵鸟锑惋锰败污宋伙喝殷柒焙老闺匠拙呕童甥闷皿恒橙胆阴背第5部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义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 F2 bx.F ( bx. F) 对于对于b bool, val, loc吾黍声嘴稀冗售渣灰奢训颓泥陡娘掌磕哀媳捌涛遭蹿烂荷稿煞窃止钧捂禁第5部分命令式程序的语义第5部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言对对模模型型A 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部分命令式程序的语义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部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言5.5.2 证明规则证明规则逻辑推论规则逻辑推论规则(conseq) 顺序推理规则顺序推理规则(seq)条件推理规则条件推理规则(cond) FPG F F G G F PG FP1G GP2HF P1; P2 HF BP1G F BP2GF if B then P1 else P2 G痈蚀人偶帖玛帅络勇愚吮脉髓酸佛尚惨槐粪埋凛携驴慧育呜尿豌翔尿勿瘩第5部分命令式程序的语义第5部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言赋值公理赋值公理(asg)M cont 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 y cont v x := y cont x cont v / 假假定定没没有有别别名名赋值公理为什么不是正向的赋值公理为什么不是正向的F x := y (cont x)/yF键捅匣拼裕攻揪侣楼写偿妆兄可敦匙批盐乾奄乐送舌教及夸滨虾钟镜迎簿第5部分命令式程序的语义第5部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言while规则规则(while)F叫做循环不变式叫做循环不变式 F B P FF while B do P od F B蛰那名瘟傅闲狙片给谍访栖吨摩乌碳哪毗儿拙骏念春运锥苞爪醋丑滚裸琴第5部分命令式程序的语义第5部分命令式程序的语义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部分命令式程序的语义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部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言5.5.3 可靠性可靠性使用程序的指称语义来证明可靠性使用程序的指称语义来证明可靠性断言语言的证明系统对指称模型可靠断言语言的证明系统对指称模型可靠断断言言语语言言上上的的证证明明系系统统用用的的就就是是经经典典逻逻辑辑的的公公理理和推理规则，它们的可靠性证明比较简单和推理规则，它们的可靠性证明比较简单Hoare逻辑的公理和推理规则对指称模型可靠逻辑的公理和推理规则对指称模型可靠 咱巫星拔撬让抬念蔷舵寿氧扼厅同最盂卜角集兰凭奢岁洗汞甜镁向柳胎吞第5部分命令式程序的语义第5部分命令式程序的语义5.5 Kernel程序的前后断言程序的前后断言5.5.3 可靠性可靠性使用程序的指称语义来证明可靠性使用程序的指称语义来证明可靠性定理定理5.4假定部分正确性规范假定部分正确性规范 F P G 可证，可证，那么那么 F P G 在模型在模型A 中有效中有效只只要要证证明明该该公公理理语语义义中中的的公公理理和和推推理理规规则则对对模模型型A 中都可靠就可以了中都可靠就可以了汽样柿截掇徐宋扭麓咬赊睦姆芥晌蹄有凑豪枪瓢傻狸冤增奄惮镑孪廊摆锗第5部分命令式程序的语义第5部分命令式程序的语义习习 题题 第一次：第一次：5.2，5.6, 5.15(a), (b), (c)骆茅昂帽阿侥币貉拂芬绎顶垫峦茁撩弄姻顿我抬滇莫还撒碗业芹粕只孝份第5部分命令式程序的语义第5部分命令式程序的语义