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

定　價：￥34.50

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

購買這本書可以去

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

內容簡介

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

作者簡介

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

圖書目錄

第1章　緒論
1．1軟件生命周期
1．2存在的問題
1．3形式方法
1．4形式規(guī)格說明語言z
小結
習題第2章　一階邏輯與集合論
2．1命題邏輯
2．2謂詞邏輯
2．3一階邏輯中的證明
2．4集合論
小結
習題第3章　z的類型與構造單元
3．1z的類型系統(tǒng)
3．2擴充表示法
3．3z規(guī)格說明的構造單元
小結
習題第4章　關系和函數(shù)
4．1關系
4．2關系的運算
4．3函數(shù)
小結
習題第5章　模式和規(guī)格說明
5．1模式的描述功能
5．2模式的修飾和包含
5．3模式運算
5．4模式類型和通用模式
5．5規(guī)格說明文檔的結構
小結
習題第6章　序列和包
6．1序列
6．2包
小結
習題第7章　規(guī)格說明的實例
7．1簡介
7．2存儲分配管理
7．3圖書館數(shù)據(jù)庫管理實例
7．4自由類型的應用——命題邏輯證明器的規(guī)格說明
小結
習題第8章　z規(guī)格說明的形式推理
8．1問題的提出和有關的概念
8．2關于嚴密證明
8．3一個定律庫
8．4關于規(guī)格說明的推理
小結
習題第9章　z規(guī)格說明的若干推理實例
9．1兩個初始化定理的證明
9．2兩個前置條件的簡化
9．3規(guī)格說明中一般定理的證明
小結
習題第10章　從規(guī)格說明到程序
10．1程序范疇與軟件精化
10．2z規(guī)格說明的精化原則
10．3精化演算
10．4z的精化演算方法
10．5實例研究
小結
習題第11章　object-z規(guī)格說明語言
11．1為何需要面向對象的z
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)
小結
習題第12章　形式方法及其工具
12．1z規(guī)格說明語言支撐工具
12．2其他形式方法工具
12．3其他形式方法及規(guī)格說明語言
小結
習題附錄az語法
附錄bz語言術語
附錄cobject-z語法
c．1表示法
c．2縮寫
c．3產生式
附錄d部分習題解答
參考文獻