形式化方法

在計算機科學中，形式化方法是用于軟件和硬件系統的規范、開發和驗證的數學上的嚴格的技術。在軟件和硬件設計中使用形式化方法的動機是希望像其他工程學科一樣，進行適當的數學分析能夠有助于提高設計的可靠性和穩健性。形式化方法采用了各種計算機科學的理論基礎，包括邏輯計算、形式語言、自動機理論、控制理論、程序語義學、類型系統和類型理論。

半正式方法是指不被認為是完全"正式"的形式主義和語言。它把完成語義的任務推遲到以后的階段，然后通過人的解釋或通過代碼或測試用例生成器等軟件進行解釋。

形式化方法可以在多個層次上使用。第0級：可以進行正式的規范，然后非正式地開發一個程序。這被稱為正規方法的精簡版。在許多情況下，這可能是xxx成本效益的選擇。1級：形式化開發和形式化驗證可以用來以更正式的方式產生一個程序。例如，可以進行屬性證明或從規范到程序的細化。這可能最適合于涉及安全或安保的高集成度系統。第二級：可以使用定理證明器來進行完全正式的機器檢查證明。盡管工具在不斷改進，成本在不斷下降，但這可能是非常昂貴的，只有在錯誤的成本非常高的情況下（例如，在操作系統或微處理器設計的關鍵部分）才是實際值得的。有關這方面的進一步信息將在下面展開。與編程語言語義學一樣，形式化方法的風格可以粗略地分類如下。指稱語義學，其中系統的意義在域的數學理論中被表達。這類方法的支持者依靠領域被充分理解的性質來賦予系統以意義；批評者指出，并不是每個系統都可以直觀或自然地被看作是一個函數。操作語義學，其中系統的意義被表達為一個(大概)更簡單的計算模型的動作序列。

這種方法的支持者指出，他們的模型的簡單性是達到表達清晰的手段；批評者則反駁說，語義學的問題只是被拖延了(誰來定義更簡單的模型的語義？)。公理語義學，其中系統的意義被表達為前提條件和后置條件，這些條件在系統執行任務之前和之后分別為真。支持者注意到與經典邏輯的聯系；批評者注意到這種語義從來沒有真正描述過系統做了什么（僅僅是之前和之后的真實情況）。輕量級的形式化方法一些從業者認為形式化方法社區過分強調了規范或設計的完全形式化。他們認為，所涉及的語言的可表達性，以及被建模的系統的復雜性，使得完全形式化成為一項困難和昂貴的任務。作為替代方案，已經提出了各種輕量級的形式化方法，它們強調部分規范和重點應用。這種輕量級的形式化方法的例子包括Alloy對象建模符號，Denney將Z符號的某些方面與用例驅動的開發綜合起來，以及CSKVDM工具。

形式化方法可以在開發過程中的不同階段應用。

形式化方法可以用來描述要開發的系統，無論需要什么級別的細節。這種形式化的描述可以用來指導進一步的開發活動；此外，它還可以用來驗證正在開發的系統的需求是否被完整和準確地指定，或者通過用一種具有精確和明確的語法和語義的形式化語言來表達系統需求。