軟件形式規(guī)格說明語言—Z

定　價：￥34.50

作　者：	繆淮扣等編著
出版社：	清華大學(xué)出版社
叢編項：	軟件工程專業(yè)核心課程系列教材
標　簽：	計算機

購買這本書可以去

ISBN：	9787302292777	出版時間：	2012-11-01	包裝：	平裝
開本：	16開	頁數(shù)：	299	字數(shù)：

內(nèi)容簡介

　　形式方法是一種基于數(shù)學(xué)的軟件開發(fā)方法。形式規(guī)格說明是形式方法最基本的部分，它精確描述用戶需求和計算機軟件系統(tǒng)的功能，并用于軟件驗證和精化。z是目前頗受歡迎且使用較廣泛的一種形式規(guī)格說明語言。本書旨在討論軟件工程中形式方法的概念、方法和表示法，并詳細介紹z的類型系統(tǒng)、數(shù)學(xué)語言和公理定義、通用式定義、模式等結(jié)構(gòu)，還討論了z規(guī)格說明的推理和求精方法。本書還介紹了面向?qū)ο蟮囊?guī)格說明語言object—z和其他形式方法表示和工具。全書結(jié)構(gòu)合理、內(nèi)容豐富、實例詳盡多樣。各章配有習(xí)題。《軟件形式規(guī)格說明語言—z》可作為計算機、軟件工程、信息安全和信息管理等專業(yè)本科生和研究生的教材，也可作為大專院校有關(guān)專業(yè)的教師參考書，還可作為從事軟件工程、軟件開發(fā)和軟件應(yīng)用的研究人員和技術(shù)人員的參考資料。

作者簡介

暫缺《軟件形式規(guī)格說明語言—Z》作者簡介

圖書目錄

第1章　緒論
1．1軟件生命周期
1．2存在的問題
1．3形式方法
1．4形式規(guī)格說明語言z
小結(jié)
習(xí)題第2章　一階邏輯與集合論
2．1命題邏輯
2．2謂詞邏輯
2．3一階邏輯中的證明
2．4集合論
小結(jié)
習(xí)題第3章　z的類型與構(gòu)造單元
3．1z的類型系統(tǒng)
3．2擴充表示法
3．3z規(guī)格說明的構(gòu)造單元
小結(jié)
習(xí)題第4章　關(guān)系和函數(shù)
4．1關(guān)系
4．2關(guān)系的運算
4．3函數(shù)
小結(jié)
習(xí)題第5章　模式和規(guī)格說明
5．1模式的描述功能
5．2模式的修飾和包含
5．3模式運算
5．4模式類型和通用模式
5．5規(guī)格說明文檔的結(jié)構(gòu)
小結(jié)
習(xí)題第6章　序列和包
6．1序列
6．2包
小結(jié)
習(xí)題第7章　規(guī)格說明的實例
7．1簡介
7．2存儲分配管理
7．3圖書館數(shù)據(jù)庫管理實例
7．4自由類型的應(yīng)用——命題邏輯證明器的規(guī)格說明
小結(jié)
習(xí)題第8章　z規(guī)格說明的形式推理
8．1問題的提出和有關(guān)的概念
8．2關(guān)于嚴密證明
8．3一個定律庫
8．4關(guān)于規(guī)格說明的推理
小結(jié)
習(xí)題第9章　z規(guī)格說明的若干推理實例
9．1兩個初始化定理的證明
9．2兩個前置條件的簡化
9．3規(guī)格說明中一般定理的證明
小結(jié)
習(xí)題第10章　從規(guī)格說明到程序
10．1程序范疇與軟件精化
10．2z規(guī)格說明的精化原則
10．3精化演算
10．4z的精化演算方法
10．5實例研究
小結(jié)
習(xí)題第11章　object-z規(guī)格說明語言
11．1為何需要面向?qū)ο蟮膠
11．2object—z語言簡介
11．3操作
11．4分布運算符
11．5遞歸定義
11．6繼承
11．7對象包含
11．8多態(tài)性
11．9類合并
11．10self常量
11．11object—z語言的工具支持
11．12object—z實例研究：銀行系統(tǒng)
小結(jié)
習(xí)題第12章　形式方法及其工具
12．1z規(guī)格說明語言支撐工具
12．2其他形式方法工具
12．3其他形式方法及規(guī)格說明語言
小結(jié)
習(xí)題附錄az語法
附錄bz語言術(shù)語
附錄cobject-z語法
c．1表示法
c．2縮寫
c．3產(chǎn)生式
附錄d部分習(xí)題解答
參考文獻