《第五章 类型检查》由会员分享，可在线阅读，更多相关《第五章 类型检查（131页珍藏版）》请在金锄头文库上搜索。
1、第五章类型检查 本章内容静态检查中最典型的部分 类型检查 类型系统 类型检查 多态函数 重载忽略其它的静态检查 控制流检查 唯一性检查 关联名字检查 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言介绍一些和程序运行有联系的概念 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言1 程序运行时的执行错误分成两类会被捕获的错误 trappederror 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言1 程序运行时的执行错误分成两类会被捕获的错误 trappederror 例 非法指令错误 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言1 程序运行时的执行
2、错误分成两类会被捕获的错误 trappederror 例 非法指令错误 非法内存访问 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言1 程序运行时的执行错误分成两类会被捕获的错误 trappederror 例 非法指令错误 非法内存访问 除数为零引起计算立即停止不会被捕获的错误 untrappederror 例 下标变量的访问越过了数组的末端例 跳到一个错误的地址 该地址开始的内存正好代表一个指令序列错误可能会有一段时间未引起注意 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言2 良行为的程序不同场合对良行为的定义略有区别例如 没有任何不会被捕获错误的程序3 安全语言任
3、何合法程序都是良行为的通常是设计一个类型系统 通过静态的类型检查来拒绝不会被捕获错误但是 设计一个类型系统 它正好只拒绝不会被捕获错误是非常困难的 5 1类型在编程语言中的作用 5 1 1执行错误和安全语言禁止错误 forbiddenerror 不会被捕获错误集合 会被捕获错误的一个子集为语言设计类型系统的目标是在排除禁止错误良行为程序和安全语言也可基于禁止错误来定义 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统4 类型化的语言变量的类型变量在程序执行期间的取值范围 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统4 类型化的语言变量的类型类型化的语言变量都被给定类
4、型的语言表达式 语句等程序构造的类型都可以静态确定例如 类型boolean的变量x在程序每次运行时的值只能是布尔值 not x 总有意义 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统4 类型化的语言变量的类型类型化的语言未类型化的语言不限制变量值范围的语言 一个运算可以作用到任意的运算对象 其结果可能是一个有意义的值 一个错误 一个异常或一个语言未加定义的结果例如 LISP语言 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统4 类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言类型是语法的一部分 5 1类型在编程语言中的作用 5 1 2类型化语言和类型
5、系统4 类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言隐式类型化的语言不存在隐式类型化的主流语言 但可能存在忽略类型信息的程序片段 例如不需要程序员声明函数的参数类型 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统5 类型系统语言的组成部分 它由一组定型规则 typingrule 构成 这组规则用来给各种程序构造指派类型设计类型系统的根本目的是用静态检查的方式来保证合法程序运行时的良行为类型系统的形式化类型表达式 定型断言 定型规则类型检查算法通常是静态地完成类型检查 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统6 良类型的程序没有类型错误的程序7
6、 合法程序良类型程序 若语言定义中 除了类型系统外 没有用其它方式表示的对程序的约束 8 类型可靠 typesound 的语言所有良类型程序 合法程序 都是良行为的类型可靠的语言一定是安全的语言 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统语法的和静态的概念动态的概念类型化语言安全语言良类型程序良行为的程序 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统9 类型检查 未类型化语言可以通过彻底的运行时详细检查来排除所有的禁止错误如LISP语言10 类型检查 类型化语言类型检查也可以放在运行时完成 但影响效率一般都是静态检查 类型系统被用来支持静态检查静态检查语言通常
7、也需要一些运行时的检查数组访问越界检查 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊括所有不会被捕获的错误Pascal语言无标志的变体记录类型函数类型的参数 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊括所有不会被捕获的错误Pascal语言用C语言的共用体 union 来举例unionU intu1 int u2 u int p u u1 10 p u u2 p 0 5 1类型在编程语言中的作用 5 1 2类型化语言和类型系统实际使用的一些语言并不安全C语言还有很多不安全的并
8、且被广泛使用的特征 如 指针算术运算 类型强制 参数个数可变在语言设计的历史上 安全性考虑不足是因为当时强调代码的执行效率在现代语言设计上 安全性的位置越来越重要C的一些问题已经在C 中得以缓和更多一些问题在Java中已得到解决 5 1类型在编程语言中的作用 5 1 3类型化语言的优点从工程的观点看 类型化语言有下面一些优点开发的实惠较早发现错误类型信息还具有文档作用编译的实惠程序模块可以相互独立地编译运行的实惠可得到更有效的空间安排和访问方式 5 2描述类型系统的语言 类型系统主要用来说明编程语言的定型规则 它独立于类型检查算法定义一个类型系统 一种重要的设计目标是存在有效的类型检查算法类型
9、系统的基本概念可用于各类语言 包括函数式语言 命令式语言和并行语言等本节讨论用形式方法来描述类型系统然后讨论实例语言时 先定义语法 再给出类型系统的形式描述 最后写出类型检查的翻译方案 5 2描述类型系统的语言 类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统 自然数表达式 需要定义它的语法 a b 3 良形公式 逻辑断言 需要定义它的语法 a b 3 d 3 c 10 推理规则 5 2描述类型系统的语言 类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 自然数表达式类型表达式a b 3int int int 良形公式a b 3 d 3 c 10 推理规则 5 2描
10、述类型系统的语言 类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 自然数表达式类型表达式a b 3int int int 良形公式定型断言a b 3 d 3 c 10 x int x 3 int推理规则 左边部分x int称为定型环境 5 2描述类型系统的语言 类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 自然数表达式类型表达式a b 3int int int 良形公式定型断言a b 3 d 3 c 10 x int x 3 int 推理规则定型规则 5 2描述类型系统的语言 类型系统的形式化类型表达式具体语法 出现在编程语言中抽象语法 出现在定型断言
11、和类型检查的实现中下一节开始举例定型断言本节讨论它的一般形式定型规则本节讨论它的一般形式 5 2描述类型系统的语言 5 2 1断言断言的形式 SS的所有自由变量都声明在 中其中 是一个静态定型环境 如x1 T1 xn TnS的形式随断言形式的不同而不同断言有三种具体形式 5 2描述类型系统的语言 环境断言 该断言表示 是良形的环境将用推理规则来定义环境的语法 而不是用文法 语法断言 nat在环境 下 nat是类型表达式将用推理规则来定义类型表达式的语法定型断言 M T在环境 下 M具有类型T例 true booleanx nat x 1 nat将用推理规则来确定程序构造实例的类型 5 2描述类
12、型系统的语言 有效断言 true boolean无效断言 true nat 5 2描述类型系统的语言 5 2 2推理规则习惯表示法前提 结论公理 推理规则 5 2描述类型系统的语言 5 2 2推理规则 规则名 注释 推理规则 注释 环境规则 Env 5 2描述类型系统的语言 5 2 2推理规则 规则名 注释 推理规则 注释 环境规则 Env 语法规则 TypeBool 5 2描述类型系统的语言 5 2 2推理规则 规则名 注释 推理规则 注释 环境规则 Env 语法规则 TypeBool 定型规则 Val 5 2描述类型系统的语言 5 2 3类型检查和类型推断类型检查用语法制导的方式 根据上下
13、文有关的定型规则来判定程序构造是否为良类型的程序构造的过程 5 2描述类型系统的语言 5 2 3类型检查和类型推断类型检查用语法制导的方式 根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程类型推断类型信息不完全的情况下的定型判定问题例如 f x t E和f x E的区别 5 3简单类型检查器的说明 5 3 1一个简单的语言P D SD D D id TT boolean integer array num ofT T T TS id E ifEthenS whileEdoS S SE truth num id EmodE E E E E E 5 3简单类型检查器的说明 例i
14、integer j integer j imod2000 5 3简单类型检查器的说明 5 3 2类型系统环境规则 Env DeclVar 其中id T是该简单语言的一个声明语句略去了基于程序中所有声明语句来构成整个 的规则 5 3简单类型检查器的说明 语法规则 TypeBool TypeInt TypeVoid void用于表示语句类型表明编程语言和定型断言的类型表达式并非完全一致 5 3简单类型检查器的说明 语法规则 TypeRef T void 具体语法 T TypeArray T void N 0 具体语法 array N ofT TypeFunction T1 T2 void 定型断言
15、中的类型表达式用的是抽象语法 5 3简单类型检查器的说明 定型规则 表达式 ExpTruth ExpNum ExpId 5 3简单类型检查器的说明 定型规则 表达式 ExpMod ExpIndex 0 E2 N 1 ExpDeref 5 3简单类型检查器的说明 定型规则 表达式 ExpFunCall 5 3简单类型检查器的说明 定型规则 语句 StateAssign T booleanorT integer StateIf StateWhile 5 3简单类型检查器的说明 定型规则 语句 StateSeq 5 3简单类型检查器的说明 5 3 3类型检查设计语法制导的类型检查器设计依据是上节的类
16、型系统类型环境 的信息进入符号表对类型表达式采用抽象语法具体 array N ofT抽象 array N T Tpointer T 考虑到报错的需要 增加了类型type error 5 3简单类型检查器的说明 5 3 3类型检查 声明语句D D DD id T addtype id entry T type addtype 把类型信息填入符号表 5 3简单类型检查器的说明 5 3 3类型检查 声明语句D D DD id T addtype id entry T type T boolean T type boolean T integer T type integer T T1 T type pointer T1 type 5 3简单类型检查器的说明 5 3 3类型检查 声明语句D D DD id T addtype id entry T type T boolean T type boolean T integer T type integer T T1 T type pointer T1 type T array num ofT1 T type array num val T1 t
