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