当前位置：网站首页>[compilation principle] type check

[compilation principle] type check

2022-06-29 20:03:00 【No card, no change】

The fifth chapter Type checking

Static check ： The compiler must check whether the source program meets the conventions of the source language in terms of syntax and semantics . This inspection is called static inspection , It diagnoses and reports program errors .

What is involved in static inspection ： Type checking 、 control flow Check 、 Uniqueness check and associated name check .

Perform error ： An error that occurs when a program is running is called an execution error .

Execution errors are divided into those that will be captured and those that will not be captured .

Errors that will be captured ： Errors that will be caught will cause the calculation to stop immediately .

Errors that will not be captured ： The occurrence of errors that will not be captured will not cause events that can be captured , Then it may lead to unpredictable behavior .

The process of good behavior ： If the operation of a program is impossible to cause errors that will not be captured , Then call the program good behavior .

Security Language ： A language in which all legitimate programs are good behavior is called a safe language .

It's usually about designing a type system , Rejecting by static type checking will not catch errors ; however , Design a type system , It just happens that it is very difficult to reject errors that will not be caught .

Prohibit errors ： For any language , You can specify a subset of all possible execution errors as forbidden errors . If it is a safety language , The Forbidden error should include all the errors that will not be captured , Plus some errors that will be caught .

The type of variable ： The value range of variables during program execution

Typed language ： If the specification of a language defines the types allowed for each operation object and operation result for each operation , The language is called a typed language .

Explicitly typed languages ： In a language , If types of the functions and variables must be explicitly declared , The language is called an explicitly typed language ;
Implicitly typed languages ： A language in which type declarations are not essential is called an implicitly typed language .

Untyped language ： If the language does not limit the value range of variables , It is called a typeless language , They have no type , Or just one generic type that contains all the values . In such a language , An operation can be applied to any operand , The result may be a meaningful value 、 A mistake 、 An exception or an undefined result of a language .

Type system ： In typed languages , The type system consists of a set of stereotypes , This set of rules is used to assign types to the various language constructs that make up a program . The fundamental purpose of designing a type system is to ensure the good behavior of legitimate programs by means of static checking , That is to ensure the security of the language .

Examples of stereotyped rules for informal descriptions are ： if M and N Are all integer expressions , be M+N It is also an integer expression . A common approach to language security is to design a type system for the language , By static （ Compile time ） Check , dynamic （ Runtime ） Check or mix static check with running check to reject all potentially unsafe programs .
The type system is mainly used to describe the stereotypes of programming languages , It is independent of the type checking algorithm . Define a type system , An important design goal is to implement an efficient type checking algorithm .
The basic concepts of a type system can be applied to various languages , Including functional languages 、 Imperative language and parallel language .

Formalization of type systems ： Type expression 、 Stereotype assertion 、 Stereotype rules .

Type checking ： Type checking is to determine the type of each syntax construct in the program according to the stereotype rules , The purpose of type checking is to reject programs that have type errors .

Type checking ： In a grammar guided way , The process of determining whether a program construct is a good type of program construct according to the context dependent stereotype rules .
Type inference ： The problem of type determination when the type information is incomplete .

A good type of program ： A program that can pass the type check is called a well typed program .

Perform error 、 Good behavior programs and security languages are defined based on the characteristics of program runtime , They are dynamic concepts ;
And the type is wrong 、 Well typed programs and typed languages are static concepts .

Well typed languages ： All good type programs （ Legal procedures ） It's all good behavior , A well typed language must be a safe language .

The advantages of typed languages over untyped languages ：

The benefits of development . Errors can be found earlier . If the type system is well designed , Type checking can find most common programming errors . For large-scale software development , Interfaces and modules have methodological advantages , Here, the type information can be organized into the interface of the program module .
The benefits of compilation . Program modules can be compiled independently of each other , Each module depends only on the interfaces of other modules . Compilation of large systems can be more efficient , Because changing one module does not cause recompilation of other modules .
The benefits of operation . Collect type information at compile time , This ensures that you can know the size of the data space when compiling , Thus, more effective space arrangement and access mode can be obtained , It improves the running efficiency of the object code .

A type system is a logical system , It is mainly used to describe the stereotypes of programming languages , That is, the inference rules in the type system .
The type system is independent of the type checking algorithm . This is similar to the formal grammar that can be used to describe the syntax of a programming language , But this description is independent of the parsing algorithm . It is useful to separate the type system from the type checking algorithm ： The type system belongs to the language definition , The type checking algorithm belongs to the compiler .

There are three kinds of assertions ： Environment assertion , Syntax assertions and stereotype assertions .

$\left. \begin{array}{l} P\rightarrow D;E \\ P\rightarrow D;D \\ P\rightarrow \textbf{id}:T \\ T\rightarrow \textbf{char} \\ T\rightarrow \textbf{integer}\\ T\rightarrow \textbf{array}[\textbf{num}]\space of\space T_1\\ T\rightarrow \land T_1 \\ E\rightarrow \textbf{literal} \\ E\rightarrow \textbf{num} \\ E\rightarrow \textbf{id} \\ E\rightarrow E_1\space \textbf{mod}\space E_2 \\ E\rightarrow E_1[E_2] \\ E\rightarrow E_1\land \\ \\ The following productions are independent , Independent of each other , It has nothing to do with the grammar above \\\\ S\rightarrow \textbf{id}:=E\\ S\rightarrow \textbf{if}\space E\space \textbf{then}\space S_1 \\ S\rightarrow \textbf{while}\space E\space \textbf{do} \space S_1 \\ S\rightarrow S_1;S_2 \\ T\rightarrow T_1\space'\rightarrow'T_2\\ E\rightarrow E_1(E_2) \\ \end{array} \right.$

Use abstract syntax to express type expressions ：

$[ Failed to transfer the external chain picture , The origin station may have anti-theft chain mechanism , It is suggested to save the pictures and upload them directly (img-emjtY3Ih-1656206533093)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200625191.png)]$

$[ Failed to transfer the external chain picture , The origin station may have anti-theft chain mechanism , It is suggested to save the pictures and upload them directly (img-zB7D23mH-1656206533094)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200637548.png)]$

$[ Failed to transfer the external chain picture , The origin station may have anti-theft chain mechanism , It is suggested to save the pictures and upload them directly (img-rJRoIBTY-1656206533095)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200641963.png)]$

$[ Failed to transfer the external chain picture , The origin station may have anti-theft chain mechanism , It is suggested to save the pictures and upload them directly (img-gauAlXZC-1656206533095)(C:\Users\23343\AppData\Roaming\Typora\typora-user-images\image-20220617200649559.png)]$