《 軟體開發的形式化方法》是 2005年 高等教育出版社出版的圖書。
基本介紹
- 書名：軟體開發的形式化方法
- 又名：Formal Methods of Software Development
- 原版名稱： 高等學校研究生系列教材
- ISBN：9787040160796
- 頁數：265頁
- 出版社：高等教育出版社
- 出版時間：第1版 (2005年1月1日)
- 裝幀：平裝
- 開本：16
- 正文語種：簡體中文
內容簡介,目錄,
內容簡介
《軟體開發的形式化方法》對軟體開發中的形式化方法進行了介紹和討論，內容涵蓋了SE2004中關於"軟體的形式化方法"的知識點，主要包括：有限狀態機、Statecharts、Petri網、通信順序進程、通信系統演算、一階邏輯、程式正確性證明、時態邏輯、模型檢驗、Z、VDM、Larch等。形式化方法是建立在嚴格數學基礎上、具有精確數學語義的開發方法。從廣義角度，形式化方法是軟體開發過程中分析、設計及實現的系統工程方法。狹義地，形式化方法是軟體規格和驗證的方法。
《軟體開發的形式化方法》可作為計算機、軟體工程等專業高年級本科生或研究生的教學用書，也可供相關領域的研究人員和工程技術人員參考。
目錄
第1章 軟體及其開發概述
1.1 軟體開發的歷史
1.2 軟體危機
1.3 軟體工程
1.4 形式化方法
習題
第2章 有限狀態機及其擴展
2.1 有限狀態機
2.2 Statecharts
習題
第3章 Petri網
3.1 位置/遷移Petri網
3.2 高級Petri網
習題
第4章 進程代數
4.1 通信順序進程
4.2 通信系統演算
習題
第5章 一階邏輯
5.1 命題邏輯
5.2 謂詞邏輯
5.3 程式正確性證明
習題
第6章 時態邏輯
6.1 模態邏輯
6.2 線性時態邏輯
6.3 計算樹邏輯
6.4 模型檢驗
習題
第7章 Z
7.1 概述
7.2 表示抽象
7.3 操作抽象
7.4 Z規格的例
習題
第8章 VDM
8.1 概述
8.2 表示抽象
8.3 操作抽象
8.4 VDM規格的例
習題
第9章 Larch
參考文獻
