1 类型检查诸概念

程序运行时的执行错误

会被捕获的错误

• 例如：非法指令，非法内存访问，除 0 等。
• 捕获到错误会使计算立刻停止。

不会被捕获的错误

• 例如：下标越界

安全语言

良行为程序

• 没有任何【不会被捕获的错误】的程序

安全语言

• 任何构建于其上的合法程序都是 well-behaved 的
• 设计类型系统，通过静态类型检查来拒绝不会被捕获的错误

设计正好只拒绝 不会被捕获错误 的类型系统是困难的。

实际上往往是拒绝禁止错误（forbidden error）

• 不会被捕获错误 + 会被捕获错误的一个子集

类型及语言

变量类型限定了变量在程序执行期间的取值范围。

类型化的语言：C/C++, Java, Go

非类型化的语言：LISP, JavaScript, Perl

“类型化” 只是指变量类型是不是静态可确定的。

对于显示类型化语言，类型是语法的一部分。

类型系统

• 语言的组成部分
• 由一组定型规则构成，用来给各种程序构造指派类型
• 用 静态检查 的方式来保证 合法程序 在运行时的 良行为
• 类型系统通过类型表达式、定型断言、定型规则形式化

良类型程序

• 没有类型错误的程序
• 若语言定义中除了类型系统外，没有其他约束，则良类型程序也称为合法程序
• 类型可靠语言：所有良类型程序（合法程序）都是良行为的
• 类型可靠语言一定是安全语言

语法和静态的概念	动态的概念
类型化语言	安全语言
良类型程序	良行为的程序

类型检查

未类型化语言

以通过运行时的类型推断和检查来排除禁止错误

类型化语言

• 类型检查也可以放在运行时完成，但影响效率
• 一般都是静态检查，类型系统被用来支持静态检查
• 通常也需要一些运行时的检查，如数组访问越界检查

一些实际的编程语言并不安全

如 C 语言

• 指针与普通变量共用（union）的危险
• 指针算术运算，强制类型转换，变长参数（不安全但被广泛使用的特征）
• 不安全但被广泛使用的特征

C 的一些问题已经在 C++ 中得以缓和，更多一些问题在 Java 中已得到解决。

本文阅读量