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