形式語義學基礎與形式說明(第二版)（簡體書）

本書第一版是20世紀80年代國家教委計算機軟件專業教材編委會推薦教材之一。本書詳細地給出了形式語義學的基礎理論框架，但它並不是一本純理論的教材，而是一本理論與軟件實踐相結合的教材。
全書共分十章。介紹了指稱語義學、代數語義學、操作語義學與公理語義學的基本內容及其應用，并介紹了并發程序設計語言各流派的語義模型和新一代計算機計算模型的理論問題。例如curry的組合邏輯，Martin-Lof的直覺主義數學的討論都是近代計算機理論較重要的基礎內容。
本書內容豐富，重點突出，并配有大量習題，可作為高等院校電子信息、計算機科學專業本科高年級學生、研究生的教材，也可供信息技術人員和計算機軟件設計、工程人員參考。

屈延文，現任中國信息安全產業商會機構常務副理事長，中國信息安全測評中心顧問和北京大學、武漢大學、華中科技大學等兼職教授，是信息化與安全總體諮詢機構QNS工作室的主要成員之一。是中國CAD事業、軟件工程與計算機科學和信息化科學的開拓者與主要的推動者之一，是我國計算機程序設計語言、操作系統和軟件工程專家和中國著名計算機科學學者，參與并主持國家信息化多項重大工程建設工作。目前，他是信息化與安全的總體設計師，是中國信息安全產業標準化聯盟總體組組長，主持可信網絡世界體系結構框架（TCAF）標準體系的研究、制定和推動工作。同時，長期為國家培養了數量眾多的計算機科學和信息化科學的高水平的科學與技術人才。 軟件行為學、網絡世界行為學科（形式行為學）的開創者。曾著有《形式語義學基礎與形式說明》、《實用類型程序設計》、《軟件行為學》、《信息化行為學理論基礎與形式化方法》，主筆《銀行行為監管》和《銀行行為控制》等著作。

第1章 引論
1.1 形式語義學
1.2 指稱語義學
1.3 代數語義學
1.4 操作語義學
1.5 公理語義方法
1.6 形式說明語言
第2章 指稱語義學基礎
2.1 論域問題引子
2.2 域的構造
2.3 偏序與完全偏序
2.4 單調函數與連續函數
2.5 連續泛函
2.6 泛函不動點及遞歸程序
2.7 抽象及-演算
2.8 指稱語義定義初步
習題
參考文獻
第3章 程序設計語言的指稱語義
3.1 程序設計語言的基本概念
3.2 存儲語義
3.3 環境(聲明)語義
3.4 命令語義
3.5 表達式語義
3.6 連續
3.7 證明技術
3.8 小結
習題
參考文獻
第4章 指稱語義的一些例子
4.1 例子1
4.2 例子2
4.3 例子3
4.4 例子4
習題
參考文獻
第5章 代數語義學基礎
5.1 概述
5.2 范疇論
5.3 圖范疇及圖文法
5.4 類別代數理論
5.5 抽象數據類型
5.6 等式理論與項重寫系統
5.7 實例
習題
參考文獻
第6章 操作語義學與屬性文法
6.1 操作語義概述
6.2 施用表達式(AE)的機器計算
6.3 屬性文法概述
6.4 屬性文法分類
6.5 用屬性文法進行編譯程序設計
6.6 屬性文法定義語言
6.7 實例：AGDL的語法
習題
參考文獻
第7章 組合邏輯
7.1 概述
7.2 組合子
7.3 組合邏輯的語法理論
7.4 組合邏輯的邏輯基礎
7.5 函數性基本理論
7.6 范疇組合邏輯
7.7 小結
習題
參考文獻
第8章 公理語義方法
8.1 概述
8.2 程序正確性驗證的基本概念
8.3 程序正確性驗證技術
8.4 Hoare公理系統
8.5 Dijkstra的最弱前置條件
8.6 Martin-lof類型論
習題
參考文獻
第9章 維也納發展方法：Meta-Lallguage
9.1 概況
9.2 在VDM中的邏輯注釋
9.3 抽象數據類型
9.4 抽象文法
9.5 組合算子
9.6 VDM與程序設計語言
習題
參考文獻
第10章 并發程序設計語言的語義與說明
10.1 並行系統概述
10.2 并發程序設計語言概述
10.3 冪域及不確定性
10.4 通訊順序進程(CSP)
10.5 并發程序設計語言的指稱語義
10.6 通訊順序進程的操作語義
10.7 進程與通訊網絡的抽象數據類型
10.8 并發程序設計語言的公理語義
習題
參考文獻