☆☆☆☆☆




點擊這裡下載

類似圖書 點擊查看全場最低價

---

內容簡介

　　　　計算係統的形式語義是目前計算機科學理論研究的兩大方嚮之一，其研究成果對程序設計語言、編譯技術、應用軟件、分布式係統等分支領域有重大的實際意義。本書大體上分為三個部分。第一部分是數學基礎，為第一章。第二部分包括第二到第五章，概述瞭形式語義中的操作語義、指稱語義、公理語義和代數語義四大經典流派。第三部分包括第六到第九章，概述瞭形式語義學的現代應用， 分彆介紹分布式係統、移動計算和移動通信係統、非規範進程代數和微觀生命係統，以及量子程序設計語言的形式語義。 　　全書內容豐富，結構嚴謹，集形式語義學理論及其應用的有關分支之大成，係統地反映瞭這個領域各方麵的研究成果，特彆是它的近代發展潮流和趨勢，並對不同流派的理論和方法給予瞭分析和評論。 　　本書可作為計算機科學專業研究生、本科生有關課程的教材或教學參考書，也可供有關專業或交叉學科的科研人員進修或作為工具書。

內頁插圖

目錄

第1章數學基礎
1.1λ演算
1.2格論
1.3範疇論
1.4不動點理論
1.5Petri網論
1.6Hilbert空間和相關拓撲、代數結構
1.7概率和隨機過程
1.8矢列演算、綫性邏輯、綫性類型係統和綫性帶類型λ演算
1.8.1從矢列演算講起
1.8.2綫性邏輯
1.8.3綫性類型係統

第2章操作語義
2.1概述
2.2SECD抽象機
2.3維也納定義語言
2.4赫斯利方法和PL／Ⅰ標準
2.5W文法及其抽象機
2.6變換語義學
2.7結構化的操作語義

第3章指稱語義
3.1概述
3.2指稱語義的描述方法
3.3函數式語言的指稱語義
3.4命令式語言： 直接語義和繼續語義
3.5變量、說明和作用域
3.6過程和函數
3.7元語言META Ⅳ
3.8域的遞歸理論
3.9遞歸域的兩個模型
3.10冪域理論
3.11不確定程序的指稱語義
3.12概率冪域和概率指稱語義
3.13基於概率不確定冪域的指稱語義
3.14計算理論的範疇論語義

第4章公理語義
4.1概述
4.2Hoare公理係統
4.3分程序的公理語義
4.4過程的公理語義
4.5聯立子程序的公理語義
4.6類程的公理語義
4.7Pascal的公理語義
4.8完備性和可錶達性
4.9過程公理的健康性和完備性
4.10完全正確性
4.11最弱前置條件和不確定性公理語義
4.12最弱概率前置語義
4.12.1概率程序的最弱前置語義
4.12.2概率不確定程序的最弱前置語義
4.13類型理論和程序邏輯
4.14模態邏輯和時序邏輯
4.15分支時序邏輯和綫性時序邏輯
4.16區間邏輯和時段演算
4.16.1區間邏輯IL
4.16.2時段演算DC
4.16.3一個實例
4.17動態邏輯

第5章代數語義
5.1概述
5.2Σ代數和初始語義
5.3擴充的公理形式
5.4健康性、完備性和可判定性
5.5充分完備性和層次一緻性
5.6理論描述語言Clear
5.7代數語義的範疇論基礎
5.8終結語義
5.9格語義
5.10可觀察性和觀察等價性
5.11偏Σ代數
5.12模型描述語言ASL
5.13程序設計語言的代數語義
5.14帶動態結構的程序的語義

第6章並發和分布式程序的形式語義
6.1概述
6.2分布式程序設計語言CSP
6.3CSP的結構化操作語義
6.4CSP的流語義
6.5TCSP和失敗語義
6.6並行程序的公理語義
6.7CSP的公理語義
6.8通信係統演算(CCS)
6.9CCS的操作語義
6.10同步樹和通信樹
6.11雙模擬和行為等價性
6.12SCCS和集閤推導語義
6.13CCS的偏序推導語義
6.14CCS的Petri網語義
6.15分布式變遷係統和CCS
6.16CCS的真並發語義
6.17Hennessy�睲ilner 邏輯
6.17.1基本HM邏輯
6.17.2帶遞歸HM邏輯
6.18通信進程代數 ACP傢族及其靜態語義
6.18.1基本進程代數BPA
6.18.2進程代數PA
6.18.3通信進程代數ACP
6.18.4ACP的擴充
6.18.5ACP的最大擴充ACPc
6.19動態ACP及其操作語義
6.20ACP的指稱語義和雙模擬語義
6.21抽象數據類型作為進程代數的代數語義
6.22進程代數並發語義的比較研究

第7章移動通信和移動計算係統的形式語義
7.1概述
7.2π演算及其操作語義
7.3π演算的雙模擬語義
7.4進程代數的符號變遷語義
7.4.1CCS型的進程代數的符號語義
7.4.2π演算的（強）符號語義
7.4.3π演算的（弱）符號語義
7.5多維π演算和異步π演算
7.5.1多維π演算
7.5.2異步π演算
7.6安全π演算SPI
7.7SPI演算的環境敏感雙模擬語義
7.8Applied π演算
7.9Applied π演算的符號語義
7.9.1Delaune，Kremer和Ryan的DApplied π演算及其
符號語義
7.9.2Dolev�瞃ao模型、可達性模型和約束係統
7.9.3劉佳和林惠民的符號LApplied π演算語義
7.10對稱π演算： χ演算和Fusion演算
7.10.1χ演算
7.10.2Fusion演算
7.11移動Ambient演算
7.11.1基本Ambient演算——移動Ambient演算
7.11.2完整Ambient演算——通信Ambient演算
7.12Ambeint演算的類型係統
7.13分布式Ambient演算的雙模擬語義
7.14安全Ambient演算及其雙模擬語義
7.14.1安全Ambient演算SA
7.14.2帶口令的安全Ambient演算SAP
7.15封裝Ambient演算
7.15.1封裝Ambient演算BA
7.15.2新封裝Ambient演算NBA
7.15.3密封Ambient演算SBA

第8章非規範進程代數和微觀生命係統的形式語義
8.1概述
8.2從強化操作語義到因果π演算
8.3概率進程代數
8.3.1部分概率進程代數PCCS
8.3.2全概率進程代數APPA
8.4性能評估進程代數PEPA
8.5隨機π演算
8.6含噪π演算
8.7進程演算的拓撲理論
8.8進程序列演算CPS
8.8.1CPS的語法和操作語義
8.8.2CPS的序列雙模擬語義
8.8.3CPS的特徵序列雙模擬語義
8.9CPS的序列極限雙模擬
8.9.1動程的貼近雙模擬語義
8.9.2CPS的極限序列雙模擬語義
8.10Gillespie算法
8.11π通路演算——分子水平的生物進程代數
8.11.1關於通路
8.11.2π通路演算編程信號傳導通路
8.11.3隨機π通路演算編程基因調控通路
8.12κ演算——基於規則的蛋白質相互作用語言
8.12.1蛋白質相互作用和κ演算
8.12.2κ演算的操作語義和帶鈎語義
8.12.3κ演算的指稱語義
8.13從Gamma模型到化學抽象機
8.13.1Gamma計算模型
8.13.2化學抽象機
8.13.3概率化學抽象機
8.13.4模糊化學抽象機
8.14生化抽象機和計算樹邏輯
8.15溶液級建模語言Bio�睵EPA
8.16固定生物膜計算和P係統
8.16.1基本P係統及其變型
8.16.2基於通信的P係統
8.16.3麵嚮DNA計算的H係統和拼接P係統
8.16.4神經型P係統和尖峰放電型P係統
8.17基於移動生物膜的BioAmbients演算
8.17.1BioAmbients演算的基本內容
8.17.2隨機BioAmbients演算
8.18膜演算語言Brane
8.18.1膜演算
8.18.2射影膜演算

第9章量子語言的形式語義
9.1概述
9.2一些基本概念
9.2.1基於波動力學的量子力學公設
9.2.2量子力學公設的Hilbert空間錶示
9.2.3量子力學公設的Dirac錶示形式
9.3量子隨機存取機、量子僞碼及其操作語義
9.3.1Knill的量子隨機存取機QRAM
9.3.2Nagarajan等的順序量子隨機存取機SQRAM
9.3.3Ado和Mateus的基於復雜性分析的QRAM設計及其
操作語義
9.4命令式量子語言及其操作語義
9.4.1命令式量子程序設計語言QCL
9.4.2命令式量子程序設計語言LanQ的抽象機語義
9.4.3不確定性命令式量子語言qGCL
9.5量子λ演算及其類型係統
9.6函數式量子語言的框圖操作語義
9.7量子程序語義的範疇論詮釋
9.8量子可逆計算和不可逆計算
9.8.1刻畫可逆計算的嚴格廣群語義
9.8.2刻畫不可逆計算的幺半群範疇語義
9.8.3函數式量子語言QML及其可逆化操作語義
9.8.4從不可逆計算到可逆計算： pGCL語言的可逆化改造

9.9函數式量子語言的範疇論指稱語義
9.10量子程序的最弱前置條件語義和公理語義
9.10.1Hermitian算子作為量子謂詞
9.10.2最弱前置條件語義及其證明規則
9.10.3量子程序的Hoare公理係統
9.11量子進程代數的操作語義
9.11.1量子進程代數QPALg
9.11.2通信量子進程CQP
9.11.3量子多項式機器QPM
9.12量子進程代數的雙模擬語義
9.12.1qCCS1及其量子概率雙模擬語義
9.12.2qCCS2及其漸近雙模擬
9.12.3QPALg的概率分支雙模擬

前言/序言

　　前言計算係統的形式語義前言 　　本書是1992年齣版的《計算機語言的形式語義》一書（簡稱1992版）的更新版。在1992版中我們分彆介紹瞭形式語義形式語義的四個主要流派：操作語義、指稱語義、公理語義和代數語義，並在此基礎上綜閤闡述瞭並發和分布式程序分布式程序的形式語義。從該書齣版以來，已經二十餘年過去瞭，在此期間，國內外形式語義學的研究有瞭許多重大的突破。 　　首先，應該提到的是移動通信的發展促進瞭一類新的進程代數——π演算的齣現和發展，使得用進程代數編寫的程序不僅可以在固定網絡上運行，而且可以改變通信網絡的拓撲結構，並在可變的網絡結構上實行通信。圍繞π演算齣現瞭許多變種，開展瞭深入的研究。除瞭可變的網絡結構之外，π演算還創造瞭其他的手段來改進通信技術。例如，利用π演算，有可能建立專用的私密信道。隨著π演算而興起的環境演算環境演算Ambient甚至可以提供建立網上防火牆的手段。服務於保密通信的Spi演算Spi演算把編碼和解碼引進瞭語言之中。帶有噪音信道的含噪進程代數有希望把香農的信息論引進進程代數中，從而在兩類通信理論之間架起一座橋梁。所有這些使得服務於移動通信的進程代數成瞭一門單獨的學問。 　　其次，分子生物學是近年來發展最快的研究方嚮之一。人類基因圖譜的測序完成大大推動瞭基因組學、蛋白質組學，以及係統生物學的研究。恩格斯曾經說過，數學在生物學中的應用為零，但是這樣的時代早就過去瞭。以數學為基礎的形式化方法已經深入到生物領域，成為描述微觀生命現象的有力手段。特彆值得稱道的是概率論和隨機過程作為重要的數學手段在麵嚮微觀生命現象的進程代數理論中發揮瞭重要作用。除瞭概率進程代數、隨機進程代數和性能評估進程代數這些比較通用的工具之外，一大批特意針對微觀生命現象的描述工具已經被設計齣來並投入應用。諸如Bioambient、因果π演算、化學抽象機、生化抽象機等工具提供瞭許多頗有啓發的思路。描述微觀生命現象的數學工具早已經不純粹是微積分和微分方程等連續數學的天下，而成瞭連續工具和離散工具八仙過海的多極世界。 　　再次，實用化量子計算機齣現和推廣應用的前景正在吸引越來越多的科學傢關注量子計算領域。近年來齣現瞭一批麵嚮量子計算的程序設計語言，其中也包括量子進程代數，科學傢們已經開始討論量子軟件和量子軟件工程。量子程序設計和經典程序設計有許多本質不同。例如，量子不可剋隆原理的存在使得量子程序設計語言不可能有簡單的賦值語句。同時，由於對一個量子係統的測量會引起該係統所處狀態的坍縮，這使得係統狀態的可觀察性和程序運行流程的可控製性受到影響。另一方麵，量子力學的特殊性質並非隻對量子程序設計起限製作用，它的某些性質有可能對量子程序設計是“有用”的。例如，量子離物傳態量子離物傳態、量子密集編碼、量子密碼通信等方麵的研究成果有可能對量子網絡和分布式量子軟件工程産生較大影響，宜於我們去關注和開發利用。在一定意義上，量子程序的運行可以用經典程序來模擬。因此，盡管量子計算機還沒有完全實現，但是量子程序設計和量子軟件的研究並不一定要等到量子計算機實現以後再做，而是可以先行一步。而量子密碼通信先於量子計算機的實現又提供瞭研究量子軟件的必要性和現實性。更進一步說，量子軟件的研究成果可以為未來量子計算機的設計提供新思路，比起先有經典計算機，後有經典程序設計的曆史來說，這樣做更閤理。同樣，在實際設計和使用量子程序設計語言之前先把它們的數學基礎，即形式語義研究清楚，然後再去設計和使用，這比起傳統的程序設計語言先設計、先使用，後論證其理論基礎、後補其漏洞來說，未嘗不是一件好事。 　　近十餘年來形式語義學的研究成果極其豐富，本書把以上三個方麵作為補寫和更新的重點，是充分考慮到實踐需求的一種選擇。這三個方麵都具有強烈的應用背景，同時又有深刻的理論問題，構成瞭三個新的章。同時本書也對原有的六章內容做瞭必要的補充。其中主要的四部分是：指稱語義一章原書以（反映程序不確定性的）冪域理論結尾，本書添加瞭概率冪域理論和概率加不確定性冪域理論，同時還介紹瞭基於單體的計算理論和指稱語義的完全抽象性完全抽象性研究。在公理語義一章添加瞭Hoare邏輯的概率推廣和Dijkstra最弱前置條件語義最弱前置條件語義（簡稱最弱前置語義）的概率推廣。同時還介紹瞭基於一種實時模態邏輯的時段演算。並發和分布式語義一章原來重點介紹瞭CSP和CCS兩個進程代數理論，本書補充介紹瞭另一個重要的進程代數ACP， 從而比較完備地展示瞭進程代數傢族的三劍客架構。另外還分彆給齣瞭以擴充Petri網形式齣現的CCS真並發語義和以抽象數據類型形式齣現的CCS代數語義。這兩種方法原則上可以推廣到其他進程代數。這一章最後以Glabbeek的進程代數並發語義的比較研究結尾。最後，由於本書增添瞭以上各項內容，對第一章數學基礎也要做必要的（最低限度的）增補。其中完整增加的有三節：一些基本的代數、拓撲和泛函知識，概率和隨機過程隨機過程知識，以及綫性邏輯和Gentzen演算知識。另外對範疇論和格論兩節做瞭必要的增補。 　　自然界有大量的信息交換並不采取人類語言或計算機語言的形式。一個明顯的例子是生命係統。例如，DNA序列就可以看成是一種文字，它構成瞭生命的“天書”。基因對蛋白質的錶達，細胞間和細胞內部的通信，這裏都有信息交換和信息處理在起作用。另一個明顯的例子是量子係統。凡涉及量子計算、量子糾纏、量子通信、量子密鑰等問題，無不歸於信息錶示和信息處理的範疇。盡管現在的生命過程描述語言和量子程序設計語言都以計算機語言的形式齣現，用於生命現象的模擬、預測和量子計算機的編程，我們仍然可以把微觀生命係統和量子係統看成自然界的“天造”計算係統。俗話說人算不如天算，它們不僅應該和人造的計算係統平起平坐，而且還為人造計算係統提供瞭啓示和展望。為此也需要形式化的數學工具，以嚴格和正確地刻畫生命信息和量子信息的錶示和處理。為此，我們統稱本書的內容為計算係統的形式語義。 　　本書的內容通過每章的概述、除概述以外的各節，以及文獻和中、英名詞索引四部分組成，它們互不包含。概述是各章涉及內容的一個鳥瞰。章中各節是對其中某些內容有選擇地展開講解。文獻是前兩部分內容的齣處和延伸閱讀信息，其中早期文獻可以提供有關研究的發展淵源信息，而近期文獻則可以提供相關領域的發展前景和專傢們的視角。由於形式語義的文獻數量極多，肯定有一些重要的有關文獻在寫作本書時被遺漏掉。即使是已經列入本書介紹範圍的一些文獻，也肯定有一些因為作者理解不深，甚至理解有誤而未能在本書中正確介紹其思想。我想提請讀者注意的是，本書不能作為開展研究工作的直接依據。有興趣在形式語義領域開展研究的讀者，可以參照本書提供的綫索，進一步閱讀原著文獻，可以在閱讀時對照本書的解釋、分析和某些進一步的發展，但是不能忽視閱讀原著，以免齣現可能的誤導。 　　本書在撰寫過程中得到瞭很多專傢的幫助。從開始有寫這本書的計劃起，作者經常和應明生教授就此交流看法並得到他的很多寶貴建議。應明生、周巢塵、林惠民、夏培肅、陳儀香、袁崇義、林闖、李未、李剋正、Bauer、Petri、Broy、Krieg�睟rückner、Reisig等教授都曾嚮作者提供他們的著作，使作者獲得瞭寶貴的知識來源。為撰寫本書，作者參考的文獻數量較大，無法一一緻謝。其中包括許多不署名的維基百科類資料，非常感謝這些未曾謀麵的知識傳播者。我們在書中盡可能地對引用的資料給齣瞭齣處，包括插圖。 　　為瞭減少本書可能給讀者帶來的枯燥感，我們在每一章的前麵加配瞭一首唐詩，每首詩的意境和它所在章的內容（之某些重要部分）存在一些本質的聯想。我想讀者會同意：在文化藝術和科學技術這兩個差彆巨大的領域之間不可能有真正的科學對應關係或推理關係，必須強調這僅僅是一種聯想關係。它肯定不唯一，也肯定因人而異。學習和研究都是艱苦的勞動，但同時也應該是快樂的。作者贊成博拉·米盧蒂諾維奇的快樂足球理念，從事科學工作也要有快樂感。在此感謝馬鼕潔應邀為封麵作圖，並為每章的唐詩配圖作畫，使本書增色不少。 　　作者真誠地感謝清華大學齣版社的大度寬容和堅定支持，使得這本撰寫時間寬度達十年以上的書稿能夠最終完成。
計算係統的形式語義 下載 mobi epub pdf txt 電子書

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

評分☆☆☆☆☆

類似圖書 點擊查看全場最低價

查看全網最低價