【PL理论】(31) 类型系统:静态分析 (Static Analysis) | 静态类型系统 | 什么是类型?

2024-06-18 16:36

本文主要是介绍【PL理论】(31) 类型系统:静态分析 (Static Analysis) | 静态类型系统 | 什么是类型?,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

  • 💭 写在前面:本章我们将进入类型系统的讲解,回顾一下之前我们整理的 F- 语言,然后介绍一下静态分析和静态类型系统。讨论程序员该如何处理一些 bug,有没有完美的静态分析器。

目录

0x00 回顾:F- 语言

0x01 静态分析(Static Analysis)

0x02 静态类型系统(Static Type System)

0x03 什么是类型?


0x00 回顾:F- 语言

我们之前定义了简化版 F# 的语法和语义,并将其命名为 F-。

这是没有匿名 / 递归函数的版本:

我们还实现了一个解释器,根据语义定义运行程序,程序的执行意味着对F中的表达式进行求值。

floyd:~/Lab3$ cd FMinus/
floyd:~/Lab3/FMinus$ ls
FMinus.fsproj src testcase
floyd:~/Lab3/FMinus$ ls src
AST.fs FMinus.fs Lexer.fsl Main.fs Parser.fsy Types.fs(let rec evalExp (exp: Exp) (env: Env) : Val =)

请记住,某些在语法上有效的 F 程序未定义其语义。直观地说,这种情况相当于程序错误(漏洞),例如:类型不匹配、使用未绑定变量、除零错误,到目前为止,这些错误是在运行时捕获的(通过引发异常)

在现实世界中的编程语言中,还可能存在各种其他类型的错误(bug),例如:缓冲区溢出、悬空指针、未初始化数据的使用,等等。

有时,即使程序的语义定义是明确的,也可能存在问题,例如:逻辑错误、内存泄漏,等等。

0x01 静态分析(Static Analysis)

每个人都知道漏洞普遍存在且很重要,程序员无法避免犯错,我们应该如何处理这些漏洞?

开发一种能够在运行前检测漏洞的自动化技术怎么样?

  • 自动化:由程序分析,而非人工
  • 运行前:防止其在实际运行中引发严重问题

这种技术(或用于此的工具/程序)被称为静态分析(静态分析器),请记住,在编程语言中,静态表示 "在运行前决定"。

但遗憾的是,完美的静态分析器是不存在的,编写一个完美的程序分析算法被证明是不可能的(不可判定问题),参见自动机理论中的停机问题。

这里,完美是指健全性和完备性:

  • 健全性:有错误的程序总是被拒绝 / 从不遗漏错误 / 如果程序通过检查,保证没有错误
  • 完备性:没有错误的程序总是被接受 / 从不拒绝安全的程序 / 如果被拒绝,必定有错误

我们必须在健全性和完备性之间做出取舍,有时,我们甚至两者都要放弃。

尽管如此,这样的静态分析器(带有近似性)仍然是有用的。

0x02 静态类型系统(Static Type System)

静态类型系统是最原始和最流行的静态分析器形式之一,其目标是在运行前自动检测类型错误,通常作为编译器或解释器的一部分配备。

我们应该选择哪一方面:健全性还是完备性? F# 采用的是健全(但不完备)的类型系统,本专栏我们也将讨论 F- 的健全类型系统。

0x03 什么是类型?

类型是一组值,或者可以将其视为值的抽象。

bool: { 真, 假 }

int: { … , -2, -1, 0, 1, 2, … }

int -> int:接受一个整数并返回一个整数的函数集合:

let incr : int -> int = fun x -> x + 1 

'a -> 'a:接受任意类型 'a 并返回相同类型的函数集合:

let identity : 'a -> 'a = fun x -> x


📌 [ 笔者 ]   王亦优
📃 [ 更新 ]   2024.6.10
❌ [ 勘误 ]   /* 暂无 */
📜 [ 声明 ]   由于作者水平有限,本文有错误和不准确之处在所难免,本人也很想知道这些错误,恳望读者批评指正!

📜 参考资料 

Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. .

这篇关于【PL理论】(31) 类型系统:静态分析 (Static Analysis) | 静态类型系统 | 什么是类型?的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/1072530

相关文章

怎样通过分析GC日志来定位Java进程的内存问题

《怎样通过分析GC日志来定位Java进程的内存问题》:本文主要介绍怎样通过分析GC日志来定位Java进程的内存问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一、GC 日志基础配置1. 启用详细 GC 日志2. 不同收集器的日志格式二、关键指标与分析维度1.

MySQL中的表连接原理分析

《MySQL中的表连接原理分析》:本文主要介绍MySQL中的表连接原理分析,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录1、背景2、环境3、表连接原理【1】驱动表和被驱动表【2】内连接【3】外连接【4编程】嵌套循环连接【5】join buffer4、总结1、背景

解析C++11 static_assert及与Boost库的关联从入门到精通

《解析C++11static_assert及与Boost库的关联从入门到精通》static_assert是C++中强大的编译时验证工具,它能够在编译阶段拦截不符合预期的类型或值,增强代码的健壮性,通... 目录一、背景知识:传统断言方法的局限性1.1 assert宏1.2 #error指令1.3 第三方解决

python中Hash使用场景分析

《python中Hash使用场景分析》Python的hash()函数用于获取对象哈希值,常用于字典和集合,不可变类型可哈希,可变类型不可,常见算法包括除法、乘法、平方取中和随机数哈希,各有优缺点,需根... 目录python中的 Hash除法哈希算法乘法哈希算法平方取中法随机数哈希算法小结在Python中,

Java Stream的distinct去重原理分析

《JavaStream的distinct去重原理分析》Javastream中的distinct方法用于去除流中的重复元素,它返回一个包含过滤后唯一元素的新流,该方法会根据元素的hashcode和eq... 目录一、distinct 的基础用法与核心特性二、distinct 的底层实现原理1. 顺序流中的去重

linux重启命令有哪些? 7个实用的Linux系统重启命令汇总

《linux重启命令有哪些?7个实用的Linux系统重启命令汇总》Linux系统提供了多种重启命令,常用的包括shutdown-r、reboot、init6等,不同命令适用于不同场景,本文将详细... 在管理和维护 linux 服务器时,完成系统更新、故障排查或日常维护后,重启系统往往是必不可少的步骤。本文

关于MyISAM和InnoDB对比分析

《关于MyISAM和InnoDB对比分析》:本文主要介绍关于MyISAM和InnoDB对比分析,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录开篇:从交通规则看存储引擎选择理解存储引擎的基本概念技术原理对比1. 事务支持:ACID的守护者2. 锁机制:并发控制的艺

Mac系统下卸载JAVA和JDK的步骤

《Mac系统下卸载JAVA和JDK的步骤》JDK是Java语言的软件开发工具包,它提供了开发和运行Java应用程序所需的工具、库和资源,:本文主要介绍Mac系统下卸载JAVA和JDK的相关资料,需... 目录1. 卸载系统自带的 Java 版本检查当前 Java 版本通过命令卸载系统 Java2. 卸载自定

CSS中的Static、Relative、Absolute、Fixed、Sticky的应用与详细对比

《CSS中的Static、Relative、Absolute、Fixed、Sticky的应用与详细对比》CSS中的position属性用于控制元素的定位方式,不同的定位方式会影响元素在页面中的布... css 中的 position 属性用于控制元素的定位方式,不同的定位方式会影响元素在页面中的布局和层叠关

MyBatis Plus 中 update_time 字段自动填充失效的原因分析及解决方案(最新整理)

《MyBatisPlus中update_time字段自动填充失效的原因分析及解决方案(最新整理)》在使用MyBatisPlus时,通常我们会在数据库表中设置create_time和update... 目录前言一、问题现象二、原因分析三、总结:常见原因与解决方法对照表四、推荐写法前言在使用 MyBATis