第五章类型检查.ppt

上传人：sofeeling205

文档编号：374085

上传时间：2018-10-05

格式：PPT

页数：131

大小：1.03MB

《第五章类型检查.ppt》由会员分享，可在线阅读，更多相关《第五章类型检查.ppt（131页珍藏版）》请在麦多课文档分享上搜索。

1、第五章类型检查,本章内容静态检查中最典型的部分类型检查：类型系统、类型检查、多态函数、重载忽略其它的静态检查：控制流检查、唯一性检查、关联名字检查,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言介绍一些和程序运行有联系的概念,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误,5.1 类型在编程语言中的作用,5.

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

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

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

5、型化语言和类型系统 4、类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言类型是语法的一部分,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统 4、类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言隐式类型化的语言不存在隐式类型化的主流语言，但可能存在忽略类型信息的程序片段，例如不需要程序员声明函数的参数类型,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统 5、类型系统语言的组成部分,它由一组定型规则（typing rule）构成，这组规则用来给各种程序构造指派类型设计类型系统的根本目的是用静态检查的方式来保证

6、合法程序运行时的良行为类型系统的形式化类型表达式、定型断言、定型规则类型检查算法通常是静态地完成类型检查,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统 6、良类型的程序没有类型错误的程序 7、合法程序良类型程序（若语言定义中，除了类型系统外，没有用其它方式表示的对程序的约束） 8、类型可靠（type sound）的语言所有良类型程序（合法程序）都是良行为的类型可靠的语言一定是安全的语言,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统语法的和静态的概念动态的概念类型化语言安全语言良类型程序良行为的程序,5.1 类型在编程语言中的作用,5

7、.1.2 类型化语言和类型系统 9、类型检查：未类型化语言可以通过彻底的运行时详细检查来排除所有的禁止错误如LISP语言 10、类型检查：类型化语言类型检查也可以放在运行时完成，但影响效率一般都是静态检查，类型系统被用来支持静态检查静态检查语言通常也需要一些运行时的检查数组访问越界检查,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊括所有不会被捕获的错误 Pascal语言无标志的变体记录类型函数类型的参数,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊

8、括所有不会被捕获的错误 Pascal语言用C语言的共用体（union）来举例union U int u1; int u2; u;int p;u.u1 = 10;p = u.u2;p = 0;,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统实际使用的一些语言并不安全 C语言还有很多不安全的并且被广泛使用的特征，如：指针算术运算、类型强制、参数个数可变在语言设计的历史上，安全性考虑不足是因为当时强调代码的执行效率在现代语言设计上，安全性的位置越来越重要 C的一些问题已经在C+中得以缓和更多一些问题在Java中已得到解决,5.1 类型在编程语言中的作用,5.1.3 类型

9、化语言的优点从工程的观点看，类型化语言有下面一些优点开发的实惠较早发现错误类型信息还具有文档作用编译的实惠程序模块可以相互独立地编译运行的实惠可得到更有效的空间安排和访问方式,5.2 描述类型系统的语言,类型系统主要用来说明编程语言的定型规则,它独立于类型检查算法定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等本节讨论用形式方法来描述类型系统然后讨论实例语言时：先定义语法，再给出类型系统的形式描述，最后写出类型检查的翻译方案,5.2 描述类型系统的语言,类型系统的形式化类型系统是一种逻辑系统

10、有关自然数的逻辑系统 - 自然数表达式（需要定义它的语法）a+b, 3 - 良形公式（逻辑断言，需要定义它的语法）a+b=3, (d=3)(c10) - 推理规则,5.2 描述类型系统的语言,类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 - 自然数表达式类型表达式a+b, 3 int, int int - 良形公式 a+b=3, (d=3)(c10) - 推理规则,5.2 描述类型系统的语言,类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 - 自然数表达式类型表达式a+b, 3 int, int int - 良形公式定型断言a+b=3,

11、 (d=3)(c10) x:int | x+3 : int 推理规则 ( |左边部分x:int称为定型环境 ),5.2 描述类型系统的语言,类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统 - 自然数表达式类型表达式a+b, 3 int, int int - 良形公式定型断言a+b=3, (d=3)(c10) x:int | x+3 : int - 推理规则定型规则,5.2 描述类型系统的语言,类型系统的形式化类型表达式具体语法：出现在编程语言中抽象语法：出现在定型断言和类型检查的实现中下一节开始举例定型断言本节讨论它的一般形式定型规则本节讨论它的一

13、统的语言,有效断言 | true : boolean 无效断言 | true : nat,5.2 描述类型系统的语言,5.2.2 推理规则习惯表示法前提、结论公理、推理规则,5.2 描述类型系统的语言,5.2.2 推理规则（规则名）（注释）推理规则（注释）环境规则(Env ),5.2 描述类型系统的语言,5.2.2 推理规则（规则名）（注释）推理规则（注释）环境规则(Env ) 语法规则(Type Bool),5.2 描述类型系统的语言,5.2.2 推理规则（规则名）（注释）推理规则（注释）环境规则(Env ) 语法规则(Type Bool) 定型规则(Val

14、 +),5.2 描述类型系统的语言,5.2.3 类型检查和类型推断类型检查用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程,5.2 描述类型系统的语言,5.2.3 类型检查和类型推断类型检查用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程类型推断类型信息不完全的情况下的定型判定问题例如：f (x : t) = E 和 f (x) = E的区别,5.3 简单类型检查器的说明,5.3.1 一个简单的语言 P D ; S D D ; D | id : T T boolean | integer | array num of

15、 T | T | T T S id := E | if E then S | while E do S | S ; S E truth | num | id | E mod E | E E | E | E (E ),5.3 简单类型检查器的说明,例i : integer;j : integer;j := i mod 2000,5.3 简单类型检查器的说明,5.3.2 类型系统环境规则 (Env ) (Decl Var)其中id : T是该简单语言的一个声明语句略去了基于程序中所有声明语句来构成整个的规则,5.3 简单类型检查器的说明,语法规则 (Type Bool) (Type Int)(

16、Type Void) void用于表示语句类型表明编程语言和定型断言的类型表达式并非完全一致,5.3 简单类型检查器的说明,语法规则 (Type Ref) (T void) 具体语法： T (Type Array) (T void) (N0)具体语法：array N of T (Type Function) (T1, T2 void)定型断言中的类型表达式用的是抽象语法,5.3 简单类型检查器的说明,定型规则表达式 (Exp Truth) (Exp Num)(Exp Id),5.3 简单类型检查器的说明,定型规则表达式 (Exp Mod) (Exp Index)(0 E2 N1)(Exp D

17、eref),5.3 简单类型检查器的说明,定型规则表达式 (Exp FunCall),5.3 简单类型检查器的说明,定型规则语句 (State Assign) (T=boolean orT= integer)(State If)(State While),5.3 简单类型检查器的说明,定型规则语句 (State Seq),5.3 简单类型检查器的说明,5.3.3 类型检查设计语法制导的类型检查器设计依据是上节的类型系统类型环境的信息进入符号表对类型表达式采用抽象语法具体：array N of T 抽象：array (N, T)T pointer (T) 考虑到报错的需要，增加了类型ty

18、pe_error,5.3 简单类型检查器的说明,5.3.3 类型检查声明语句 D D; D D id : T addtype (id.entry, T.type)addtype：把类型信息填入符号表,5.3 简单类型检查器的说明,5.3.3 类型检查声明语句 D D; D D 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; D D id

19、: 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 of T1 T.type = array(num.val, T1.type),5.3 简单类型检查器的说明,5.3.3 类型检查声明语句 D D; D D id : T addtype (id.entry, T.type) T boolean T.type = boolean T integer T.type = integer T T1 T

20、.type = pointer(T1.type) T array num of T1 T.type = array(num.val, T1.type) T T1 T2 T.type = T1.type T2.type ,5.3 简单类型检查器的说明,类型检查表达式 E truth E.type = boolean E num E.type = integer E id E.type = lookup(id.entry),5.3 简单类型检查器的说明,类型检查表达式 E truth E.type = boolean E num E.type = integer E id E.type = loo

21、kup(id.entry) E E1 mod E2 E.type = if E1.type = integer and E2. type = integer then integerelse type_error ,5.3 简单类型检查器的说明,类型检查表达式 E E1 E2 E.type = if E2. type = integer and E1. type = array(s, t) then telse type_error ,5.3 简单类型检查器的说明,类型检查表达式 E E1 E2 E.type = if E2. type = integer and E1. type = arr

22、ay(s, t) then telse type_error E E1 E.type = if E1.type = pointer(t) then telse type_error ,5.3 简单类型检查器的说明,类型检查表达式 E E1 E2 E.type = if E2. type = integer and E1. type = array(s, t) then telse type_error E E1 E.type = if E1.type = pointer(t) then telse type_error E E1 (E2 ) E. type = if E2 . type = s

23、 andE1. type = s t then t else type_error ,5.3 简单类型检查器的说明,类型检查语句 S id := E if (id.type = E.type ,5.3 简单类型检查器的说明,类型检查语句 S id := E if (id.type = E.type S if E then S1 S. type = if E. type = booleanthen S1. typeelse type_error ,5.3 简单类型检查器的说明,类型检查语句 S while E do S1 S.type = if E.type = boolean then S1.

24、 typeelse type_error ,5.3 简单类型检查器的说明,类型检查语句 S while E do S1 S.type = if E.type = boolean then S1. typeelse type_error S S1; S2 S. type = if S1. type = void andS2. type = void then voidelse type_error ,5.3 简单类型检查器的说明,类型检查程序 P D; S P. type = if S. type = void then voidelse type_error ,5.3 简单类型检查器的说明,5

25、.3.4 类型转换 E E1 op E2 E.type = if E1.type = integer and E2.type = integerthen integerelse if E1.type = integer and E2.type = realthen realelse if E1.type = real and E2.type = integerthen realelse if E1.type = real and E2.type = realthen realelse type_error ,5.4 多态函数,5.4.1 为什么要使用多态函数例：用Pascal语言写不出

26、求表长度的通用程序若有下面的类型type link = cell ;cell = recordinfo : integer;next : linkend;针对这个类型，可以写出下页的表长函数,5.4 多态函数,function length(lptr : link) : integer; var len : integer;beginlen := 0;while lptr nil do beginlen := len + 1;lptr := lptr. nextend;length := len end;,计算过程并不涉及表元的数据类型,但语言的类型系统使得该函数不能通用,5.4 多

27、态函数,例：用ML语言很容易写出求表长度的程序而不必管表元的类型 fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1;,5.4 多态函数,例：用ML语言很容易写出求表长度的程序而不必管表元的类型 fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1;length ( “sun”, “mon”, “tue” ) length ( 10, 9, 8 ) 都等于3,5.4 多态函数,多态函数允许变元的类型有多种不同的情况

28、函数体中的语句的执行能适应变元类型有多种不同的情况（区别于重载的特征）多态算符例如：数组索引、函数应用、通过指针间接访问相应操作的代码段接受不同类型的数组、函数等 C语言手册中关于取地址算符&的论述是：如果运算对象的类型是，那么结果类型是指向的指针”,5.4 多态函数,5.4.2 类型变量 length的类型可以写成.list() integer 允许使用类型变量，还便于讨论未知类型在不要求标识符的声明先于使用的语言中，通过类型变量的使用去确定程序变量的类型,5.4 多态函数,例 function deref (p); beginreturn p end;,5.4 多

29、态函数,例 function deref (p); - 对p的类型一无所知： beginreturn p end;,5.4 多态函数,例 function deref (p); - 对p的类型一无所知： beginreturn p - = pointer( ) end;,5.4 多态函数,例 function deref (p); - 对p的类型一无所知： beginreturn p - = pointer( ) end; deref的类型是. pointer( ) ,5.4 多态函数,5.4.3 一个含多态函数的语言 P D; E 引入类型变量、笛卡 D D; D |

32、型系统中增加的推理规则环境规则 (Env Var)语法规则 (Type Var)(Type Product),5.4 多态函数,类型系统中增加的推理规则语法规则 (Type Parenthesis)(Type Forall)(Type Fresh),5.4 多态函数,类型系统中增加的推理规则定型规则 (Exp Pair)(Exp FunCall)(其中S是T1和T3的最一般的合一代换),5.4 多态函数,5.4.4 代换、实例和合一 1、代换: 类型表达式中的类型变量用其所代表的类型表达式去替换,5.4 多态函数,5.4.4 代换、实例和合一 1、代换: 类型表达

33、式中的类型变量用其所代表的类型表达式去替换 function subst (t : type_expression ) : type_expression; beginif t是基本类型 then return telse if t是类型变量then return S(t)else if t 是t1 t2 then return subst(t1) subst(t2) end,5.4 多态函数,2、实例把subst函数用于t后所得的类型表达式是t的一个实例，用S (t)表示。例子（s t 表示s是t 的实例） pointer( integer ) pointer( ) pointer(

34、 real ) pointer( ) integer integer pointer( ) ,5.4 多态函数,下面左边的类型表达式不是右边的实例integer real 代换不能用于基本类型 integer real 的代换不一致 integer 的所有出现都应该代换,5.4 多态函数,3、合一如果存在某个代换S使得S(t1) = S(t2)，那么这两个表达式t1和t2能够合一 4、最一般的合一代换S S(t1) = S(t2)；对任何其它满足S(t1) = S(t2)的代换S，代换S(t1)是S(t1)的实例,5.4 多态函数,5.4.5 多态函数的类型检查多态函数和

35、普通函数在类型检查上的区别 (1)同一多态函数的不同出现无须变元有相同类型,5.4 多态函数,(2)必须把类型相同的概念推广到类型合一,5.4 多态函数,(2)必须把类型相同的概念推广到类型合一 (3)要记录类型表达式合一的结果,5.4 多态函数,检查多态函数的翻译方案 EE1 (E2 )p = mkleaf (newtypevar);unify (E1. type, mknode ( , E2.type, p) ); E. type = p E E1, E2E. type = mknode ( , E1.type , E2.type) E id E. type = fres

36、h (lookup(id.entry),5.4 多态函数,5.4 多态函数,确定表长度的ML函数 fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1; 为完成类型检查把它用抽象语言来改写（见下一页）,5.4 多态函数,length : ; lptr : ; if : . boolean ; null : . list () boolean ; tl : . list () list () ; 0 : integer ; 1 : integer ; + : integer integer int

37、eger ; match : . ; match ( - 表达式，匹配length函数的length (lptr), - 函数首部和函数体的类型if (null (lptr), 0, length (tl(lptr) +1) ),类型声明部分,5.4 多态函数,5.4 多态函数,5.4 多态函数,5.4 多态函数,fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1; length函数的类型是. list() integer,5.5 类型表达式的等价,当允许对类型表达式命名后：类型表达式是

38、否相同就有了不同的解释出现了结构等价和名字等价两个不同的概念type link = cell; var next : link;last : link;p : cell;q, r : cell;,5.5 类型表达式的等价,5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）type link = cell; var next : link;last : link;p : cell;q, r : cell;,5.5 类型表达式的等价,5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）类型表达式树一样type link = cell; var next

39、 : link;last : link;p : cell;q, r : cell;,5.5 类型表达式的等价,5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）类型表达式树一样相同的类型构造符作用于相同的子表达式 type link = cell; var next : link;last : link;p : cell;q, r : cell;,5.5 类型表达式的等价,5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）有类型名时，用它们所定义的类型表达式代换它们，所得表达式完全相同(类型定义无环时) type link = cell; va

40、r next : link;last : link;p : cell;q, r : cell;,next, last, p, q和r结构等价,cell,cell,5.5 类型表达式的等价,类型表达式的结构等价测试sequiv(s, t) (无类型名时) if s 和 t 是相同的基本类型thenreturn true else if s = array(s1, s2) and t = array(t1, t2) thenreturn sequiv(s1, t1) and sequiv(s2, t2) else if s = s1 s2 and t = t1 t2 thenreturn sequ

41、iv(s1, t1) and sequiv(s2, t2) else if s = pointer (s1) and t = pointer(t1) thenreturn sequiv(s1, t1) else if s = s1 s2 and t = t1 t2 thenreturn squiv(s1, t1) and sequiv(s2, t2) else return false,5.5 类型表达式的等价,5.5.2 类型表达式的名字等价把每个类型名看成是一个可区别的类型type link = cell; var next : link;last : link;p : cell;q,

42、r : cell;,5.5 类型表达式的等价,5.5.2 类型表达式的名字等价把每个类型名看成是一个可区别的类型两个类型表达式名字等价当且仅当这两个类型表达式不进行名字代换就能结构等价 type link = cell; var next : link;last : link;p : cell;q, r : cell;,next和last名字等价 p, q和r名字等价,5.5 类型表达式的等价,Pascal的许多实现用隐含的类型名和每个声明的标识符联系起来 type link = cell; type link = cell; var next : link; np = cell;las

43、t : link; nqr = cell;p : cell; var next : link;q, r : cell; last : link;p : np;q : nqr;r : nqr;,这时，p与q和r 不是名字等价,5.5 类型表达式的等价,注意:类型名字的引入只是类型表达式的一个语法约定问题，它并不像引入类型构造符或类型变量那样能丰富所能表达的类型,5.5 类型表达式的等价,5.5.3 记录类型 (Type Record) (li是有区别的)(Val Record) (li是有区别的)(Val Record Select),5.5 类型表达式的等价,5.5.4 类型表示中的环 typ

44、e link = cell ; cell = recordinfo : integer ; next : link end;,引入环的话，递归定义的类型名可以替换掉,5.5 类型表达式的等价,5.5.4 类型表示中的环 type link = cell ; cell = recordinfo : integer ; next : link end;,结构等价测试过程有可能不终止,5.5 类型表达式的等价,C语言对除记录（结构体）以外的所有类型使用结构等价，而记录类型用的是名字等价，以避免类型图中的环,5.6 函数和算符的重载,重载符号有多个含义，但在每个引用点的含义都是唯一的例如：

45、加法算符+可用于不同类型，“+”是多个函数的名字，而不是一个多态函数的名字在Ada中，( ) 是重载的，A( I ) 有不同含义重载的消除在重载符号的引用点，其含义能确定到唯一,5.6 函数和算符的重载,5.6.1 子表达式的可能类型集合例 Ada语言声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex;,5.6 函数和算符的重载,5.6.1 子表达式的可能类型集合例 Ada语言声明： function “” (i, j : integer ) re

46、turn complex; function “” (x, y : complex ) return complex; 使得算符重载，可能的类型包括： integer integer integer -这是预定义的类型 integer integer complex complex complex complex,5.6 函数和算符的重载,5.6.1 子表达式的可能类型集合例 Ada语言声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex; 使得算符重载，

47、可能的类型包括： integer integer integer 2 (3 5) integer integer complex complex complex complex,5.6 函数和算符的重载,5.6.1 子表达式的可能类型集合例 Ada语言声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex; 使得算符重载，可能的类型包括： integer integer integer 2 (3 5) integer integer complex (3 5) z complex complex complex z是复型,5.6 函数和算符的重载,以函数应用为例，考虑类型检查在每个表达式都有唯一的类型时，函数应用的类型检查是： EE1 (E2 ) E. type = if E2. type = s and E1. type = s t then t else type_ error ,

下载提示：本站仅提供存储空间/不修改/不编辑