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

內(nèi)容概要

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

書籍目錄

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

編輯推薦

　　《普通高等教育“十一五”國家級規(guī)劃教材·軟件工程專業(yè)核心課程系列教材：軟件形式規(guī)格說明語言Z》具有以下特點：　　1 教育部高等學校軟件工程專業(yè)教學指導分委員會推薦教材?！　? 根據(jù)教育部“軟件工程課程體系研究”項目成果《中國軟件工程學科教程》及專業(yè)規(guī)范組織編寫?！　? 與最新ACM和IEEE CCSE同步?！　? 匯集示范性軟件工程專業(yè)教學成果。

圖書封面

評論、評分、閱讀與下載

---

    軟件形式規(guī)格說明語言 PDF格式下載

---