什麼是形式化方法

軟體形式化方法是指建立在嚴格數學基礎上的軟體開發方法。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以應用嚴格的數學符號來說明、開發和驗證基於計算機的系統。

形式化方法的本質是基於數學的方法來描述目標軟體系統屬性的一種技術。不同的形式化方法的數學基礎是不同的，有的以集合論和一階謂詞演算為基礎（如z和vdm），有的則以時態邏輯為基礎。形式化方法需要形式化規約說明語言的支援。

這樣的形式化方法提供了乙個框架，可以在框架中以系統的而不是特別的方式刻劃、開發和驗證系統。如果乙個方法有良好的數學基礎，那麼它就是形式化的，典型地以形式化規約語言給出。這個基礎提供一系列精確定義的概念，如：一致性和完整性，以及定義規範的實現和正確性。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以應用嚴格的數學符號來說明、開發和驗證基於計算機的系統。這種方法的乙個變型是淨室軟體工程（cleanroom software engineering），這一軟體工程方法目前已應用於一些軟體開發機構。