形式語義學基礎與形式說明

前言

　　本書是計算機專業(yè)人員和大學軟件、計算機科學和信息化科學專業(yè)高年級學生以及碩士研究生或博士研究生了解計算機科學理論在軟件工程應用的專門書籍。作者站在軟件的立場上來討論計算機科學（尤其是形式語義學）的理論及其應用。雖然，我們比較詳細地介紹了形式語義學基本理論框架，但它不是一本純理論的書籍，而是一本理論聯(lián)系實際的書籍；因此，在敘述中不苛求理論上的嚴密性?！　∽髡咴?980年，由于準備Ada語言的編譯程序和環(huán)境工作以及對軟件工程理論的關注，開始對形式語義學理論與實踐進行研究。當時出版本書的目標是全面提高軟件重用、軟件自動生成和軟件智能化的理論和技術水平。目前看來，這個目標現(xiàn)在仍然沒有過時。在20世紀80年代初，作者用三冊油印的講義，經過多年在北京大學、北京航空學院（北京航空航天大學）、中國科學院研究生院、北京信息工程學院和華北計算技術研究所為研究生講授此課；北京之外，在國防科技大學、武漢大學和其他大學也講授過此課程。在多年研究和講課的基礎上，本書的內容更加完善。20世紀80年代后期科學出版社正式出版了《形式語義學基礎與形式說明》一書。作為第一版，該書正式出版已經有20多年了，曾經兩次印刷，多年來一直有人不斷向作者尋求本書。在21世紀，信息化發(fā)展帶來了科學發(fā)展的強大新動力，尤其是信息化科學學科的提出，沖破了經典計算機科學研究的范圍，其中信息化和網絡世界的安全是最突出的領域。信息安全不僅需要實施更加嚴格的產品保證計劃，同時要求信息安全測評事業(yè)具有逐步達到高級別的安全測評能力，尤其是提高結構性和形式化驗證能力，依此來推動我國信息系統(tǒng)產品質量的全面提升。所以，必須對信息化與安全產業(yè)和測評機構進行結構性和形式化驗證方法的培訓。再版本書是實施這種高素質培訓的教材建設，再版工作被列為中國信息安全測評中心的自然科學基金項目內容之一?！　”緯侔孢€有更廣泛和深刻的意義。在20世紀90年代，作者開始特別關注信息化體系結構和信息安全的理論問題。顯然，信息化與網絡世界中的大量問題，例如互操作性和安全性問題，已經不可能從經典的計算機科學理論中得到幫助和指導。信息化的體系結構已經不是計算機的體系結構，不是軟件的體系結構，也不是應用系統(tǒng)的體系結構。信息化的體系結構概念要比這些方面的體系結構復雜得多。信息化體系結構的實踐告訴我們，要劃分運營、系統(tǒng)和技術三個視圖來研究體系結構。經過多年研究，作者認為，運營體系結構，從理論的高度看，其核心的概念范疇是主體和行為，包括人類信息化行為和網絡世界中的虛擬主體和行為。

內容概要

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

作者簡介

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

書籍目錄

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

章節(jié)摘錄

　　聲明范疇的成分在于建立及改變環(huán)境；命令范疇的成分（即語句世界的成分）在于執(zhí)行并改變狀態(tài)；而表達式范疇的成分在于計算產生值。在語言的聲明范疇中，又主要包括作用域及可見性兩個概念。在命令范疇中的原子成分是賦值語句，GOTO語句的存在主要用于改變程序的執(zhí)行順序，也就是說，具有GOTO語句的語言程序，其書寫順序與執(zhí)行順序是不同的。在表達式范疇中，函數(shù)定義（或稱函數(shù)抽象）與函數(shù)施用是兩個基本概念。如果一個表達式不僅計算產生值，而且還改變狀態(tài)，我們稱這個表達式有副作用（side-effect）?！　≡赩on Neumann計算機體系中，程序設計語言還引入了地址概念，致使表達式計算產生的值與地址聯(lián)系起來。如果使用這個值，則必須引用置有該值的內存的地址，我們稱這樣的程序是依賴于環(huán)境的，因為計算的結果與所在存儲器的位置有關。　　如果一個語言沒有命令范疇，它只有表達式范疇及表示類型與對象的聲明范疇，而且這種語言中的每一個函數(shù)都不依賴于環(huán)境而存在，那么它所計算的結果與所在存儲器的位置無關，只要滿足了函數(shù)定義域則可以處處施用，絕無副作用，那么稱這樣的語言為施用型語言（applicative language）?！　槭裁匆芯啃问秸Z義學呢？　　理論研究的最強大的動力是發(fā)展生產，促進社會的進步。軟件生產長期停留在手工勞動的狀態(tài)，生產力很低。像所有其他工業(yè)發(fā)展那樣，軟件產業(yè)也要追求自動化生產，大規(guī)模生成，高效率及高質量生產的目標。　　為了發(fā)展軟件生產力及保證軟件生產的質量，軟件工程方法被廣泛地研究并得到普遍的應用。軟件工程方法一般化分為如下幾個階段：

編輯推薦

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

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    形式語義學基礎與形式說明 PDF格式下載

---