中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第5章 类型检查

第五章类型检查 名》 语法 语法 类型 分析 检查 悟 代生 码 中间 成 表示 器 器 本章内容 静态检查中最典型的部分一类型检查: 类型系统、类型检查、多态函数、重载 忽略其它的静态检查:控制流检查、唯一性检查、 关联名字检查
第五章 类 型 检 查 本章内容 – 静态检查中最典型的部分 — 类型检查: 类型系统、类型检查、多态函数、重载 – 忽略其它的静态检查:控制流检查、唯一性检查、 关联名字检查 语法 分析 器 类型 检查 器 中间 代码 生成 器 语 法 树 语 法 树 中间 表示 记号 流

5.1类型在编程语言中的作用 5.1.1 执行错误和安全语言 介绍一些和程序运行有联系的概念
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 介绍一些和程序运行有联系的概念

5.1类型在编程语言中的作用 5.1.1执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误(trapped error)
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 • 会被捕获的错误(trapped error)

5.1类型在编程语言中的作用 5.1.1执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误(trapped error) 一例:非法指令错误
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 • 会被捕获的错误(trapped error) – 例:非法指令错误

5.1类型在编程语言中的作用 5.1.1执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误(trapped error.) 一例:非法指令错误、非法内存访问
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 • 会被捕获的错误(trapped error) – 例:非法指令错误、非法内存访问

5.1类型在编程语言中的作用 5.1.1执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误(trapped error) -例:非法指令错误、非法内存访问、除数为零 -引起计算立即停止 不会被捕获的错误(untrapped error) 例:下标变量的访问越过了数组的末端 例:跳到一个错误的地址,该地址开始的内存正 好代表一个指令序列 错误可能会有一段时间未引起注意
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 • 会被捕获的错误(trapped error) – 例:非法指令错误、非法内存访问、除数为零 – 引起计算立即停止 • 不会被捕获的错误(untrapped error) – 例:下标变量的访问越过了数组的末端 – 例:跳到一个错误的地址,该地址开始的内存正 好代表一个指令序列 – 错误可能会有一段时间未引起注意

5.1类型在编程语言中的作用 5.1.1执行错误和安全语言 2、良行为的程序 不同场合对良行为的定义略有区别 例如,没有任何不会被捕获错误的程序 3、安全语言 任何合法程序都是良行为的 通常是设计一个类型系统,通过静态的类型检查 来拒绝不会被捕获错误 但是,设计一个类型系统,它正好只拒绝不会被 捕获错误是非常困难的
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 2、良行为的程序 – 不同场合对良行为的定义略有区别 – 例如,没有任何不会被捕获错误的程序 3、安全语言 – 任何合法程序都是良行为的 – 通常是设计一个类型系统,通过静态的类型检查 来拒绝不会被捕获错误 – 但是,设计一个类型系统,它正好只拒绝不会被 捕获错误是非常困难的

5.1类型在编程语言中的作用 5.1.1 执行错误和安全语言 禁止错误(forbidden error) -不会被捕获错误集合+会被捕获错误的一个子集 为语言设计类型系统的目标是在排除禁止错误 良行为程序和安全语言也可基于禁止错误 来定义
5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 • 禁止错误(forbidden error) – 不会被捕获错误集合 + 会被捕获错误的一个子集 – 为语言设计类型系统的目标是在排除禁止错误 良行为程序和安全语言也可基于禁止错误 来定义

5.1类型在编程语言中的作用 5.1.2类型化语言和类型系统 4、类型化的语言 变量的类型 变量在程序执行期间的取值范围
5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 • 变量的类型 – 变量在程序执行期间的取值范围

5.1类型在编程语言中的作用 5.1.2类型化语言和类型系统 4、类型化的语言 变量的类型 类型化的语言 变量都被给定类型的语言 表达式、语句等程序构造的类型都可以静态确定 例如,类型boolean的变量x在程序每次运行时的值只能是 布尔值,not(c)总有意义
5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 • 变量的类型 • 类型化的语言 – 变量都被给定类型的语言 – 表达式、语句等程序构造的类型都可以静态确定 – 例如,类型boolean的变量x在程序每次运行时的值只能是 布尔值,not (x)总有意义
按次数下载不扣除下载券;
注册用户24小时内重复下载只扣除一次;
顺序:VIP每日次数-->可用次数-->下载券;
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第4章 语法制导的翻译.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第3章 语法分析.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第2章 词法分析.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第1章 引论(主讲:张昱、陈意云).ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第十讲 大数据的处理和分析.pptx
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第九讲 新型计算模型和顺序交互的数学.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第六讲 计算复杂性和算法分析.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第八讲 多核体系结构与并行编程模型.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第七讲 面向计算机体系结构的程序优化.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第四讲 离散数学与计算机科学.pptx
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第五讲 经典计算的计算模型.pptx
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第三讲 编程语言的类型系统.pptx
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第二讲 对程序进行推理的逻辑.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)第一讲 代数等式理论的自动定理证明.ppt
- 中国科学技术大学:《计算机科学导论》课程教学资源(PPT课件讲稿)课程简介(主讲:陈意云).ppt
- 《计算机学报》:形状图理论的定理证明 Automated theorem proving for theory of shape graphs.pdf
- 形状图逻辑和形状系统 Shape graph logic and shape system.pdf
- A Shape Graph Logic and A Shape System.pdf
- 一个程序验证器的设计和实现 An Automatic Program Verifier for PointerC.pdf
- 处理指针相等关系不确定的指针逻辑 Pointer logic dealing with uncertain equality of pointers.pdf
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第6章 运行时存储空间的组织和管理.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第10章 依赖于机器的优化.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第11章 编译系统和运行系统.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第12章 面向对象语言的编译.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第13章 函数式语言的编译.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第7章 中间代码生成.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第8章 代码生成.ppt
- 中国科学技术大学:《编译原理与技术》课程教学资源(PPT课件讲稿)第9章 独立于机器的优化.ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第1章 引言(主讲:陈意云).ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(课件讲稿)第2章 数据流分析(Nielson等)Principles of Program Analysis - Data Flow Analysis.pdf
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第2章 数据流分析(补充).ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(课件讲稿)第3章 基于约束的分析(Nielson等)Principles of Program Analysis - Control Flow Analysis.pdf
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第3章 基于约束的分析(补充).ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(课件讲稿)第4章 抽象解释(Nielson等)Principles of Program Analysis - Abstract Interpretation.pdf
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第4章 抽象解释(补充).ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(课件讲稿)第5章 类型和效果系统(Nielson等)Principles of Program Analysis - Type and Effect Systems.pdf
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第5章 类型和效果系统(补充).ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第6章 模型检测.ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第7章 程序验证 Program verification.ppt
- 中国科学技术大学:《程序分析与程序验证》课程教学资源(PPT课件讲稿)第7章 程序验证 ProgramVerification Necula 01 Theorem Proving.ppt