注冊 | 登錄讀書好,好讀書,讀好書!
讀書網(wǎng)-DuShu.com
當(dāng)前位置: 首頁出版圖書教育/教材/教輔考試研究生入學(xué)考試軟件開發(fā)的形式化方法

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

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

定 價:¥26.00

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

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

內(nèi)容簡介

  《軟件開發(fā)的形式化方法》對軟件開發(fā)中的形式化方法進(jìn)行了介紹和討論,內(nèi)容涵蓋了SE2004中關(guān)于"軟件的形式化方法"的知識點,主要包括:有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)、通信順序進(jìn)程、通信系統(tǒng)演算、一階邏輯、程序正確性證明、時態(tài)邏輯、模型檢驗、Z、VDM、Larch等。形式化方法是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上、具有精確數(shù)學(xué)語義的開發(fā)方法。從廣義角度,形式化方法是軟件開發(fā)過程中分析、設(shè)計及實現(xiàn)的系統(tǒng)工程方法。狹義地,形式化方法是軟件規(guī)格和驗證的方法?!盾浖_發(fā)的形式化方法》可作為計算機(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計時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計數(shù)器方法(125)
5.3.5最弱前置謂詞方法(127)..
習(xí)題(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)
習(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ī)網(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)...

本目錄推薦

掃描二維碼
Copyright ? 讀書網(wǎng) ranfinancial.com 2005-2020, All Rights Reserved.
鄂ICP備15019699號 鄂公網(wǎng)安備 42010302001612號