课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 1.模型理论关心的问题 给定模型M,哪些问题可以由模型M解决；如何 比较模型的表达能力 本讲座介绍类型检查的好 2.程序理论关心的问题处，讨论类型系统的设计 给定模型M,如何用模型M解决问题 包括程序设计范型、程序设计语言、 程序设计、 形式语义、类型论、程序验证、程序分析等 3.计算理论关心的问题 给定模型M和一类问题，解决该类问题需多少资源
课 程 内 容 • 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何 比较模型的表达能力 2. 程序理论关心的问题 – 给定模型M，如何用模型M解决问题 – 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 本讲座介绍类型检查的好 处，讨论类型系统的设计 2
讲座提纲 ·了解类型系统的重要性 围绕数组类型的若干实例来解释这个重要性 基本知识 一类型表达式、定型断言、定型规则、类型系统 多态类型 多态函数、类型变量、多态函数的类型推断和类 型检查 依赖类型 依赖类型的实例、编程语言中使用依赖类型的状 况
讲 座 提 纲 • 了解类型系统的重要性 – 围绕数组类型的若干实例来解释这个重要性 • 基本知识 – 类型表达式、定型断言、定型规则、类型系统 • 多态类型 – 多态函数、类型变量、多态函数的类型推断和类 型检查 • 依赖类型 – 依赖类型的实例、编程语言中使用依赖类型的状 况 3
了解类型系统的重要性 编译器对程序进行的检查 语法检查 依据编程语言的语法 类型名、变量名和函数名等先声明后引用的检查 依据先声明后引用的原则 类型检查 依据类型系统 例如，若a是long类型的数组，m是long类型，则 编译器会发现m+“123”和a+3.5都有类型错误 其它检查
了解类型系统的重要性 • 编译器对程序进行的检查 – 语法检查 依据编程语言的语法 – 类型名、变量名和函数名等先声明后引用的检查 依据先声明后引用的原则 – 类型检查 依据类型系统 例如，若a是long类型的数组，m是long类型，则 编译器会发现m + “123”和a + 3.5都有类型错误 – 其它检查 4
了解类型系统的重要性 类型系统 编程语言的组成部分，它由一组定型规则(ypig rule)构成，这组规则用来给各种程序构造（变 量、表达式和函数等)指派类型 ●例1：“若M和N都是long类型的表达式，则M+N 也是long类型的表达式”是非形式描述的定型规则 ●例2：若函数f的某个形参是long类型，则对应的 实参也应是long类型。若对应实参是char、short 和i类型，则系统会自动把它们提升为long类型 设计类型系统的根本目的是用类型检查的方式来 保证合法程序运行时侯的行为是良好的
了解类型系统的重要性 • 类型系统 – 编程语言的组成部分，它由一组定型规则（typing rule）构成，这组规则用来给各种程序构造（变 量、表达式和函数等）指派类型 • 例1: “若M和N都是long类型的表达式, 则M+N 也是long类型的表达式”是非形式描述的定型规则 • 例2：若函数f的某个形参是long类型，则对应的 实参也应是long类型。若对应实参是char、short 和int类型，则系统会自动把它们提升为long类型 – 设计类型系统的根本目的是用类型检查的方式来 保证合法程序运行时侯的行为是良好的 5
了解类型系统的重要性 ,一点个人评论对发行量最大那本C程序设计教材) - 对类型和类型系统介绍不足 没有强调变量、表达式和函数等都具有类型 ·没有强调对各种运算的运算对象和运算结果的 类型都有规定 完全没有数组类型的概念 ·教材：数组是一组有序数据的集合。inta10I定 义一个整型数组，数组名是a,它有10个整型元素 ●1 正确的观点：对于声明inta10],a是元素类型 为int、大小为3的数组类型的一个变量
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – 对类型和类型系统介绍不足 • 没有强调变量、表达式和函数等都具有类型 • 没有强调对各种运算的运算对象和运算结果的 类型都有规定 – 完全没有数组类型的概念 • 教材：数组是一组有序数据的集合。int a[10]定 义一个整型数组，数组名是a，它有10个整型元素 • 正确的观点：对于声明int a[10]，a是元素类型 为int、大小为3的数组类型的一个变量 6
了解类型系统的重要性 ·一点个人评论（对发行量最大那本C程序设计教材） C99有关数组类型的描述 An array type describes a contiguously allocated nonempty set of objects with a particular member object type,called the element type.Array type are characterized by their element type and the number of elements in the array.An array type is said to be derived from its element type,and if its element type is T,the array is sometimes called "array of T
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – C99有关数组类型的描述 An array type describes a contiguously allocated nonempty set of objects with a particular member object type, called the element type. Array type are characterized by their element type and the number of elements in the array. An array type is said to be derived from its element type, and if its element type is T, the array is sometimes called “array of T ”. 7
了解类型系统的重要性 ,一点个人评论对发行量最大那本C程序设计教材) 没有数组类型的概念，多维数组的描述虽直观， 但不清晰 教材：f1 oat payl3]I6]定义一个f1oat型的二维数 组，第1维有3个元素，第2维有6个元素。二维数组 可看作一种特殊的一维数组，其元素又是一个数组 ● 正确的观点：对于声明float pay[3]I6],pay是 大小为3的一种数组类型的变量，该数组类型的元 素的类型是：大小为6、元素类型为f1oat的数组类型 介绍程序员自己定义数据类型和关键字typedef的 介绍太晚
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – 没有数组类型的概念，多维数组的描述虽直观， 但不清晰 • 教材：float pay[3][6]定义一个float型的二维数 组，第1维有3个元素，第2维有6个元素。二维数组 可看作一种特殊的一维数组，其元素又是一个数组 • 正确的观点： 对于声明float pay[3][6]，pay是 大小为3的一种数组类型的变量，该数组类型的元 素的类型是: 大小为6、元素类型为float的数组类型 – 介绍程序员自己定义数据类型和关键字typedef的 介绍太晚 8
了解类型系统的重要性 一点个人评论对发行量最大那本C程序设计教材) -例1：读者难以理解编译器就下面▣代码报告的错误 typedef int array 100]50]; void f(array a)a]10; main()int b[50][100];f(b); 该函数在Liux上用GCC编译，报告的错误如下： ●第2行： incompatible types when assigning to int50]'from type 'int' ●第3行：expected int(*)儿50]'，but argument is of type 'int (*100]
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – 例1: 读者难以理解编译器就下面代码报告的错误 typedef int array[100][50]; void f(array a) { a[0] = 10; } main( ) { int b[50][100]; f(b); } – 该函数在Linux上用GCC编译, 报告的错误如下： • 第2行： incompatible types when assigning to ‘int[50]’ from type ‘int’ • 第3行： expected ‘int (*)[50]’, but argument is of type ‘int (*)[100]’ 9
了解类型系统的重要性 ·一点个人评论（对发行量最大那本C程序设计教材） 解释一下指针运算符“*” ●long al10l; a-> 10 ·a和a+n分别代表数组a a+1-> 20 的第1和第n个元素的地址 。*a表示取相应地址的内容 ●*a和a0]都等于10 。*(a+1)和a1]都等于20
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – 解释一下指针运算符“*” • long a[10]; • a和a+n分别代表数组a 的第1和第n个元素的地址 • *a表示取相应地址的内容 • *a和a[0]都等于10 • *(a+1)和a[1]都等于20 10 10 20 a → a+1 →
了解类型系统的重要性 ·一点个人评论（对发行量最大那本C程序设计教材） 一例2：读者难以理解编译器就下面代码报告的错误 long a[10][10]; a[0][0] main(){*(a+1)=a+1;} a0][1] 该函数在Linux上用GCC编译， a1]0 报告的错误如下： a11] incompatible types when assigning to long int10]'from ●。 type 'long int (*)[10] a[90] a91
了解类型系统的重要性 • 一点个人评论(对发行量最大那本C程序设计教材) – 例2: 读者难以理解编译器就下面代码报告的错误 long a[10][10]; main( ) { *(a + 1) = a + 1; } – 该函数在Linux上用GCC编译, 报告的错误如下： incompatible types when assigning to ‘long int[10]’ from type ‘long int (*)[10]’ … … 11 … … a[9][0] a[9][1] a[1][0] a[1][1] … … a[0][0] a[0][1] … … a →