形式語義學基礎與形式說明（第2版）

編輯推薦

中國信息安全測評中心自然科學基金項目內容組成之一
站在軟體立場上討論計算機科學的理論及其套用
詳細給出形式語義學的基礎理論框架
理論與軟體實踐相結合

內容簡介

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

作者簡介

屈延文，現任中國信息安全產業商會機構常務副理事長，中國信息安全測評中心顧問和北京大學、武漢大學、華中科技大學等兼職教授，是信息化與安全總體諮詢機構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 並發程式設計語言的公理語義
習題
參考文獻

形式語義學基礎與形式說明（第2版）

基本介紹

編輯推薦

內容簡介

作者簡介

目錄

相關詞條

熱門詞條