课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 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