跳转到内容

型别安全

本页使用了标题或全文手工转换
维基百科,自由的百科全书

电脑科学中,一部分程式语言具备型别安全(中国台湾用语习惯称型别为型别;依据上下文、意思、特定用语的不同,常称数据为资料)的性质。这个术语在不同的社群中有不同的定义,特别是正规的型别理论上的定义远远强过大多数的程式员的理解,但对于使用型别系统的认知,皆旨在避免必然的错误形式,和不良的程式行为(称为型别错误)。

类型错误(type error)是错误或不期望的程序行为,由不同数据类型的差别所引起,适用于程序的常量、变量、方法(函数),如把整型(int)当作了浮点型(float)。

型别安全可以静态方式实施,及早在编译时期就捕捉到潜藏的错误;或者以动态方式,在执行时期关联型别的资讯,并在必要时检测即将发生的错误。型别安全是程式语言的性质,而不是程式所自有的。例如,有可能以型别不安全的语言,编写出型别安全的程式。在此是以程式语言为主,而不讨论以个人能力维护的型别安全。

某个行为之所以会被程式语言归类为型别错误,通常是因为试图对不适当型别的进行运算。其分类的基本原则是:部分语言设计者和程式员的看法认为,如果所有运算不引起程式瓦解、安全上的瑕疵、或其它明显故障,即为合理的,而不视之为一个错误;其他人则认为所有违背程式员意图的,就是错误的,而且应该标上“不安全”。在静态型别系统中,型别安全通常包含一个保证,所有运算式最终的值都是合理的静态型别成员(比子型别多态性所要求的还要更加精确细微)。

型别安全近似于所谓的记忆体安全(就是限制从记忆体的某处,将任意的位元组合复制到另一处的能力)。例如,某个语言的实作具有若干型别 ,假如存在若干适当长度的位元,且其不为 的正统成员。若该语言允许把那些资料复制到 型别的变数,那个语言就不是型别安全的,因为这些运算可将非 型别的值赋给该变数。反过来说,若该语言型别不安全的程度,最高只到允许将任意整数用作为指标,显然它就不是记忆体安全的。

大部分的静态型别语言,都提供了一定程度的型别安全,而且其严格性更胜于记忆体的安全性。因其型别系统强迫程式员以适当的抽象资料型别定义来使用,即使对记忆体安全或任何可能的灾难而言,并不需如此严格的要求。

定义

Robin Milner 对于型别安全所喊出的口号:

“具备良好型别的程式从不出错。”

这一口号的涵义,取决于语言形式化语义的类别。在指称语义学里,型别安全意谓着一个运算式的值具有良好型别τ,则表达式是一个属于τ的集合的真正的成员。

1994年,Andrew Wright 和 Matthias Felleisen操作语义学定义的公式描述:何谓现今的标准定义,以及对于型别安全的检验技术。根据上述方法,型别安全是以程式语言语义中的两个性质所决定的:

藏存性
程式中的良好型别这一性质,即使转换了语言的法则(即,评价法则或约简法则),也不会有所改变。
进行性
具备良好型别的程式从不卡住,即从不进入一个使其无法进一步转换的未知状态。

这些性质不是无中生有的,而是和程式语言所描述出来的语义相连系,而且各式各样的语言存在著可以此基准来充实的广大的空间。因为“型别良好”程式的概念已是静态语义学的一部分,而“卡住”(或者“搞错”)则是动态语义学方面的属性。

语言的型别安全性

学术研究用途的玩具语言,常会提出型别安全方面的需求。另一方面,许多语言以人工方式所产生的型别安全,证实经常需要上千次的检查。不过,某些语言,如Standard ML,其严格定义了语义,且 Java 也已提供型别安全[来源请求]。其它语言如 Haskell 也被认为是型别安全。暂且不理会语言定义的性质,在执行时期发生的某些错误,应归于实作时的缺陷,或是用了其它语言撰写的程式库;这种错误可能使给定的实作,在某些情况下的型别不再安全。

型别安全语言的记忆体管理

要实现完善的型别安全语言,它至少需要垃圾回收或增加记忆体配置和解配置的限制(本节主要针对前者)。更明确地说,不允许悬置指标横跨不同结构型别的存在。这有一技术上的原因:假定型别语言(如Pascal要求分配的记忆体必须显式释放)。如果存在一个仍旧指向之前的记忆体位址的悬置指标,新的资料结构可能会分配到同一空间。例如,如果初始化一个指向整数区域资料结构的指标,但新物件的指标区域却分配在整数的地方,然后指标区域可借由改变整数区域的值简单改变成任可东西(经由间接引用悬置指标)。因为当指标改变时,尚未指定将会发生什么,所以这个语言就不是型别安全的。大部分型别安全的语言满足使用垃圾回收实现记忆体的管理。

在允许指标算术的语言中,实作垃圾回收器是最好的,所以在型别不安全的语言或型别安全可能失效的语言中,如此实作回收器的程式库是最好的。C 和 C++ 经常使用。

型别安全与强型别

在各种强型别的定义中,其往往成为型别安全的同义词;然而,型别安全与动态型别并不互相排斥。也可将动态型别视为非常宽松的静态型别语言,而且所有语法正确的程式皆具备良好型别;只要它的动态语义学能够保证绝不会有程式“搞错”,它就可以满足上述定义,且可称为型别安全。

参阅

参考资料