课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 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