静态程序分析

静态程序分析（英语：Static program analysis）是指在不运行程序的条件下，进行程序分析的方法。和要在程序运行时才能进行的动态程序分析（英语：dynamic program analysis）是不同的^[1]。大部分的静态程序分析的对象是针对特定版本的源代码，也有些静态程序分析的对象是目标代码。静态程序分析一词多半是指配合静态程序分析工具进行的分析，人工进行的分析一般称为程序理解或代码审查。

静态程序分析的复杂程度依所使用的工具而异，简单的只考虑个别语句及声明的行为，复杂的可以分析程序的完整源代码。不同静态程序分析技术对分析得到的信息的用途也有所不同，简单的可以是高亮标识可能存在的代码错误（如lint），复杂的可以是形式化方法，也就是用数学的方式证明程序的某些行为符合其设计规约。

软件度量和反向工程可以视为一种静态程序分析的方式。在实务上，在定义所谓的软件质量指针（software quality objectives）后，软件度量的推导及程序分析常一起进行，在开发嵌入式系统时常会用这种方式进行。

静态程序分析的商业用途可以用来验证安全关键计算机系统中的软件，并指出可能有计算机安全隐患的代码，这类的应用越来越多。^[2]例如以下的产业已确定用静态程序分析作为提升复杂软件质量的方法：

1. 医疗软件：美国的美国食品药品监督管理局确定在医疗设备上使用静态程序分析^[3]。
2. 核能软件：英国的健康与安全委员会（英语：Health and Safety Executive）建议针对堆保护系统（英语：Reactor Protective System）的软件进行静态程序分析中^[4]。

在信息安全的领域中，静态程序分析会称为静态应用程序安全检测，简称SAST。

形式化方法

主条目：形式化方法

形式化方法是一种利用纯粹数学的方式分析软件的方法，应用到的数学技巧包括指称语义、公理语义、操作语义学及抽象释义等计算机科学中的方法。

针对任何图灵完全的编程语言，不可能存在一算法可以找出任意程序在运行期间的所有错误，也没有数学方法可以得到一程序是否会有运行期间的错误的结果。上述的结论是由库尔特·哥德尔、阿隆佐·邱奇及阿兰·图灵在1930年代研究停机问题所得的结果。不过如同许多不可判定问题一様，在实务仍会设法找到有用的近似解。

以下是一些形式化静态分析的实现方式：

• 模型检查（英语：Model checking）针对有有限状态或是可以用抽象化简化为有限状态的系统。
• 数据流分析可以收集有关程序在不同点计算所得的可能数值。
• 抽象释义可以被看作对计算机程序的部分执行，获取关于它的语义信息（比如，控制结构、信息流）而不进行所有计算。Frama-c（英语：Frama-c）及Polyspace等工具主要是以抽象释义为基础。
• 在代码中加入断言，此方法最早是由霍尔逻辑提出。有些编程语言有对应的支持工具，例如SPARK（Ada编程语言的子集）、Java 建模语言（英语：Java Modeling Language）（其中使用ESC/Java（英语：ESC/Java）及ESC/Java2）及针对C语言的Frama-c WP 插件（最弱初始条件（英语：Predicate transformer semantics#Weakest preconditions）），此插件需配合延伸至ACSL（英语：ANSI/ISO C Specification Language）（ANSI/ISO C Specification Language）的C语言。

相关条目

• 程序分析
• 动态程序分析（英语：Dynamic program analysis）
• 形态分析（英语：Shape analysis (program analysis)）
• 形式语义学
• 形式验证
• 软件测试
• 文件产生器（英语：Documentation generator）
• 静态程序分析工具栏表（英语：List of tools for static code analysis）
• 静态应用程序安全测试