第第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语言增加有关并发部分的表达式语言增加有关并发部分的表达式形式语义（串行部分和并行部分）形式语义（串行部分和并行部分）为通信行为分析设计的推理系统为通信行为分析设计的推理系统举例举例