《类型和效果系统》PPT课件

《《类型和效果系统》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第5章类型和效果系统内容概述先前介绍的技术可用于类型语言和非类型语言本章讨论如何利用类型上的标注来表达感兴趣的程序分析的性质，在类型检查时完成这样的分析首先用加标注的类型系统来讨论控制流分析及其语义可靠性和其它理论性质然后讨论计算加标注类型的算法，包括算法的可靠性和完备性最后给出一些用类型和效果系统来规范的其它例子：副作用分析、异常分析、区域推导、通信分析第5章类型和效果系统类型和效果系统概要效果系统和加标注的类型系统的融合在效果系统中，断言的典型形式e:12其中告知e运行时发生的事情，例如什么东西被修改、引发异常加标注的类型系统用来表达语言构造的类型上的标注和它子构造的类

2、型上的标注之间的关系第5章类型和效果系统5.1控制流分析以控制流分析为例来介绍加标注的类型系统介绍FUN语言及其类型系统加标注的类型断言加标注的类型系统关注计算到函数抽象的每个子表达式的值标注的等价第5章类型和效果系统5.2理论上的性质操作语义：无环境的自然语义语义的正确性用类型系统得出某表达式的类型是，则该表达式在操作语义下求得的值的类型也是程序分析的解的存在性1、定义标注完全格2、再定义标注类型的完全格3、擦掉标注后是同样定型断言的加标注定型断言集合构成一个Moorefamily第5章类型和效果系统5.3推断算法利用前面的推理系统：需要使用者有足够的远见来猜测适当的类型及

3、其上的标注利用推断算法：利用一种试探性的猜测（使用标注变量）而后再被精确化（对变量进行代换）的机制基础类型系统的算法控制流分析的算法语法上的可靠性和完备性第5章类型和效果系统5.4效果列举一些更复杂、功能更强的类型和效果系统它们是：副作用分析、异常分析、区域推导除了使用子效果外，需要使用子定型、let多态和多态递归实现技术也相应地变得复杂第5章类型和效果系统5.4.1副作用分析对每个表达式，分析哪些存储单元被创建、赋值和读取FUN语言增加赋值语句形式语义为副作用分析设计带标注的类型系统举例第5章类型和效果系统5.4.2异常分析对每个表达式，分析会引发哪些异常FUN语言增加和异常有关

4、的语句形式语义为异常分析设计带标注的类型系统举例第5章类型和效果系统5.4.3区域推理分析存放值的区域什么时候可以回收，以便决定将它们分配在栈上还是堆上FUN语言增加显式的区域信息（存储分配信息）形式语义为区域分析设计的推理系统举例第5章类型和效果系统5.5运行行为用类型和效果系统来分析运行时原子动作的时序特点具体分析并发程序的通信行为：进程创建、通道分配、通道上发送和接受数据FUN语言增加有关并发部分的表达式形式语义（串行部分和并行部分）为通信行为分析设计的推理系统举例