第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 推断算法 – 利用前面的推理系统：需要使用者有足够的远见 来猜测适当的类型及其上的标注 – 利用推断算法：利用一种试探性的猜测（使用标 注变量）而后再被精确化（对变量进行代换）的 机制 – 基础类型系统的算法 – 控制流分析的算法 – 语法上的可靠性和完备性