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

定　價(jià)：￥26.00

作　者：	古天龍著
出版社：	高等教育出版社
叢編項(xiàng)：	高等學(xué)校研究生系列教材
標(biāo)　簽：	軟件方法

購買這本書可以去

ISBN：	9787040160796	出版時(shí)間：	2005-01-01	包裝：	簡裝本
開本：	24cm	頁數(shù)：	265	字?jǐn)?shù)：

內(nèi)容簡介

　　《軟件開發(fā)的形式化方法》對軟件開發(fā)中的形式化方法進(jìn)行了介紹和討論，內(nèi)容涵蓋了SE2004中關(guān)于"軟件的形式化方法"的知識點(diǎn)，主要包括：有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)、通信順序進(jìn)程、通信系統(tǒng)演算、一階邏輯、程序正確性證明、時(shí)態(tài)邏輯、模型檢驗(yàn)、Z、VDM、Larch等。形式化方法是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上、具有精確數(shù)學(xué)語義的開發(fā)方法。從廣義角度，形式化方法是軟件開發(fā)過程中分析、設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法。狹義地，形式化方法是軟件規(guī)格和驗(yàn)證的方法?！盾浖_發(fā)的形式化方法》可作為計(jì)算機(jī)、軟件工程等專業(yè)高年級本科聲或研究生的教學(xué)用書，也可供相關(guān)領(lǐng)域的研究人員和工程技術(shù)人員參考。

作者簡介

暫缺《軟件開發(fā)的形式化方法》作者簡介

圖書目錄

第1章軟件及其開發(fā)概述...
1.1軟件開發(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高級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ì)算樹邏輯(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ù)庫管理(189)
7.4.2自動售貨機(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ò)問題.(230)
習(xí)題(233)
第9章 Larch
9.1概述(235)
9.2Larch共享語言(236)
9.3Larch/C++接口語言(253)
9.4Larch規(guī)格的例(256)
習(xí)題(261)
參考文獻(xiàn)(263)...