程序分析与程序验证.ppt

《程序分析与程序验证.ppt》由会员分享，可在线阅读，更多相关《程序分析与程序验证.ppt（13页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、程序分析与程序验证程序分析与程序验证计算机科学技术系计算机科学技术系陈意云陈意云课课 程程 简简 介介计算机科学的理论体系计算机科学的理论体系1、模型理论、模型理论 关心的问题关心的问题给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M解决解决如何比较模型的表达能力如何比较模型的表达能力 经典计算经典计算确定的图灵机，可计算性理论属于模型理论确定的图灵机，可计算性理论属于模型理论 新型计算新型计算本质特点是交互本质特点是交互(并发、分布、网络、网格、云并发、分布、网络、网格、云)计算和交互的统一模型理论尚未出现计算和交互的统一模型理论尚未出现课课 程程 简简 介介计算机科学的理论体系

2、计算机科学的理论体系2、程序理论、程序理论 关心的问题关心的问题给定模型给定模型M，如何用模型，如何用模型M解决问题解决问题 包括的领域包括的领域程序设计范型、程序设计语言、程序设计、形式程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等语义、类型论、程序验证、程序分析等课课 程程 简简 介介计算机科学的理论体系计算机科学的理论体系3、计算理论、计算理论 关心的问题关心的问题给定模型给定模型M和一类问题，解决该类问题需要多少和一类问题，解决该类问题需要多少资源资源 包括的领域包括的领域计算复杂性理论计算复杂性理论课课 程程 简简 介介作为编译原理的后续课程，可选内容列

3、举：作为编译原理的后续课程，可选内容列举：独立于机器的优化（涉及，但不是重点）独立于机器的优化（涉及，但不是重点）依赖于机器的优化（留给高级系统结构课程）依赖于机器的优化（留给高级系统结构课程）形式语义和类型论（程序设计语言理论课程）形式语义和类型论（程序设计语言理论课程）各各种语言范型的实现技术（不涉及）种语言范型的实现技术（不涉及）提高软件质量的方法提高软件质量的方法1、程序分析、程序分析2、形式验证、形式验证模型检测：模型检测：对软件的数学模型进行系统地全面考察对软件的数学模型进行系统地全面考察程序验证：程序验证：用形式方法对软件进行数学推理用形式方法对软件进行数学推理课课 程程 简简

4、介介本课程概述本课程概述学习学习程序分析和形式验证的基本原理，它们在高程序分析和形式验证的基本原理，它们在高可信软件、代码优化、并行编译等许多方面有广可信软件、代码优化、并行编译等许多方面有广泛应用泛应用学习和讨论各类方法解决的问题、采用的技术、学习和讨论各类方法解决的问题、采用的技术、理论特性、算法等，并说明这些方法之间的关系理论特性、算法等，并说明这些方法之间的关系和不同。这些方法本身跨越多种程序设计语言特和不同。这些方法本身跨越多种程序设计语言特征征课课 程程 简简 介（程序分析原理）介（程序分析原理）什么是程序分析什么是程序分析一种静态（如编译时）的技术，用于预测程序运一种静态（如编译

5、时）的技术，用于预测程序运行时动态布局或行为的一种安全（忠实于语义）行时动态布局或行为的一种安全（忠实于语义）且有效（所需时空少）的近似且有效（所需时空少）的近似程序分析的应用程序分析的应用编译时的代码优化，以避免冗余计算编译时的代码优化，以避免冗余计算公共子表达式删除、无用赋值删除、循环优化公共子表达式删除、无用赋值删除、循环优化一些静态分析工具，用于分析所关心的程序性质一些静态分析工具，用于分析所关心的程序性质程序切片工具、安全性程序切片工具、安全性程序验证程序验证课课 程程 简简 介（程序分析原理）介（程序分析原理）集中在四种主要程序分析方式上集中在四种主要程序分析方式上数据流分析数据流

6、分析(data flow analysis)基于约束的分析基于约束的分析(constraint based analysis)抽象解释抽象解释(abstract interpretation)类型和结果系统类型和结果系统(type and effect system)对每种方式对每种方式描述主要原理，而不是技术的详细介绍描述主要原理，而不是技术的详细介绍怎样用到更复杂编程语言的分析怎样用到更复杂编程语言的分析课课 程程 简简 介（模型检测）介（模型检测）什么是模型检测什么是模型检测验证验证系系统统满满足性足性质质 （）的方法。它操）的方法。它操作在系统的模型作在系统的模型（语义）上，而不是在系

7、统的（语义）上，而不是在系统的描述（语法）上描述（语法）上模型检测的应用模型检测的应用常用于硬件和通信常用于硬件和通信协议协议的的验证验证中中模型检测方法已经在工业界逐步得到应用模型检测方法已经在工业界逐步得到应用，并且并且有一些有一些较较好的工具好的工具课课 程程 简简 介（模型检测）介（模型检测）集中在采用下面两种逻辑的方法上集中在采用下面两种逻辑的方法上线线性性时态逻辑时态逻辑：时间时间是是线线性的性的逻辑逻辑计计算算树逻辑树逻辑：时间时间可以分支的可以分支的逻辑逻辑（时态逻辑时态逻辑：公式的真假不是静：公式的真假不是静态态的）的）模型模型检测检测的大体步的大体步骤骤由用由用户户描述的一

8、个模型开始描述的一个模型开始判断用判断用户户所断言的假所断言的假设设在模型中是否有效在模型中是否有效若无效，若无效，则产则产生由生由执执行行轨轨迹构成的反例迹构成的反例课课 程程 简简 介（程序验证）介（程序验证）什么是程序验证什么是程序验证将基于将基于逻辑证逻辑证明的方法用于程序性明的方法用于程序性质质的的证证明明1、系、系统统的描述是适当的描述是适当逻辑逻辑中的一中的一组组公式公式 2、待、待证证性性质质的的规规范是另一个公式范是另一个公式 3、验证验证就是通就是通过该逻辑过该逻辑来来证证明明 程序程序验证验证的的应应用用对对安全攸关的程序，安全攸关的程序，验证验证所关心的性所关心的性质质

9、软软件的机械件的机械验证验证将改将改进软进软件的生件的生产产率、效率、率、效率、reliability课课 程程 简简 介（程序验证）介（程序验证）程序程序验证验证的大体步的大体步骤骤程序程序员员提供附加了适当断言的程序提供附加了适当断言的程序验证验证条件生成器条件生成器为该为该程序程序产产生生验证验证条件条件定理定理证证明器完成明器完成验证验证条件的条件的证证明明涉及机械验证过程的各主要部分涉及机械验证过程的各主要部分Hoare逻辑逻辑（公理（公理语义语义）、最弱前条件演算）、最弱前条件演算从程序到定理从程序到定理 验证验证条件生成条件生成从定理到从定理到证证明明 自自动动定理定理证证明明课

10、课 程程 简简 介介教材和参考书教材和参考书F.Nielson,H.R.Nielson,and C.Hankin,Principles of Program Analysis,2nd edition,Springer,2005A.V.Aho,M.S.Lam,R.Sethi,and J.D.Ullman,Compilers:Principles,Techniques,and Tools,2nd edition,Addison-Wesley,2007M.Huth and M.Ryan,Logic in Computer Science:Modelling and Reasoning about Systems,Cambridge University Press,Second Edition,2004(有中译本有中译本)教学资源网页：教学资源网页：http:/