chapter5.ppt

第五章 类 型 检 查,本章内容静态检查中最典型的部分 类型检查：类型系统、类型检查、多态函数、重载忽略其它的静态检查：控制流检查、唯一性检查、关联名字检查,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言介绍一些和程序运行有联系的概念,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言1、程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问、除数为零引起计算立即停止不会被捕获的错误（untrapped error）例：下标变量的访问越过了数组的末端例：跳到一个错误的地址，该地址开始的内存正好代表一个指令序列 错误可能会有一段时间未引起注意,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言2、良行为的程序不同场合对良行为的定义略有区别例如，没有任何不会被捕获错误的程序3、安全语言任何合法程序都是良行为的通常是设计一个类型系统，通过静态的类型检查来拒绝不会被捕获错误但是，设计一个类型系统，它正好只拒绝不会被捕获错误是非常困难的,5.1 类型在编程语言中的作用,5.1.1 执行错误和安全语言禁止错误（forbidden error）不会被捕获错误集合+会被捕获错误的一个子集为语言设计类型系统的目标是在排除禁止错误 良行为程序和安全语言也可基于禁止错误来定义,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统4、类型化的语言变量的类型变量在程序执行期间的取值范围,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统4、类型化的语言变量的类型类型化的语言变量都被给定类型的语言表达式、语句等程序构造的类型都可以静态确定例如，类型boolean的变量x在程序每次运行时的值只能是布尔值，not(x)总有意义,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统4、类型化的语言变量的类型类型化的语言未类型化的语言不限制变量值范围的语言：一个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个语言未加定义的结果例如：LISP语言,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统4、类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言类型是语法的一部分,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统4、类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言隐式类型化的语言不存在隐式类型化的主流语言，但可能存在忽略类型信息的程序片段，例如不需要程序员声明函数的参数类型,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统5、类型系统语言的组成部分,它由一组定型规则（typing rule）构成，这组规则用来给各种程序构造指派类型设计类型系统的根本目的是用静态检查的方式来保证合法程序运行时的良行为类型系统的形式化类型表达式、定型断言、定型规则类型检查算法通常是静态地完成类型检查,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统6、良类型的程序没有类型错误的程序7、合法程序良类型程序（若语言定义中，除了类型系统外，没有用其它方式表示的对程序的约束）8、类型可靠（type sound）的语言所有良类型程序（合法程序）都是良行为的类型可靠的语言一定是安全的语言,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统语法的和静态的概念动态的概念类型化语言安全语言良类型程序良行为的程序,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统9、类型检查：未类型化语言可以通过彻底的运行时详细检查来排除所有的禁止错误如LISP语言10、类型检查：类型化语言类型检查也可以放在运行时完成，但影响效率一般都是静态检查，类型系统被用来支持静态检查静态检查语言通常也需要一些运行时的检查数组访问越界检查,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊括所有不会被捕获的错误Pascal语言 无标志的变体记录类型 函数类型的参数,5.1 类型在编程语言中的作用,5.1.2 类型化语言和类型系统实际使用的一些语言并不安全禁止错误集合没有囊括所有不会被捕获的错误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 类型化语言的优点从工程的观点看，类型化语言有下面一些优点 开发的实惠较早发现错误类型信息还具有文档作用 编译的实惠程序模块可以相互独立地编译 运行的实惠可得到更有效的空间安排和访问方式,5.2 描述类型系统的语言,类型系统主要用来说明编程语言的定型规则,它独立于类型检查算法定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等本节讨论用形式方法来描述类型系统然后讨论实例语言时：先定义语法，再给出类型系统的形式描述，最后写出类型检查的翻译方案,5.2 描述类型系统的语言,类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统-自然数表达式（需要定义它的语法）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,(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 描述类型系统的语言,类型系统的形式化类型表达式具体语法：出现在编程语言中抽象语法：出现在定型断言和类型检查的实现中下一节开始举例定型断言本节讨论它的一般形式定型规则本节讨论它的一般形式,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 描述类型系统的语言,有效断言|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+),5.2 描述类型系统的语言,5.2.3 类型检查和类型推断类型检查用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程,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 of T|T|T TS id:=E|if E then S|while E do S|S;SE 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)(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 Deref),5.3 简单类型检查器的说明,定型规则表达式(Exp FunCall),5.3 简单类型检查器的说明,定型规则语句(State Assign)(T=boolean or T=integer)(State If)(State While),5.3 简单类型检查器的说明,定型规则语句(State Seq),5.3 简单类型检查器的说明,5.3.3 类型检查设计语法制导的类型检查器设计依据是上节的类型系统类型环境的信息进入符号表对类型表达式采用抽象语法 具体：array N of T抽象：array(N,T)T pointer(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=booleanT integer T.type=integerT 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=booleanT integer T.type=integerT 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;DD id:T addtype(id.entry,T.type)T boolean T.type=booleanT integer T.type=integerT T1 T.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 truthE.type=boolean E numE.type=integerE idE.type=lookup(id.entry),5.3 简单类型检查器的说明,类型检查表达式E truthE.type=boolean E numE.type=integerE idE.type=lookup(id.entry)E E1 mod E2E.type=if E1.type=integer and E2.type=integer then integer else type_error,5.3 简单类型检查器的说明,类型检查表达式E E1 E2 E.type=if E2.type=integer and E1.type=array(s,t)then t else type_error,5.3 简单类型检查器的说明,类型检查表达式E E1 E2 E.type=if E2.type=integer and E1.type=array(s,t)then t else type_error E E1 E.type=if E1.type=pointer(t)then t else type_error,5.3 简单类型检查器的说明,类型检查表达式E E1 E2 E.type=if E2.type=integer and E1.type=array(s,t)then t else type_error E E1 E.type=if E1.type=pointer(t)then t else type_error E E1(E2)E.type=if E2.type=s and E1.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.type else type_error,5.3 简单类型检查器的说明,类型检查语句S while E do S1S.type=if E.type=boolean then S1.type else type_error,5.3 简单类型检查器的说明,类型检查语句S while E do S1S.type=if E.type=boolean then S1.type else type_error S S1;S2S.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.3.4 类型转换E E1 op E2E.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语言写不出求表长度的通用程序若有下面的类型type link=cell;cell=record info:integer;next:linkend;针对这个类型，可以写出下页的表长函数,5.4 多 态 函 数,function length(lptr:link):integer;var len:integer;beginlen:=0;while lptr nil do begin len:=len+1;lptr:=lptr.nextend;length:=lenend;,计算过程并不涉及表元的数据类型,但语言的类型系统使得该函数不能通用,5.4 多 态 函 数,例：用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 多 态 函 数,多态函数允许变元的类型有多种不同的情况函数体中的语句的执行能适应变元类型有多种不同的情况（区别于重载的特征）多态算符例如：数组索引、函数应用、通过指针间接访问相应操作的代码段接受不同类型的数组、函数等C语言手册中关于取地址算符&的论述是：如果运算对象的类型是，那么结果类型是指向的指针”,5.4 多 态 函 数,5.4.2 类型变量length的类型可以写成.list()integer 允许使用类型变量，还便于讨论未知类型在不要求标识符的声明先于使用的语言中，通过类型变量的使用去确定程序变量的类型,5.4 多 态 函 数,例function deref(p);beginreturn pend;,5.4 多 态 函 数,例function deref(p);-对p的类型一无所知：beginreturn pend;,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|id:Q 儿积类型、多态函数 Q type-variable.Q|T T T T|T T|unary-constructor(T)|basic-type|type-variable|(T)E E(E)|E,E|id,5.4 多 态 函 数,5.4.3 一个含多态函数的语言P D;E 引入类型变量、笛卡D D;D|id:Q 儿积类型、多态函数 Q type-variable.Q|T T T T|T T 这是一个抽象语言,|unary-constructor(T)忽略了函数定义的|basic-type 函数体|type-variable|(T)E E(E)|E,E|id,5.4 多 态 函 数,5.4.3 一个含多态函数的语言P D;ED D;D|id:QQ type-variable.Q|TT T T|T T|unary-constructor(T)一个程序：|basic-type deref:.pointer();|type-variable q:pointer(pointer(integer);|(T)deref(deref(q)E E(E)|E,E|id,5.4 多 态 函 数,类型系统中增加的推理规则环境规则(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、代换:类型表达式中的类型变量用其所代表的类型表达式去替换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(real)pointer()integer integer pointer(),5.4 多 态 函 数,下面左边的类型表达式不是右边的实例integerreal 代换不能用于基本类型integer real 的代换不一致integer 的所有出现都应该代换,