5.1类型在编程语言中的作用 513类型化语言的优点 从工程的观点看,类型化语言有下面一些优点 开发的实惠 较早发现错误 类型信息还具有文档作用 编译的实惠 程序模块可以相互独立地编译 运行的实惠 可得到更有效的空间安排和访问方式
5.1 类型在编程语言中的作用 5.1.3 类型化语言的优点 从工程的观点看，类型化语言有下面一些优点 • 开发的实惠 – 较早发现错误 – 类型信息还具有文档作用 • 编译的实惠 – 程序模块可以相互独立地编译 • 运行的实惠 – 可得到更有效的空间安排和访问方式
52描述类型系统的语言 类型系统主要用来说明编程语言的定型规则, 它独立于类型检查算法 定义一个类型系统,一种重要的设计目标是 存在有效的类型检查算法 类型系统的基本概念可用于各类语言,包括 函数式语言、命令式语言和并行语言等 本节讨论用形式方法来描述类型系统 然后讨论实例语言时:先定义语法,再给出类型 系统的形式描述,最后写出类型检查的翻译方案
5.2 描述类型系统的语言 • 类型系统主要用来说明编程语言的定型规则, 它独立于类型检查算法 • 定义一个类型系统，一种重要的设计目标是 存在有效的类型检查算法 • 类型系统的基本概念可用于各类语言，包括 函数式语言、命令式语言和并行语言等 • 本节讨论用形式方法来描述类型系统 – 然后讨论实例语言时：先定义语法，再给出类型 系统的形式描述，最后写出类型检查的翻译方案
52描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统 自然数表达式(需要定义它的语法) a+b,3 良形公式(逻辑断言,需要定义它的语法) a+b=3,(d=3)∧(c<10) 推理规则 a <b. b<c a < c
5.2 描述类型系统的语言 类型系统的形式化 • 类型系统是一种逻辑系统 有关自然数的逻辑系统 - 自然数表达式（需要定义它的语法） a+b, 3 - 良形公式（逻辑断言，需要定义它的语法） a+b=3, (d=3)(c<10) - 推理规则 a < b, b < c a < c
52描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统类型系统 自然数表达式 类型表达式 a+b,3 int,int→int 良形公式 a+b=3,(d=3)∧(c<10) 推理规则 a <b. b<c a < c
5.2 描述类型系统的语言 类型系统的形式化 • 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int → int - 良形公式 a+b=3, (d=3)(c<10) - 推理规则 a < b, b < c a < c
52描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统类型系统 自然数表达式 类型表达式 a+b,3 int,int→int 良形公式 定型断言 a+b=3, (d=3A(c<10) X: int -X+3: int 推理规则 (左边部分xint称为 a <b. b<c 定型环境) a < c
5.2 描述类型系统的语言 类型系统的形式化 • 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int → int - 良形公式 定型断言 a+b=3, (d=3)(c<10) x:int |– x+3 : int - 推理规则 ( |–左边部分x:int称为 a < b, b < c 定型环境 ) a < c