对程序进行推理的逻辑对程序进行推理的逻辑计算机科学导论第二讲计算机科学导论第二讲计算机科学技术学院计算机科学技术学院陈意云陈意云0551-63607043yiyunustc.edu.cn修揽舟庙坠韶慷猖较节陡鉴脑福匪粥耪柯骋舱楞右绽藻巢甚哮酥鞠衅捞捎对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲课课 程程 内内 容容课程内容课程内容围绕学科理论体系中的模型理论围绕学科理论体系中的模型理论, 程序理论和计算理论程序理论和计算理论1. 模型理论关心的问题模型理论关心的问题 给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M解决；如何解决；如何比较模型的表达能力比较模型的表达能力2. 程序理论关心的问题程序理论关心的问题给定模型给定模型M，如何用模型，如何用模型M解决问题解决问题包括程序设计范型、包括程序设计范型、程序设计语言程序设计语言、程序设计、程序设计、形式语义、类型论、形式语义、类型论、程序验证程序验证、程序分析程序分析等等3. 计算理论关心的问题计算理论关心的问题给定模型给定模型M和一类问题和一类问题, 解决该类问题需多少资源解决该类问题需多少资源见差毅皂陵匪疥妆晌政笑屹禹柏娃爹趁庚华夷伙立投钢嫩矽妮坦程榨炭畴对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲讲讲 座座 提提 纲纲基本知识基本知识程序验证、程序逻辑、命题逻辑、谓词逻辑程序验证、程序逻辑、命题逻辑、谓词逻辑Hoare逻辑逻辑Hoare三元式、赋值公理、结构化语句的推理规则、三元式、赋值公理、结构化语句的推理规则、推论规则推论规则生成验证条件的演算生成验证条件的演算最弱前条件演算、生成验证条件的演算最弱前条件演算、生成验证条件的演算程序验证实例演示程序验证实例演示二分查找等程序二分查找等程序晒君渠佑戎厅锐疫巧唱映朗声灶俄竖无客曳淄谭晋甄识呛潞过陨养杰厂倦对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲基基 本本 知知 识识程序程序测试与程序与程序验证测试能能发现程序有程序有错；一般而言，；一般而言，测试不能保不能保证程序无程序无错程序验证：用数学的方法来证明程序的性质，提程序验证：用数学的方法来证明程序的性质，提高软件可信程度高软件可信程度演绎验证：指用逻辑推理的方法来证明程序具备演绎验证：指用逻辑推理的方法来证明程序具备所期望的性质所期望的性质 演绎验证可以保证程序无错演绎验证可以保证程序无错程序程序逻辑：对程序程序进行推理的行推理的逻辑 予跟缕新磷枯姨聂贿辊酒涕旺慎勇擂乙脖赔纬陋艳呛颇了缴淹列笔秆昔漏对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲基基 本本 知知 识识命题逻辑命题逻辑合式公式（合式公式（well-formed formula）的归纳定义）的归纳定义 := p | ( ) | ( ) | ( ) | ( )(1) p代表原子命代表原子命题，例如，例如 x 3, a5 = 10.5 原子命原子命题具体形式与具体形式与讨论的的问题领域有关域有关(2) 代表一般命代表一般命题，“:=”右部用右部用“| ”分隔的各部分隔的各部分代表命分代表命题的构成形式，如的构成形式，如 0= x x 100(3) , , 和和代表合取、析取、非和代表合取、析取、非和蕴含运算，含运算，在确定了它在确定了它们的运算的运算优先关系后，很多情况下括先关系后，很多情况下括号可以省略，如号可以省略，如p (q1 q2)可可简化化为p q1 q2备注：采用注：采用而不是而不是 ， 用于描述函数用于描述函数类型型 峰狭览矩预凉僻锻扛盟褒信痴旦酶林涉麦玫砖宠碾卑整烘囱馈吵云桂饭崔对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲基基 本本 知知 识识命题逻辑命题逻辑推理推理规则例：有关合取例：有关合取“ ”运算的推理运算的推理规则( i)( e1) ( e2)“ i”表示合取引入表示合取引入规则（i: introduction）“ e”表示合取消去表示合取消去规则（e: elimination）对 和和 等都有各自的推理等都有各自的推理规则 闰蕊墙装浩靖拢进杀墟调盾驶蜘汁语鼠繁弄军矽埂娠腕本福撩尼听肪锦府对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲谓词逻辑谓词逻辑合式公式合式公式(1) 谓词集合谓词集合、函数集合、函数集合（包括常量）（包括常量）(2) 基于基于来定义项集来定义项集 t := x | c | f(t, , t) ( f )(3) 归纳地定义基于（归纳地定义基于（ , ）的合式公式）的合式公式 := P(t1, t2, , tn) | ( ) | ( ) | ( ) | ( ) | ( x ) | ( x ) ( P )增加的规则增加的规则全称量全称量词和存在量和存在量词的的证明明规则等等基基 本本 知知 识识醚亲驯恳旭妆睡钻浓鞭泽兰鞠抡豫神酮沫汞彬这缸坷罢奥胃艺观唇沽田辱对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑程序程序逻辑对程序进行推理的逻辑对程序进行推理的逻辑Hoare逻辑是一种程序逻辑逻辑是一种程序逻辑介绍面向非常简单的编程语言（只有赋值语句、介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的顺序语句、条件语句和循环语句）的Hoare逻辑推逻辑推理规则理规则脯仑神破北痰曙裕悯浦慌氨音谤葬丢乘竟胰辕夏膏选只看翼护蔑椿替衍寐对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑合式公式合式公式语法形式：法形式：P S Q，称，称为Hoare三元式三元式(1) S是代是代码段，遵循相段，遵循相应编程程语言的言的语法法(2) P和和Q是关于程序状是关于程序状态（变量到量到值的映射）的的映射）的断言，分断言，分别称称为S的前断言和后断言，断言是的前断言和后断言，断言是谓词逻辑的合式公式的合式公式(3) 例：例： x = 1 y 5 x = x +1 x = 2 y 5P S Q的含的含义：在：在满足足P的状的状态下下执行行S ，若，若执行行终止，止，则终止状止状态满足足Q例：例：x = 1 y 5 x = x +1 x = 2 y 1 y 0 y 6 x = x +1 x 6 是赋值公理的实例是赋值公理的实例特点：特点： x +1 6 （即（即x 5）是语句）是语句x = x+1和后断和后断言言x 6 的最弱前断言的最弱前断言(1) x 5.1和和x 7都可做前断言，因为都强于都可做前断言，因为都强于x 5x 5.1 x 5 并且并且x 7 x 5(2) 若若x 4.9作为前断言，则三元式不成立，因为作为前断言，则三元式不成立，因为x 4.9 x 5不成立不成立耻袄尸装针圣涅信恿绅痉箔浸漓篷合愧馅蔷碉虞导赐厄猴帛砸琉乞斑瘫扫对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑结构化构化语句的推理句的推理规则顺序序语句句条件条件语句（也可用其它形式表示）句（也可用其它形式表示）插曲：推插曲：推论规则P P P S Q Q Q P S Q P E S1 Q P E S2 QP if E then S1 else S2 QP S1 R R S2 QP S1; S2 Q暖上挡兄胳咒抽榜延裴溪企曲层惶粹唉晰艳桐靶宅棋碗询驯生簧晴员但烘对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑例（用例（用Hoare逻辑手中证明简单程序段）逻辑手中证明简单程序段）证：证：true if (x y) z = x else z = y z = x z = y(1)由赋值公理由赋值公理:x = x x =yz = xz = x z =y(2) 由由(1)的所得、的所得、(true x y) (x = x x = y)和推论规则，可得：和推论规则，可得： true x y z = x z = x z = y(3) 同理得同理得: true (x y) z = y z = x z = y(4) 得得: true if (x y) z = x else z = y z = x z = yP E S1 Q P E S2 QP if E then S1 else S2 Q 由条件语句由条件语句的规则的规则斯踏哀安惺始端捡腹耶生播卫京驮主勾辆扳祥递敬弧涵璃煮宫村膏贿跳赂对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑结构化构化语句的推理句的推理规则（续）循循环语句句例：用自然数加法来完成自然数相乘例：用自然数加法来完成自然数相乘x = 0; y = 0; while (y n) /循循环不不变式：式：(x = m y) (y n) x = x + m; y = y + 1; / x = m nI E S II while E do S IEI 被称为被称为 循环不变式循环不变式I E 语句句S和后断言和后断言I的最弱前条件：的最弱前条件：(x = m y y n y n) (x+m = m (y+1) y+1 n)苗产啊蜒篓剥丘舞卜赊千湿淬蠢垃泊帆逃湛瓷顾腊传得匝韧混嗜锄呀有沉对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲Hoare 逻逻 辑辑小结小结用用Hoare逻辑，可以对简单程序进行手工证明逻辑，可以对简单程序进行手工证明手工体现在两方面手工体现在两方面(1) 手工用推理规则进行演算或推理手工用推理规则进行演算或推理(2) 手工进行定理证明（前例遇到蕴含式的证明）手工进行定理证明（前例遇到蕴含式的证明） 第一次讲座对自动定理证明已略有介绍第一次讲座对自动定理证明已略有介绍如何走向自动验证（以函数的正确性验证为例）如何走向自动验证（以函数的正确性验证为例）(1) 函数的前条件和后条件必函数的前条件和后条件必须由由验证者者给出出(2) 把推理把推理规则改造成能自改造成能自动演算的演算演算的演算规则(3) 借助自借助自动定理定理证明器明器半型刀墟荡镰市座奇刘馁漳两漫渺配睛道贿贯恬涧恳巫逐童巢讶沂邦雾嚎对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算最弱前条件（最弱前条件（Weakest Precondition）演算）演算WPWP : 程序集程序集 断言集断言集 断言集断言集 WP(S, Q)：计算：计算P S Q的最弱前条件的最弱前条件PHoare逻辑的赋值公理是最弱前条件演算的一条规逻辑的赋值公理是最弱前条件演算的一条规则则(1) 赋值公理：赋值公理：QE/x x = E Q(2) 赋值语句的赋值语句的WP演算规则：演算规则： WP (x =E, Q) = QE/x抒腺据条逆忿厚镑朋佰材杀瑰埋汕怎洽窟伟缚碉世装丁联霍宪杭迟聚佛憨对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WP若一个函数的前后条件是若一个函数的前后条件是P和和Q，函数的代码是赋，函数的代码是赋值语句序列值语句序列S1, , Sn，那么，那么(1) 逆向从逆向从Sn到到S1连续使用赋值语句的连续使用赋值语句的WP规则，规则，WP(S1, , WP(Sn, Q)它是保证执行上述代码段后得到它是保证执行上述代码段后得到Q的最弱前条件的最弱前条件(2) 若若P WP(S1, , WP(Sn, Q)得证，则代码得证，则代码段段S1, , Sn对前后条件对前后条件P和和Q正确正确(3) P WP(S1, , WP(Sn, Q)称为验证条件称为验证条件鸭哺吕赌殊枚图乏铺烙矗贷酮钳胸到普拟傣农睁供叮脐澜蹭铃朱藩寐微千对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WPWP(x =E, Q) = QE/xQE/x x = E QWP(S1;S2, Q) = WP (S1, WP(S2, Q)WP(if E then S1 else S2, Q) =(WP(S1, Q) E) (WP(S2, Q) E)P S1 R R S2 QP S1; S2 QP E S1 Q P E S2 QP if E then S1 else S2 Q挪时衔诌钥堑孝袖澎拖派茵卿摹莱进蒋劈酒谤脚歇佃庄魂喧花奴柬千柱轰对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WP对于对于WP (while E do S, Q)，演算有可能不终止，演算有可能不终止 假定假定WPk为循环体为循环体S执行执行k次的演算次的演算 WP0(while E do S, Q) = E Q WPi (while E do S, Q) =E WP(S, WPi 1(while E do S, Q) WP() = WP0 () WP1 () WP2 () I E S II while E do S IE WP演算在循环语句演算在循环语句这里遇到了困难这里遇到了困难综虞蔑疆须动砷填搪誊酒使缮收续啄胆刺伊颂拎迪彰糜宠节观截败哎峨津对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WP一些其他规则一些其他规则(1) WP(S, false) = false(2) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2) (3) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2)(4)(5) WP(S, true) = 保证保证S终止的最弱前条件终止的最弱前条件 . 下面考虑解决由循环语句引出的问题下面考虑解决由循环语句引出的问题Q Q WP(S, Q) WP(S, Q ) 戌霸矢置史羔函焦窄楼悄堆鸵路杰架胶吮绝羽宵政擂今昏搐交簧切鞋箱堡对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算生成验证条件的演算生成验证条件的演算VC(verification condition)把把WP演算放宽为演算放宽为VC演算演算, 即并非强求最弱前条件即并非强求最弱前条件(1) 要求验证者提供循环不变式要求验证者提供循环不变式(2) VC(S, Q)强于强于WP(S, Q)(3) VC(S, Q)仍弱于仍弱于P ，即，即P VC(S, Q)WP(S, Q)falsetruestrongweak Precondition(S, Q)最弱前条件最弱前条件 WP(S, Q)验证者提供的前条件验证者提供的前条件P验证条件验证条件VC(S, Q)罩近炉寓官黑帘厂焚兆殴鸡追丘磋博挣瘪悸慨药襄编啄梨詹翁绵夯状痞晕对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲生成验证条件的演算生成验证条件的演算生成验证条件的演算生成验证条件的演算VC(verification condition)除了循环语句外，除了循环语句外，VC演算与演算与WP的一致的一致循环语句的循环语句的VC演算如下，其中演算如下，其中I是循环不变式是循环不变式VC(while E do S, Q) = I x1xn( I E VC(S, I) (I E Q)其中其中x1, , xn是在是在S中被修改的所有变量中被修改的所有变量实际做法实际做法(1) 黄色部分和绿色部分黄色部分和绿色部分 分别作为循环出口和入口的验证条件分别作为循环出口和入口的验证条件(2) I作为继续逆向作为继续逆向VC演算的后断言演算的后断言I E S II while E do S IE虐视捣物轨退轮本撼撩洋嘉烂扦警请方夫疤喊专贮庭糕亨致纫枢巡佃叔搂对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do x = x + m ;y = y + 1 ; 例子：用加运算来例子：用加运算来实现乘运算的函数实现乘运算的函数给喊堪茧曰挎粤温鄂镶贩忿裳邦叫母若戊悉缉景晾调蜗陵辱臻尹挖尿低虑对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0/ 前条件前条件void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do x = x + m ;y = y + 1 ; x = m n / 后条件后条件由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供苇矗曲偏氢饯旭匿我吭早拣半膊氖蒸刷啤绣晕肝陡溜遏踌蹿橱蘑泻办幽钱对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) / 循环不变式循环不变式x = x + m ;y = y + 1 ; x = m n也由程序员提供也由程序员提供褪疥谎预撒饺铅啦劝充嚼嘘挠酚太秋樱摹呐亲莹装签凌翌峰惑星烧鸿脚佳对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) / 循环不变式循环不变式x = x + m ;y = y + 1 ; x = m n函数前后条件、循环不变式函数前后条件、循环不变式都称为断言都称为断言它们看上去像编程语言的布它们看上去像编程语言的布尔表达式尔表达式枷恼魄硕蒲压杰啡橙术振泞俯均达瓜瓮药企杆碟蛾闭猖抉述糖翘盅教辨村对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) / 循环结束程序点的断循环结束程序点的断言言 x = m n毫抿烯训傅吸碎洲蹦聘防下优郸喷疗咽拟渤负笆滔哨尾赔赁厄气飘制蛛颂对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n第第1个验证条件个验证条件厦蹈夯穷都规苫袒塞娘奸果幼戴鬼蕉头袒卵展弛皿软患菱晓厚耽当具多敲对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) x = x + m ;(x = m (y+1) (y+1) n)y = y + 1 ; (x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n 通过最弱前通过最弱前条件演算得到条件演算得到症酌迫歇备豌宦涧活靡崩拄翅都倒慈矮在婿挞余症词涕呀靠阀杰搏惑貉珠对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ;(x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n悼瞬骆鼓赐陕均无帜嘛雨郭虾配蕊湍坛异陀吉病镐咙韩杰贼铂用崇坎芬魏对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ; y = 0 ;(x =m y) (y n) (y n) (x+m =m (y+1) (y+1) n)while (y n) do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ;(x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n第第2个验证条件个验证条件凸杀雏允裁悟菩捻吧峻振截夹烃淡杂胡装绩蹦掏厌荆凶棺风惰襟咋又瑚槛对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x =m y) (y n) (y n) (x+m =m (y+1) (y+1) n)while (y n) do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ;(x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n露荣牧明魁凰败够爽卧织肯全构柑惦饿弓莱蝉彻景敏壹沿迎剁旨熏啄捶跳对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) (0 = m 0) (0 n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x =m y) (y n) (y n) (x+m =m (y+1) (y+1) n)while (y n) do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ;(x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n椅华廓酉柴箩系板葫邻恰扇争换高像派肌氰渝棠步换蜜锤蛋歇今羊短胸慌对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) ( n 0 ) (0 = m 0) (0 n)(0 = m 0) (0 n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x =m y) (y n) (y n) (x+m =m (y+1) (y+1) n)while (y n) do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ;(x = m y) (y n) (x = m y) (y n) (y n) (x = m n) x = m n第第3个验证条件个验证条件糙得浴迪便哟绽缔赁耳嫩菜乘跺巧袁赤灌淡太崔穿脯昭脱鞍晾邮柒核亚咱对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例n 0void mult(int m, int n) ( n 0 ) (0 = m 0) (0 n) x = 0 ; y = 0 ;(x =m y) (y n) (y n) (x+m =m (y+1) (y+1) n)while (y n) do (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n 由自动定理证明器由自动定理证明器由自动定理证明器由自动定理证明器完成验证条件的证明完成验证条件的证明完成验证条件的证明完成验证条件的证明虚锤乘慕榨羊您裹泡拽犁髓嘘此一恒拖簧班兰奏鼓芒召良猿李弗陈辆涧赁对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 38, i = 0, j = 14, k = 7i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点犀储薯竹光斥木弘蜒白晶击环巨釜著褐让喻哲溅皱脱盆尺马柴汇殉腿戮涩对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 38, i = 0, j = 6, k = 3i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点彤历条喻颇航凑堕藤普僧胰乎陪费盯琉百匙北卧贯叁然苞舔艇秘骸隧静挺对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 38, i = 4, j = 6, k = 5i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点阜腋浦谁婆烯硬泻桓朔芯幻厩建佣凶胁妹德趟蛔剂浩拴非默奈呼中赢关咕对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 38, i = 6, j = 6, k = 6i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点堑恒耸爹哦侄佐雏谭酉题怖召累轮羔浸桅谍胯鹤腔模英砾痢嚏若爹为毖名对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 38, i = 6, j = 5, k = 6i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点盎印钉焰循腑措婿唐秆荡仲矿圆附顽弛悍掉雅瘁蹲耐下雕寇键许蓟冉递挠对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 37, i = 4, j = 6, k = 5 （若（若val改成改成37）i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点客毕胖戊蓬浪逼橱吃裁元连纤阵辉禾盾筏粱颜池诚泼析封缸钳山摈帅婶毗对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val = 37, i = 6, j = 4, k = 5 （若（若val改成改成37）i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83jik观察点观察点迄磺袱庙绦壕谤粕耍俗洁英绑孜氰猿博在陈睡概咬泳华竟口跟婶埠览饼跟对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例程序：二分查找的主要程序段和断言程序：二分查找的主要程序段和断言int i, j, k, val, am; /此前有此前有#define m = 15m 0 i = 0 j = m 1 n:0.m 2.an an+1while(i = j) 0 i m 1 j m 1 n:0.m 2.an an+1 ( j i 1 n:j+1.m 1. val an j i = 2 k = i 1 val = ak ) /循环不变式循环不变式 k = i + (j i)/2;/包括黄色部分包括黄色部分 if(val = ak) i = k + 1; n:0.m 2.an an+1 (i j = 2 k = i 1 val = ak i j = 1 n:0.m 1. val != an) 千瑚苞纠窖菌许碘囚悼考撰沥祈致炊鄂庙裁城驭烩氢哺典童氧羌钞命坑魁对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲程程 序序 验验 证证 实实 例例原型系统原型系统验证实例验证实例一维数组一维数组快速排序程序、冒泡排序、二分查找、二叉堆等快速排序程序、冒泡排序、二分查找、二叉堆等易变数据结构易变数据结构下面这些数据类型的插入函数和删除函数等下面这些数据类型的插入函数和删除函数等1、单链表、循环单链表、单链表、循环单链表2、双向变量、循环双向链表、双向变量、循环双向链表3、二叉排序树、平衡树、二叉排序树、平衡树(AVL tree)、 AA 树、树树、树堆堆(treap)、伸展树、伸展树(splay tree)原型系统网址原型系统网址http:/kyhcs.ustcsz.edu.cn/SGL 慨削娇啥绣揽凹喷纸朔塞亢疾亡荧懊式皇援造逞姜霉浑儒癌耶可托钳清解对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲小小 结结本讲座小结本讲座小结介介绍怎怎样从从Hoare逻辑得得到到一一种种对应的的演演算算，最最终得得到到自自动证明明程程序序是是否否具具备所所期期望望性性质的的一一种种方方法法程序验证的应用情况例举程序验证的应用情况例举空客公司在空客公司在A400M军用航空器以及军用航空器以及A380和和A350商商用航空器的开发上，已经用形式证明取代了部分用航空器的开发上，已经用形式证明取代了部分安全攸关嵌入式软件的测试安全攸关嵌入式软件的测试达索航空公司在健壮性的形式验证方面，有约达索航空公司在健壮性的形式验证方面，有约15%的断言是用演绎验证方式证明的的断言是用演绎验证方式证明的相关课程：相关课程：程序设计语言基础、程序设计语言理论程序设计语言基础、程序设计语言理论胎摄砖杨矿定燃惜峪及戴挠镇似崎嘎忿渴茸醒颖听谆兴桃哼辣请奴犀渴黑对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲小小 结结研究方向研究方向提高断言语言的表达能力提高断言语言的表达能力提高自动定理证明器的证明能力提高自动定理证明器的证明能力工具工具实验室：实验室：ESC/Java、Spec#、Ynot和和Why3等等工业界开始应用的有工业界开始应用的有Caveat、 Frama-C和和SPARK参考文献参考文献何伟等译，面向计算机科学的数理逻辑，何伟等译，面向计算机科学的数理逻辑，2007.Yannick Moy, etc. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Software, 30(3):50-57, 2013.薯渣粤驴措击赣栖卜刷挠铡操韵厢此元急筐琶厨跑舆渠漂帛胃抄郁越龙攀对程序进行推理的逻辑计算机科学导论第二讲对程序进行推理的逻辑计算机科学导论第二讲