第5章类型和效果系统（补充.pptVIP

中国科大 第5章 类型和效果系统 内容概述 先前介绍的技术可用于类型语言和非类型语言 本章讨论如何利用类型上的标注来表达感兴趣的程序分析的性质，在类型检查时完成这样的分析 首先用加标注的类型系统来讨论控制流分析及其语义可靠性和其它理论性质 然后讨论计算加标注类型的算法，包括算法的可靠性和完备性 最后给出一些用类型和效果系统来规范的其它例子：副作用分析、异常分析、区域推导、通信分析 第5章 类型和效果系统 类型和效果系统概要 效果系统和加标注的类型系统的融合 在效果系统中，断言的典型形式 e : ?1 ? ?2 其中?告知e运行时发生的事情，例如什么东西 被修改、引发异常 加标注的类型系统用来表达语言构造的类型上的标注和它子构造的类型上的标注之间的关系 第5章 类型和效果系统 5.1 控制流分析 以控制流分析为例来介绍加标注的类型系统 介绍FUN语言及其类型系统 加标注的类型断言 加标注的类型系统 关注计算到函数抽象的每个子表达式的值 标注的等价 第5章 类型和效果系统 5.2 理论上的性质 操作语义：无环境的自然语义 语义的正确性 用类型系统得出某表达式的类型是?，则该表达 式在操作语义下求得的值的类型也是? 程序分析的解的存在性 1、定义标注完全格 2、再定义标注类型的完全格 3、擦掉标注后是同样定型断言的加标注定型断言集合构成一个Moore family 第5章 类型和效果系统 5.3 推断算法 利用前面的推理系统：需要使用者有足够的远见来猜测适当的类型及其上的标注 利用推断算法：利用一种试探性的猜测（使用标注变量）而后再被精确化（对变量进行代换）的机制 基础类型系统的算法 控制流分析的算法 语法上的可靠性和完备性 第5章 类型和效果系统 5.4 效果 列举一些更复杂、功能更强的类型和效果系统 它们是：副作用分析、异常分析、区域推导 除了使用子效果外，需要使用子定型、let多态和多态递归 实现技术也相应地变得复杂 第5章 类型和效果系统 5.4.1 副作用分析 对每个表达式，分析哪些存储单元被创建、赋值和读取 FUN语言增加赋值语句 形式语义 为副作用分析设计带标注的类型系统 举例 第5章 类型和效果系统 5.4.2 异常分析 对每个表达式，分析会引发哪些异常 FUN语言增加和异常有关的语句 形式语义 为异常分析设计带标注的类型系统 举例 第5章 类型和效果系统 5.4.3 区域推理 分析存放值的区域什么时候可以回收，以便决定将它们分配在栈上还是堆上 FUN语言增加显式的区域信息（存储分配信息） 形式语义 为区域分析设计的推理系统 举例 第5章 类型和效果系统 5.5 运行行为 用类型和效果系统来分析运行时原子动作的时序 特点 具体分析并发程序的通信行为：进程创建、通道 分配、通道上发送和接受数据 FUN语言增加有关并发部分的表达式 形式语义（串行部分和并行部分） 为通信行为分析设计的推理系统 举例 * ?