程序静态分析的形式化方法

发布网友发布时间：2022-04-21 15:04

共1个回答

热心网友时间：2023-09-30 06:41

程序分析中的形式化方法一般指利用纯粹严格的数学方法对软件、硬件进行分析的理论及技术。这些数学方法包括符号语义、公理语义、操作语义和抽象解释。
1952年提出的Rice定理指出，任何关于程序分析的问题都是不可判定的。因此，不存在任何一种机械化的方法能够证明程序的完全正确性。然而，针对大多数的不可判定问题，仍然可以试图找到它们的一些近似解。
形式化静态分析中用到的实现技术有：
模型检查假设系统是有限状态的、或者可以通过抽象归结为有限状态。
抽象解释将每条语句的影响模型化为一个抽象机器的状态。相比实际系统，抽象机器更简单更容易分析，但其代价是丧失了分析的完备性（并不是原始系统中的每种性质在抽象机器中都是保留的）。抽象解释当且仅当抽象机器中的每一个性质都能与原始系统中的性质正确映射时，才被称作可靠（sound）的。
断言在霍恩逻辑中首次被提出。目前存在一些针对特定程序设计语言的工具，例如ESC/JAVA和ESC/JAVA2中分别使用的SPARK语言和JML语言。