軟件工程形式化方法與語言

內(nèi)容概要

本書選取并介紹了三種代表性的形式化方法，它們分別是以集合論和一階謂詞演算為基礎(chǔ)的Z語言，以時(shí)態(tài)邏輯為基礎(chǔ)的XYZ，還有以直覺數(shù)學(xué)學(xué)派為基礎(chǔ)的類型理論。     本書既可以作為計(jì)算機(jī)專業(yè)的研究生的形式化課程教材，又可以用作專業(yè)人員的參考書。雖然真正從事形式化方面的工作的人員不多，但是有必要通過對(duì)該課程的學(xué)習(xí)，使學(xué)生在理論、技術(shù)和方法上都得到了系統(tǒng)而有效的訓(xùn)練，有利于提高軟件人員的素質(zhì)和能力。

書籍目錄

第1章 引論  1.1 軟件工程  1.2 軟件生存期  1.3 早期工作的重要性  1.4 規(guī)格說明及其形式化  1.5 一些重要的形式化規(guī)格說明語言  1.6 關(guān)于本書使用的Z語言第2章 命題邏輯  2.1 命題  2.2 合取  2.3 析取  2.4 蘊(yùn)含  2.5 等價(jià)  2.6 否定  2.7 永真式與矛盾式第3章 謂詞邏輯  3.1 謂詞演算  3.2 量詞與作用域  3.3 代換  3.4 全稱量詞的引入與消去  3.5 存在量詞的引入與消去第4章 相等與確定性的描述  4.1 相等性  4.2 一點(diǎn)規(guī)則  4.3 數(shù)量概念的表達(dá)與唯一量詞  4.4 對(duì)象的確定性描述第5章 集合  5.1 集合及其定義方法    5.1.1 集合的枚舉定義法    5.1.2 集合理解定義一利用謂詞定義集合  5.2 冪集  5.3 笛卡兒積  5.4 并集、交集和差集  5.5 類型第6章 對(duì)象的定義  6.1 聲明  6.2 省略法定義  6.3 公理定義  6.4 類屬定義第7章 關(guān)系  7.1 聲明  7.2 定義域和值域  7.3 關(guān)系上的操作    7.3.1 限制與縮減    7.3.2 關(guān)系求逆    7.3.3 關(guān)系的復(fù)合    7.3.4 關(guān)系的閉包    7.3.5 關(guān)系的映象(image)第8章 函數(shù)  8.1 偏函數(shù)和全函數(shù)  8.2 函數(shù)的λ表示法  8.3 內(nèi)射、滿射與雙射  8.4 有限函數(shù)  8.5 函數(shù)性質(zhì)小結(jié)  8.6 函數(shù)上的操作第9章 序列  9.1 序列的有關(guān)概念  9.2 序列的形式化定義  9.3 序列上的操作  9.4 序列上的函數(shù)  9.5 結(jié)構(gòu)歸納法  9.6 袋第10章 遞歸定義的類型  10.1 從自然數(shù)的定義談起  10.2 遞歸定義的類型  10.3 原始遞歸第11章 構(gòu)型(schema)與規(guī)格說明的結(jié)構(gòu)化  11.1 構(gòu)型的表示記號(hào)  11.2 一個(gè)應(yīng)用例子的非形式描述  11.3 描述抽象狀態(tài)的構(gòu)型  11.4 描述操作的構(gòu)型  11.5 作為聲明使用的構(gòu)型  11.6 作為謂詞使用的構(gòu)型  11.7 重命名  11.8 類屬構(gòu)型  11.9 構(gòu)型演算    11.9.1 構(gòu)型的包含    11.9.2 構(gòu)型的修飾    11.9.3 構(gòu)型的析取運(yùn)算    11.9.4 構(gòu)型的合取運(yùn)算    11.9.5 構(gòu)型的否定運(yùn)算    11.9.6 構(gòu)型的隱藏運(yùn)算    11.9.7 構(gòu)型的復(fù)合運(yùn)算    11.9.8 構(gòu)型的前置條件  11.10 規(guī)格說明的提升方法    11.10.1 幾個(gè)操作分解的簡單例子第12章 一個(gè)規(guī)格說明的實(shí)例——文件系統(tǒng)  12.1 非形式的描述——程序設(shè)計(jì)接口  12.2 文件上的操作的形式描述  12.3 文件系統(tǒng)的形式化規(guī)格說明  12.4 形式化分析與推理第13章 數(shù)據(jù)求精理論  13.1 什么是求精  13.2 關(guān)系的求精  13.3 關(guān)系求精的進(jìn)一步討論  13.4 相同狀態(tài)上的操作的求精  13.5 數(shù)據(jù)類型與數(shù)據(jù)求精  13.6 模擬關(guān)系與數(shù)據(jù)求精  13.7 模擬條件的寬松與解開第14章 操作求精  14.1 關(guān)系與操作構(gòu)型  14.2 向前模擬  14.3   向后模擬第15章 類型理論  15.1 預(yù)備知識(shí)  15.1.1 命題和集合  15.1.2 表達(dá)式理論  15.1.3  Martin-Lof類型理論  15.2 多型集合    15.2.1 基本規(guī)則    15.2.2 集合族的笛氏積和不交和    15.2.3 兩個(gè)集合的笛氏積和不交和    15.2.4 各種集合    15.2.5 相等性集合    15.2.6 小集合之集合    15.2.7 良序    15.2.8 一般樹  15.3 子集合    15.3.1 子集合一般理論    15.3.2 命題常元  15.4 單型集合    15.4.1 類型    15.4.2 類型對(duì)集合的定義第16章 時(shí)序邏輯  16.1 XYZ系統(tǒng)簡介  16.2 時(shí)序邏輯語言XYZ/E的基礎(chǔ)部分    16.2.1 基本概念    16.2.2 狀態(tài)轉(zhuǎn)換與單元    16.2.3 三種不同形式的控制結(jié)構(gòu)    16.2.4 Horn子句語言XYZ/PE0    16.2.5 指針  16.3 時(shí)序邏輯語言XYZ/E的基層模塊    16.3.1 程序框架    16.3.2 過程與函數(shù)    16.3.3 包塊  16.4 時(shí)序邏輯語言XYZ/E的并發(fā)成分    16.4.1 進(jìn)程與并行語句    16.4.2 通信

圖書封面

圖書標(biāo)簽Tags

無

評(píng)論、評(píng)分、閱讀與下載

---

    軟件工程形式化方法與語言 PDF格式下載

---