靜態程式分析

靜態程式分析（英語：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）
• 靜態應用程式安全測試