《軟件開發的形式化方法》對軟件開發中的形式化方法進行了介紹和討論，內容涵蓋了SE2004中關于"軟件的形式化方法"的知識點，主要包括：有限狀態機、Statecharts、Petri網、通信順序進程、通信系統演算、一階邏輯、程序正確性證明、時態邏輯、模型檢驗、Z、VDM、Larch等。形式化方法是建立在嚴格數學基礎上、具有精確數學語義的開發方法。從廣義角度，形式化方法是軟件開發過程中分析、設計及實現的系統工程方法。狹義地，形式化方法是軟件規格和驗證的方法。