雖然 Ada 提供了許多在運行時充當安全防護的功能，但在檢測到違規時會引發異常，但其中一些功能可能過于復雜，無法保證在程序運行之前安全執行。例如指針就是這種情況，指針可用于在內存中創建任意復雜的共享數據結構。SPARK 是 Ada 的一個子集，它禁止這些功能，最明顯的是指針，以便能夠在編譯時提供強有力的保證。SPARK的下一個修訂版SPARK 2014的預覽版以及相關的驗證工具已經可用。

盡管SPARK的演進一直伴隨著Ada的演進，每個新版本的Ada（SPARK 83，SPARK 95，SPARK 2005）都有一個新版本的SPARK，但新版本SPARK 2014在許多方面都有很大的不同。SPARK 2014 是 2010年啟動的一個項目的結果，該項目旨在使使用形式驗證而不是測試關鍵軟件具有成本效益。就在幾個月前，空中客車公司提出了采用正式方法的五個“必備”標準：健全性，代碼的適用性，“普通”工程師在“普通”計算機上的可用性，對經典方法的改進，可認證性。在這三年中，我們非常牢記這五個標準，以下是SPARK 2014和相關驗證工具GNATprove的結果。

穩?。?/p>

這是語言和工具的基石。它不僅限于說：“我們使用霍爾邏輯”。我們想要實現的是“最大”的健全性：當你適當地使用它們時，不僅工具不能陳述錯誤的屬性，而且通過濫用工具（例如通過陳述錯誤的公理）來獲得對軟件的錯誤信心也不容易。為了確保最大的合理性，采取了許多決定，例如禁止用戶陳述公理。

對代碼的適用性：

SPARK 2014 是 Ada 的最大可能子集，它仍然可以進行形式驗證。特別是，它包括泛型、標記類型、判別器、動態類型、早期回報以及 SPARK 2005 中排除的許多其他功能。對于代碼中無法正式分析的部分，我們已經可以將形式驗證與測試結合起來。因此，它不是一種全有或全無的技術，而是您可以在任何Ada項目中真正引入的技術。

普通工程師的可用性：

這是這些年來讓我們最忙的問題。首先，我們已經實現了自動化水平，大多數證明都是自動通過的，特別是沒有運行時錯誤的證明。其次，我們將工具緊密集成到開發人員工作流（例如，通過使用項目文件和自動計算的依賴項）和開發環境（例如，在特定子程序或代碼行上運行GNATprove 的能力，以及顯示有問題的程序路徑）。

改進測試：

形式驗證是詳盡無遺的，這一事實使其成為關鍵軟件所要求的昂貴單元測試活動的理想替代品。這方面的主要挑戰是促進逐步采用正式核查。由于形式驗證所需的子程序合同對于測試已經很有用，并且由于GNATproly可以單獨應用于任何Ada程序中的各個SPARK子程序，因此切換到形式驗證可以在幾天內完成。

可認證性：

當我們開始這個項目時，航空電子標準DO-178的正式方法補充尚未最終確定。從那時起，它與新版本的標準DO-178C一起發布，因此今天，GNATprove 可以用于代替在最高級別A或B開發的平面中測試關鍵嵌入式程序。我們在IEEE軟件上發表了一篇關于如何處理在這種情況下覆蓋的微妙問題的論文。當然，已經認可形式化方法的其他領域的項目（例如鐵路）也可以使用GNATprove。

該項目開發的工業案例研究的結果是公開的，供其他人了解新技術擅長什么以及當前發展階段。當用戶從以前的SPARK技術切換到新的SPARK 2014技術時，最常見的評論可能是執行規范的能力提供了令人難以置信的可用性改進。這種動態技術和靜態技術的結合對于軟件驗證的未來無疑是有希望的。

審核編輯：郭婷