高級靜態分析工具正在成為許多專業程序員工具包的標準部分。同時，越來越重視基于契約的編程，其中明確的前置條件、后置條件和其他契約被添加到源代碼中，以幫助增強軟件安全性和安全性，因為嵌入式系統變得越來越復雜和相互依賴。當這兩種趨勢相遇時，就會出現一些有趣的機會。特別是，某些高級靜態分析工具開始直接識別合約，有些甚至通過從現有代碼中推斷出合約來幫助程序員創建合約。對高級靜態分析的回顧有助于為討論基于契約的編程奠定基礎。

回顧高級靜態分析

較新的靜態分析工具不再簡單地執行編碼指南，而是深入研究程序結構的語義，有效地模擬運行時可能發生的情況，以檢測邏輯不一致或安全漏洞。這些工具通常基于編譯器技術，使用高級數據流分析來確定程序可能出錯的地方，方法是跟蹤變量在運行時可能具有的值，然后檢查這些值是否都被程序正確處理以及是否可能被污染數據在被信任之前經過適當的審查。在代碼實際上安全可靠但工具的價值跟蹤或污點跟蹤不夠精確的地方，此類工具仍然存在產生誤報（實際上是誤報）的挑戰。盡管如此，

圖 1 說明了靜態分析器如何使用數據流分析來跟蹤變量（例如Count ）的可能值，并確定這些值中的任何一個是否可能在以后的某個時間點導致問題。正在顯示表格的值，然后是平均值。這里的經典“錯誤”是忽略表為空的可能性，從而導致可能的被零除錯誤。

圖 1：高級流量分析示例

在這個例子中，為了避免被零除，程序員已經包含了一個表有至少一個元素的斷言（即“ Table‘Length 》= 1） ”。但是，需要進行一些數據流分析來驗證Float（Count）在除法“ Sum / Float（Count） ”中是否非零。這需要靜態分析器將Float（Count）的值鏈接到Count的值，將Count的最終值鏈接到由Table’Range確定的循環迭代次數，并將該數字鏈接到Table‘Length（X’Range 表示“X‘First 。. X’Last”，而 X‘Length 表示“（如果 X’First 》 X‘Last then 0 else X’Last – X‘First + 1）”）。對程序員來說容易的事情可以為靜態分析器做更多的工作。

那么靜態分析器對“ pragma Assert（Table’Length 》= 1） ”做了什么？這就是分析器不同的地方，這取決于他們是采用自下而上還是自上而下的策略來發現跨越過程邊界的錯誤，以及他們如何將這一點與基于合同的編程概念相結合。

基于合同的編程適合的地方

基于契約的編程（除其他外）是使用前置條件和后置條件來表達對組成程序的功能和過程（即子程序）的輸入和輸出（分別）的期望。

在圖 1 的示例中，程序員的意圖顯然是“ Table‘Length 》= 1 ”作為該過程的先決條件。不幸的是，這個Assert隱藏在過程的代碼中，而不是很容易被調用者看到。在 Eiffel［1］ 或 Ada 2012［2］ 等語言中，前置條件和后置條件是語法的一部分，或者在 C# 或 Java 等語言中使用 Spec#［3］ 或 Java 建模語言 （JML）［4］ 等擴展，程序員對Display_Table過程的表輸入的意圖可以使用顯式前置條件來表達。例如，在 Ada 2012 中，此過程的規范可以寫成：

過程 Display_Table（Table： Float_Array） 與 Pre =》 Table’Length 》= 1;

這為Display_Table過程指定了方面Pre（“前提條件”的縮寫），因此它對調用者可見并有效地成為Display_Table上的合同，這表明只要Table的長度至少為 1，Display_Table就可以執行它的正確工作。

靜態分析：檢查和推斷合約

現在回到圖 1 中的 pragma Assert。如果沒有明確的合同要求調用者確保Table‘Length 》= 1，靜態分析器可能會正確地抱怨，因為沒有什么可以阻止調用者傳入零長度表。但是，許多靜態分析器使用不同的策略。他們不是立即抱怨Assert，而是依靠更多的全局檢查來確定是否存在真正的問題，并且僅在有一個通過零長度表的調用時才抱怨。如前所述，這些全局的、過程間的檢查可以主要是自下而上的，也可以主要是自上而下的，如圖 2 所示。

圖 2：自上而下與自下而上的過程間靜態分析

在自上而下的策略中，分析器從程序的入口點向下走，在每次調用時用實際參數代替形式，直到識別出每個子程序的每次調用，累積一組可能的實際值傳入對于每個正式的。然后使用該值集來確定是否可能通過某些特定的調用鏈違反Assert 。

在自下而上的策略中，分析從程序的葉子（不進行調用的子程序）開始，分析每個子程序以確定它對其輸入施加的要求。在此示例中，Assert（Table’Length 》= 1）被有效地轉換為過程的隱式前提條件。靜態分析器本質上是在為每個子程序推斷未聲明的合約，然后將其傳播到每個調用點，其中前提條件成為調用點實際參數的隱式斷言。這個過程一直持續到更高級別的子程序，直到最終整個程序都被分析完。

隨著程序變得越來越大，自下而上的方法可以比自上而下的方法更好地擴展，但它取決于推斷潛在的復雜合同，包括條件先決條件，其中一個輸入的先決條件可能取決于另一個輸入的值。例如，對于以“ if X 》 0 then Assert（Y 》 0） ”開頭的過程，推斷的前提條件應該是“ X 》 0 ==》 Y 》 0 ”。兩種通過自下而上分析推斷合約的高級靜態分析工具是 AdaCore 的 CodePeer 工具，它分析 Ada 源代碼，以及 Microsoft Research 的 Clousot 工具，它分析 .NET 程序。

隨著明確的前置條件和后置條件開始出現在程序中，使用像 Ada 2012 這樣的語言，這些合同和高級靜態分析工具的功能之間出現了新的協同作用。顯式契約可以簡化程序間分析，因為程序員已經完成了艱苦的工作。該工具可以簡單地檢查顯式前提條件，而不必在調用中傳播。在子程序中，該工具可以使用前置條件作為可能輸入值的精確描述，而無需猜測程序員的意圖。

顯式契約還可以幫助其他希望使用子程序的程序員，因為它們充當機器可檢查的注釋和直接嵌入代碼中的低級需求。但它們只有在程序員編寫它們時才有幫助。由于一些高級靜態分析工具可以從源代碼中推斷出合約，它們可以提供自動將它們插入源代碼。Clousot之類的工具允許程序員“祝福”推斷的合約，使其成為源代碼的永久部分。

未來：一邊編程一邊證明

靜態分析和基于合同的編程之間的協同作用可能允許更快地采用這兩種技術。隨著這兩者的集成，一種新的編程方法可能會出現，程序員的助手會在創建源代碼時幫助推斷和檢查合同。隨著程序的編寫，安全性得到了證明，就像文本編輯器中的拼寫檢查器可以確保不會出現拼寫錯誤的單詞一樣。隨著這些技術的成熟，我們可以希望不安全、不安全的程序將不再是常態，而是從一開始就內置安全性和安全性，并附帶代碼的機器可檢查、人類可讀的合約。書面。CodePeer和 Clousot等工具展示了一些可能性。

審核編輯：郭婷