軟件開發(fā)的形式化方法

第1章 軟件及其開發(fā)概述...
1.1軟件開發(fā)的歷史(1)
1.2軟件危機(2)
1.3軟件工程(5)
1.4形式化方法(15)
習題.(22)
第2章 有限狀態(tài)機及其擴展
2.1有限狀態(tài)機(23)
2.1.1基本概念(23)
2.1.2有限狀態(tài)機的復合(30)
2.1.3生產(chǎn)者-消費者系統(tǒng)(32)
2.2Statecharts(34)
2.2.1Statecharts中的狀態(tài)(34)
2.2.2Statecharts中的遷移(36)
2.2.3電梯控制系統(tǒng)(40)
習題(45)
第3章 Petri網(wǎng)
3.1位置/遷移Petri網(wǎng)(47)
3.1.1基本定義(47)
3.1.2特殊Petri網(wǎng)(51)
3.1.3Petri網(wǎng)的性質(zhì)(53)
3.1.4Petri網(wǎng)的分析(56)
3.1.5Petri網(wǎng)規(guī)格的例(62)
3.2高級Petri網(wǎng)(66)
3.2.1謂詞/遷移Petri網(wǎng)(66)
3.2.2有色Petri網(wǎng)(69)
3.2.3計時Petri網(wǎng)(71)
習題.(72)
第4章 進程代數(shù)
4.1通信順序進程(74)
4.1.1進程及其表示(74)
4.1.2事件跡及其操作(77)
4.1.3進程的復合操作(81)
4.1.4進程的模型(85)
4.1.5進程之間的通信(89)
4.1.6CSP規(guī)格的例(93)
4.2通信系統(tǒng)演算(95)
4.2.1CCS的基本概念(95)
4.2.2AB協(xié)議的規(guī)格(96)
習題.(98)
第5章 一階邏輯
5.1命題邏輯(99)
5.1.1命題與聯(lián)結詞(99)
5.1.2命題公式(101)
5.1.3命題邏輯演算(102)
5.2謂詞邏輯(105)
5.2.1謂詞公式(105)
5.2.2謂詞邏輯演算(107)
5.2.3謂詞邏輯的應用(108)
5.3程序正確性證明(112)
5.3.1歸納斷言方法(112)
5.3.2公理化方法(116)
5.3.3程序集方法(121)
5.3.4計數(shù)器方法(125)
5.3.5最弱前置謂詞方法(127)..
習題(137)
第6章 時態(tài)邏輯
6.1模態(tài)邏輯(140)
6.2線性時態(tài)邏輯(143)
6.2.1命題線性時態(tài)邏輯(143)
6.2.2一階線性時態(tài)邏輯(146)
6.2計算樹邏輯(150)
6.3模型檢驗(154)
習題(157)
第7章 Z
7.1概述(159)
7.2表示抽象(166)
7.2.1集合.關系及函數(shù)(166)
7.2.2序列和包(172)
7.2.3自由類型(174)
7.2.4模式(176)
7.3操作抽象(178)
7.3.1模式運算及合成(178)
7.3.2通用式函數(shù)(188)
7.4Z規(guī)格的例(189)
7.4.1圖書數(shù)據(jù)庫管理(189)
7.4.2自動售貨機(199)
習題(199)
第8章 VDM
8.1概述.(206)
8.2表示抽象(207)
8.2.1基本運算和基本類型(207)
8.2.2集合與序列(208)
8.2.3映射與函數(shù)(211)
8.2.4復合類型(214)
8.2.7狀態(tài)和不變量(216)
8.3操作抽象(218)
8.3.1操作的表示(218)
8.3.2聲明(220)
8.4VDM規(guī)格的例(224)
8.4.1家庭供暖系統(tǒng)(224)
8.4.2計算機網(wǎng)絡問題.(230)
習題(233)
第9章 Larch
9.1概述(235)
9.2Larch共享語言(236)
9.3Larch/C++接口語言(253)
9.4Larch規(guī)格的例(256)
習題(261)
參考文獻(263)...