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

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