05 编译器原理与技术---类型检查

1 .第 5 章 类型检查 编译原理与技术

2 .静态 检查中最典型的部分 — 类型检查： 类型系统、类型检查、多态函数、重载 忽略其它的静态检查：控制流检查、唯一性检查、关联名字 检查 5 类型检查 内容提要 语法 分析器 类型 检查器 中间 代码 生成器 语法树 语法树 中间 表示 记号流

3 .编译时的控制流检查的例子 main() { printf ("\ n%ld

4 .编译时的唯一性检查的例子 main() { int i ; switch( i ){ case 10 : printf ("%d

5 .C 语言 称 & 为地址运算符， &a 为变量 a 的地址 数组名代表数组第一个元素的地址 问题 ： 如果 a 是一个数组名，那么表达式 a 和 &a 的 值都是 数组 a 第一个元素的地址，它们的使用 是否有 区别？ 用四个 C 文件的编译报错或运行结果来提示 5 类型检查 例题 3

6 .typedef int A[10][20]; A a ;   A *fun() { return(a); } 该 函数在 Linux 上用 gcc 编译，报告的错误如下 : 第 5 行： warning: return from incompatible pointer type 5 类型检查 例题 3

7 .typedef int A[10][20]; A a ;   A *fun() { return(&a); } 该函数在 Linux 上用 gcc 编译时，没有错误 5 类型检查 例题 3

8 .typedef int A[10][20]; typedef int B[20]; A a ;   B *fun() { return(a); } 该函数在 Linux 上用 gcc 编译时，没有错误 5 类型检查 例题 3

9 .typedef int A[10][20]; A a ; fun() { printf (“% d,%d,%d

10 .结论 ： 对一 个 t 类型的 数组 a [ i 1 ][ i 2 ]…[ i n ] 来说， 表达式 a 的类型是： pointer(array(0.. i 2 –1, … array(0.. i n –1, t)…)) 表达式 &a 的类型是： pointer(array(0.. i 1 –1, … array(0.. i n –1, t)…)) 5 类型检查 例题 3

11 .5.1 类型在编程语言中的作用 第 5 章 类型检查

12 .5.1.1 执行错误和安全语言 介绍一些和程序运行有联系的概念 （ 1 ）程序运行 时的执行错误分成两类 会被捕获的错误（ trapped error ） 例：非法指令 错误 例：非法 内存 访问 例：除数 为零 引起计算立即停止 不会被捕获的错误（ untrapped error ） 例：下标变量的访问越过了数组的末端 例：跳到一个 错误地址 ，该地址开始的内存正好代表一个指令序列 错误可能会有一段时间未引起 注意 5.1 类型在编程语言中的作用

13 .（ 2 ）良 行为的程序 不同场合对良行为的定义略有区别 例如，没有任何不会被捕获错误的程序 （ 3 ）安全 语言 任何合法程序都是良行为 的语言成为安全语言 通常是设计一个类型系统，通过静态的类型检查来拒绝不会被捕获错误 但是，设计一个类型系统，它正好只拒绝不会被捕获错误是非常困难的 （ 4 ）禁止 错误（ forbidden error ） 不会被捕获错误集合 + 会被捕获错误的一个子集 为语言设计类型系统的目标是在排除禁止错误 良 行为程序和安全语言也可基于禁止错误来 定义 5.1 类型在编程语言中的作用

14 .5.1.2 类型化语言和类型系统 （ 1 ）类型 化的语言 变量的类型 变量在程序执行期间的取值范围 类型化的语言 变量都被给定类型的语言 表达式、语句等程序构造的类型都可以静态确定 例如，类型 boolean 的变量 x 在程序每次运行时的值只能是布尔值， not (x) 总有意义 未类型化的语言 不限制变量值范围的语言 ：一 个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个语言未加定义的结果 例如： LISP 语言 5.1 类型在编程语言中的作用

15 .显 式类型化语言 类型是语法的一部分 隐 式类型化的语言 不存在隐式类型化的主流语言，但可能存在忽略类型信息的程序片段，例如不需要程序员声明函数的参数类型 5.1 类型在编程语言中的作用

16 .（ 2 ）类型 系统 语言的组成部分 , 它由一组定型规则（ typing rule ）构成，这组规则用来给各种程序构造指派类型 设计类型系统的根本目的是用静态检查的方式来保证合法程序运行时的良行为 类型系统的形式化 类型表达式、定型断言、定型规则 类型检查算法 通常是静态地完成类型检查 5.1 类型在编程语言中的作用

17 .（ 3 ）良 类型的程序 没有类型错误的程序 （ 4 ）合法 程序 良类型程序（若语言定义中，除了类型系统外，没有用其它方式表示的对程序的约束） （ 5 ）类型 可靠（ type sound ）的语言 所有良类型程序（合法程序）都是良行为的 类型可靠的语言一定是安全的语言 5.1 类型在编程语言中的作用

18 .（ 6 ） 未类型化 语言的类型检查 可以通过彻底的运行时详细检查来排除所有的禁止错误 如 LISP 语言 （ 7 ） 类型化 语言的类型检查 类型检查也可以放在运行时完成，但影响效率 一般都是静态检查，类型系统被用来支持静态检查 静态检查语言通常也需要一些运行时的检查 数组访问越界检查 5.1 类型在编程语言中的作用 语法的和静态的 概念 动态 的概念 类型 化 语言 安全 语言 良 类型 程序 良 行为的程序 类型系统 类型检查

19 .实际使用的一些语言并不安全 禁止错误集合没有囊括所有不会被捕获的错误 Pascal 语言 无标志的变体记录类型 函数类型的参数 C 语言 还有很多不安全的并且被广泛使用的特征，如： 指针算术运算、类型强制、参数个数可变 在语言设计的历史上，安全性考虑不足是因为当时强调代码的执行 效率 5.1 类型在编程语言中的作用

20 .用 C 语言的共用体（ union ）来举例 union U { int u1; int  u2;} u; int  p; u.u1 = 10; p = u.u2;  p = 0; 在 现代语言设计上，安全性的位置越来越重要 C 的一些问题已经在 C++ 中得以缓和 更多一些问题在 Java 中已得到 解决 安全性  效率的平衡 5.1 类型在编程语言中的作用

21 .5.1.3 类型化语言的优点 从 工程的观点看，类型化语言有下面一些优点 开发 的实惠 较早发现错误 类型信息还具有文档作用 编译 的实惠 程序模块可以相互独立地编译 运行 的实惠 可得到更有效的空间安排和访问方式 5.1 类型在编程语言中的作用

22 .5.2 描述类型系统的语言 第 5 章 类型检查

23 .类型系统主要用来说明编程语言的定型规则 , 它独立于类型检查算法 定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法 类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等 本 节讨论用形式方法来描述类型系统 然后讨论实例语言时：先定义语法，再给出类型系统的形式描述，最后写出类型检查的翻译方案 5.2 描述类型系统的语言

24 .类型系统的形式化 类型系统是一种 逻辑系统 5.2 描述类型系统的语言 有关自然数的逻辑系统 - 自然数 表达式 （ 需要定义它的语法） a+b , 3 - 良 形 公式 （ 逻辑断言，需要定义它的语法） a+b =3, ( d=3 ) ^ ( c<10) - 推理规则 a < b, b < c a < c 类型系统 - 类型 表达式 int , int  int - 定型 断言 x : int | – x+3 : int ( | –左边 部分 x:int 称为定型 环境 ) - 定型 规则  |– M : int ,  |– N : int  |– M + N : int

25 .类型系统的形式化 类型表达式 具体语法：出现在编程语言中 抽象语法：出现在定型断言和类型检查的实现中 下一节开始举例 定型 断言 本节讨论它的一般形式 定型 规则 本节讨论它的一般形式 5.2 描述类型系统的语言

26 .5.2.1 断言 断言 的形式  |– S S 的所有自由变量都声明 在  中 其中  是 一个静态定型环境， 如 x 1 :T 1 , …, x n :T n S 的形式随断言形式的不同而不同 断言有三种具体形式 5.2 描述类型系统的语言

27 .环境断言  | –  该断言 表示  是 良形的环境 将用环境推理规则来定义定型环境的 语法 语法断言  | – nat 在 环境  下， nat 是类型表达式 将用语法推理规则来定义类型表达式的 语法 定型断言  | – M : T 在 环境  下 ， M 具有类型 T 例：  | – true : boolean x : nat | – x+1 : nat 将用推理规则来确定程序构造实例的 类型 5.2 描述类型系统的语言

28 .有效断言  | – true : boolean 无效 断言  | – true : nat 5.2 描述类型系统的语言

29 .5.2.2 推理规则 习惯 表示法 前提、结论 公理（若前提为空） 5.2 描述类型系统的语言  1 |– S 1 , …,  n |– S n  |– S