课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 1.模型理论关心的问题 给定模型M,哪些问题可以由模型M解决；如何 比较模型的表达能力 本次讲座讨论怎样用数 2.程序理论关心的问题学方法证明程序是正确的 给定模型M,如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3.计算理论关心的问题 给定模型M和一类问题，解决该类问题需多少资源
课 程 内 容 • 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何 比较模型的表达能力 2. 程序理论关心的问题 – 给定模型M，如何用模型M解决问题 – 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源2 本次讲座讨论怎样用数 学方法证明程序是正确的
讲座提纲 ,基本知识 -程序验证、程序逻辑、命题逻辑、谓词逻辑 Hoare逻辑 Hoare.三元式、 赋值公理、结构化语句的推理规 则、推论规则 生成验证条件的演算 一最弱前条件演算、生成验证条件的演算 程序验证实例演示 -二分查找程序 3
讲 座 提 纲 • 基本知识 – 程序验证、程序逻辑、命题逻辑、谓词逻辑 • Hoare逻辑 – Hoare三元式、赋值公理、结构化语句的推理规 则、推论规则 • 生成验证条件的演算 – 最弱前条件演算、生成验证条件的演算 • 程序验证实例演示 – 二分查找程序 3
序曲 ·近几年软件错误带来危害的事例 2012年，美国KCP金融公司由于电子交易系统出 现故障，交易算法出错，导致该公司对150支不同 的股票高价购进、低价抛出，直接给公司带来了 4.4亿美元的损失，当天股票下跌62% 2013年9月12日，美联航售票网站一度出现问题， 售出票面价格为0-10美元的超低价机票，引发抢 购。大约15分钟后，美联航发现错误，关闭售票 网站并声称正在进行维护。大约两个多小时后， 该公司售票网站恢复正常，并且承认已卖出的票 有效
序 曲 • 近几年软件错误带来危害的事例 – 2012年，美国KCP金融公司由于电子交易系统出 现故障，交易算法出错，导致该公司对150支不同 的股票高价购进、低价抛出，直接给公司带来了 4.4亿美元的损失，当天股票下跌62% – 2013年9月12日，美联航售票网站一度出现问题， 售出票面价格为0-10美元的超低价机票，引发抢 购。大约15分钟后，美联航发现错误，关闭售票 网站并声称正在进行维护。大约两个多小时后， 该公司售票网站恢复正常，并且承认已卖出的票 有效 4
序曲 软件错误带来危害的事例 据《自然》杂志网站报道，广受世界天文学界期 待的日本旗舰级天文卫星“瞳”(Hitomi)于 2016年2月17日发射升空，但在大约5周之后便出 现翻滚失控迹象。经调查后日本方面宣布，事故 原因源自底层软件错误。卫星的控制系统在发现 飞行姿态失控时，采取了错误的调整，推进器点 火时朝向了错误的反方向，导致自身旋转更加严 重，最终彻底失控
序 曲 • 软件错误带来危害的事例 – 据《自然》杂志网站报道，广受世界天文学界期 待的日本旗舰级天文卫星“瞳”（Hitomi）于 2016年2月17日发射升空，但在大约5周之后便出 现翻滚失控迹象。经调查后日本方面宣布，事故 原因源自底层软件错误。卫星的控制系统在发现 飞行姿态失控时，采取了错误的调整，推进器点 火时朝向了错误的反方向，导致自身旋转更加严 重，最终彻底失控 5
序曲 软件无处不在 全世界有超过10亿辆汽车在行驶，每辆新汽车上 都有20~80个微处理器，有多达3000万行的代码 在运行 全世界每年有多达23亿次手术，在每个现代医疗 设备上往往会有超过30万行的代码在运行 全世界有超过3000辆高速列车在行驶，每辆列车 上会有多达6000万行的代码在运行 -全世界有超过300万架飞机，新型飞机上会有多达 2000万行代码在运行 如何保证这些代码没有错误？
序 曲 • 软件无处不在 – 全世界有超过10亿辆汽车在行驶，每辆新汽车上 都有20～80个微处理器，有多达3000万行的代码 在运行 – 全世界每年有多达23亿次手术，在每个现代医疗 设备上往往会有超过30万行的代码在运行 – 全世界有超过3000辆高速列车在行驶，每辆列车 上会有多达6000万行的代码在运行 – 全世界有超过300万架飞机，新型飞机上会有多达 2000万行代码在运行 如何保证这些代码没有错误？ 6
基本知识 程序：在数组a中快速查找某个值 101521283237 44 49 53 57 6267717783 int am] Vn:[0..m-2].an]a n+1] ·怎样进行测试 -对数组a的长度m(m>0) 的各种情况都要测试吗？ -对a中出现的各个元素都需要测试吗？ -对a中不出现的元素要测多少种情况？
基 本 知 识 • 程序：在数组a中快速查找某个值 int a[m] n:[0..m−2].a[n] 0) 的各种情况都要测试吗？ – 对a中出现的各个元素都需要测试吗？ – 对a中不出现的元素要测多少种情况？ 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 7
基本知识 程序测试与程序验证 测试能发现程序有错；一般而言，硬测试不能保证 程序无错 程序验证：用数学的方法来证明程序的性质，提 高软件可信程度 演绎验证：指用逻辑推理的方法来证明程序具备 所期望的性质 就所期望的性质而言，演绎验证可保证程序无错 程序逻辑：对程序进行推理的逻辑 Q
基 本 知 识 • 程序测试与程序验证 – 测试能发现程序有错；一般而言，测试不能保证 程序无错 – 程序验证：用数学的方法来证明程序的性质，提 高软件可信程度 – 演绎验证：指用逻辑推理的方法来证明程序具备 所期望的性质 就所期望的性质而言，演绎验证可保证程序无错 – 程序逻辑：对程序进行推理的逻辑 8
基本知识 命题逻辑 程序设计中用到命题逻辑的知识 if(0=100){.;n=n+1;} 。!是命题逻辑的一元运算符（下面用一而不是！）
基 本 知 识 • 命题逻辑 程序设计中用到命题逻辑的知识 – if (0 = 100) { …; n = n + 1;} • !是命题逻辑的一元运算符（下面用而不是 !） 9
基本知识 ·命题逻辑 -合式公式(wel-formed formula) 的归纳定义 中：=pl中1pv中|中入中1中→中1（φ） (1)p代表原子命题，例如x>3,a5]=10.5 原子命题具体形式与讨论的问题领域有关 (2)中代表一般命题，“：=”右部用“|”分隔的 各部分代表命题的构成形式，如0<=x人x<100 (3)入，V,一和→代表合取、析取、非和蕴涵运算， 在确定了它们的运算优先关系后，很多情况下括 号可以省略，如pV(q1入q2)可简化为pVq1入q2 备注：蕴涵采用→而不是→，→用于描述函数类型
基 本 知 识 • 命题逻辑 – 合式公式（well-formed formula）的归纳定义 ::= p | | | | | ( ) (1) p代表原子命题，例如 x > 3, a[5] == 10.5 原子命题具体形式与讨论的问题领域有关 (2) 代表一般命题，“::=”右部用“| ”分隔的 各部分代表命题的构成形式，如 0<= x x <100 (3) , , 和代表合取、析取、非和蕴涵运算， 在确定了它们的运算优先关系后，很多情况下括 号可以省略，如p (q1 q2 )可简化为p q1 q2 备注：蕴涵采用而不是→， →用于描述函数类型 10
基本知识 命题逻辑 一推理规则 例：有关合取“入”运算的推理规则 (ne1) φ入 (Ae2) “人i”表示合取引入规则(i:introduction) “人e”表示合取消去规则 (e:elimination) 对和一等也都有各自的推理规则
基 本 知 识 • 命题逻辑 – 推理规则 例：有关合取“”运算的推理规则 ( i) (e1 ) (e2 ) “ i”表示合取引入规则（i: introduction） “ e”表示合取消去规则（e: elimination） 对和等也都有各自的推理规则 11