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

回顧高級靜態(tài)分析

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

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

圖 1：高級流量分析示例

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

那么靜態(tài)分析器對“ pragma Assert（Table’Length 》= 1） ”做了什么？這就是分析器不同的地方，這取決于他們是采用自下而上還是自上而下的策略來發(fā)現(xiàn)跨越過程邊界的錯誤，以及他們?nèi)绾螌⑦@一點與基于合同的編程概念相結合。

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

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

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

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

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

靜態(tài)分析：檢查和推斷合約

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

圖 2：自上而下與自下而上的過程間靜態(tài)分析

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

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

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

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

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

未來：一邊編程一邊證明

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

審核編輯：郭婷