【编译原理】类型检查

第五章类型检查

静态检查： 编译器必须检查源程序是否满足源语言在语法和语义两个方面的约定。这种检查称为静检查，它诊断和报告程序错误。

静态检查所涉及的内容： 类型检查、控制流检查、唯一性检查和关联名字检查。

执行错误： 程序运行时出现的错误称为执行错误。

执行错误分为会被捕获的错误和不会被捕获的错误。

会被捕获的错误： 会被捕获的错误会引起计算立即停止。

不会被捕获的错误： 不会被捕获的错误的出现不会引起可被捕捉的事件，然后可能引发难以预料的行为。

良行为的程序： 如果一个程序的运行不可能引起不会被捕获错误的出现,那么就称该程序是良行为的。

安全语言： 所有合法程序都是良行为的语言称为安全语言。

通常是设计一个类型系统，通过静态的类型检查来拒绝不会被捕获错误；但是，设计一个类型系统，它正好只拒绝不会被捕获错误是非常困难的。

禁止错误： 对任何一种语言，可以指定所有可能执行错误集合的一个子集作为禁止错误。若是安全语言，则禁止错误应该包括所有不会被捕获的错误，再加上部分会被捕获的错误。

变量的类型： 变量在程序执行期间的取值范围

类型化语言： 若语言的规范为其每种运算都定义了各运算对象和运算结果所允许的类型，则该语言称为类型化语言。

显式类型化语言：在一种语言中，若函数和变量的类型必须显式声明，则该语言被称为显式类型化语言；

隐式类型化语言：类型声明不是必不可少的语言被称为隐式类型化语言。

无类型语言： 语言若不限制变量的取值范围，则称之为无类型语言，它们没有类型，或者说仅有一个包含所有值的泛类型。在这样的语言中，一个运算可以作用于任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个语言未加定义的结果。

类型系统： 在类型化语言中，类型系统由一组定型规则构成，这组规则用来给构成一个程序的各种语言构造指派类型。设计类型系统的根本目的是用静态检查的方式来保证合法程序运行时的良行为，也就是保证语言的安全性。

非形式描述的定型规则的例子有：若M和N都是整型表达式，则M+N也是整型表达式。保证语言安全性的通常做法是为语言设计一个类型系统，通过静态（编译时）检查，动态（运行时）检查或静态检查与运行检查混合的方式来拒绝一切有潜在不安全性的程序。

类型系统主要用来说明编程语言的定型规则，它独立于类型检查算法。定义一个类型系统，一种重要的设计目标是实现有效的类型检查算法。

类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等。

类型系统的形式化：类型表达式、定型断言、定型规则。

类型检查： 类型检查就是根据定型规则来确定程序中各语法构造的类型，类型检查的目的是拒绝那些有类型错误的程序。

类型检查：用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程。

类型推断：类型信息不完全的情况下的定型判定问题。

良类型的程序： 能够通过类型检查的程序称为良类型的程序。

执行错误、良行为程序和安全语言是基于程序运行时特征来定义的,它们是动态的概念；

而类型错误、良类型程序和类型化语言是静态的概念。

类型可靠的语言： 所有良类型程序（合法程序）都是良行为的，类型可靠的语言一定是安全的语言。

类型化语言相比于无类型语言的优点：

开发的实惠。可以较早发现错误。若类型系统设计得很好，类型检查可以发现大部分常见的程序设计错误。对于大规模软件开发来说,接口和模块有方法学上的优点，类型信息在这里可以组织到程序模块的接口中。
编译的实惠。程序模块可以相互独立地编译，每个模块仅依赖于其他模块的接口。大系统的编译可以更有效，因为改变一个模块并不会引起其他模块的重新编译。
运行的实惠。在编译时收集类型信息，保证了在编译时就能知道数据占用空间的大小，因而可得到更有效的空间安排和访问方式，提高了目标代码的运行效率。

类型系统是一种逻辑系统，它主要用来描述编程语言的定型规则，即类型系统中的推理规则。

类型系统独立于类型检查算法。这类似于形式文法可用来描述编程语言的语法，但这种描述独立于语法分析算法。把类型系统从类型检查算法中分离出来是有益的：类型系统属于语言定义,而类型检查算法属于编译器。

断言分为三种：环境断言，语法断言和定型断言。

$\left.$

\begin{array}{l} P \to D; E \\ P \to D; D \\ P \to id : T \\ T \to char \\ T \to integer \\ T \to array [num] o f T_{1} \\ T \to \land T_{1} \\ E \to literal \\ E \to num \\ E \to id \\ E \to E_{1} mod E_{2} \\ E \to E_{1} [E_{2}] \\ E \to E_{1} \land \\ 下 面 几 个 产 生 式 是 独 立 的 ， 相 互 无 关 ， 与 上 面 的 文 法 也 无 关 \\ S \to id := E \\ S \to if E then S_{1} \\ S \to while E do S_{1} \\ S \to S_{1}; S_{2} \\ T \to T_{1}^{'} \to^{'} T_{2} \\ E \to E_{1} (E_{2}) \end{array}

\right.

P \to D; E P \to D; D P \to id : T T \to char T \to integer T \to array [num] o f T_{1} T \to \land T_{1} E \to literal E \to num E \to id E \to E_{1} mod E_{2} E \to E_{1} [E_{2}] E \to E_{1} \land 下 面 几 个 产 生 式 是 独 立 的 ， 相 互 无 关 ， 与 上 面 的 文 法 也 无 关 S \to id : = E S \to if E then S_{1} S \to while E do S_{1} S \to S_{1}; S_{2} T \to T_{1}^{'} \to^{'} T_{2} E \to E_{1} (E_{2})

对类型表达式采用抽象语法表示：

$[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-emjtY3Ih-1656206533093)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200625191.png)]$

$[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-zB7D23mH-1656206533094)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200637548.png)]$

$[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-rJRoIBTY-1656206533095)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200641963.png)]$

$[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-gauAlXZC-1656206533095)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200649559.png)]$

采用定型规则表示：

相关阅读:
数据预处理
linux网络协议栈源码分析 - 网络层IP网际协议
医院设备利用（Use of Hospital Facilities, ACM/ICPC World Finals 1991, UVa212）rust解法
java Object类型转Map
利用改进的YOLOv5模型对玉米和杂草进行精准检测和精准喷洒
【LeetCode】11. 盛最多水的容器
树莓派(Raspberry Pi)miniDLNA服务搭建
纯c语言算法bin文件转换为数组
卷积神经网络结构有哪些,卷积神经网络结构特点
网购窗帘一定要注意的细节 - 好佳居窗帘十大品牌

原文地址：https://blog.csdn.net/weixin_46221946/article/details/125466834

【编译原理】类型检查

第五章 类型检查

第五章类型检查