-- 會員 / 註冊 -- 　
　帳號：
　密碼：
　 | 註冊 | 忘記密碼
3/26 新書到！ 3/19 新書到！ 3/14 新書到！ 12/12 新書到！
購書流程•Q & A•站務留言版•客服信箱
│ 3ds Max│ Maya│ Rhino│ After Effects│ SketchUp│ ZBrush│ Painter│ Unity│
│ PhotoShop│ AutoCad│ MasterCam│ SolidWorks│ Creo│ UG│ Revit│ Nuke│
│ C#│ C│ C++│ Java│ 遊戲程式│ Linux│ 嵌入式│ PLC│ FPGA│ Matlab│
│ 駭客│ 資料庫│ 搜索引擎│ 影像處理│ Fluent│ VR+AR│ ANSYS│ 深度學習│
│ 單晶片│ AVR│ OpenGL│ Arduino│ Raspberry Pi│ 電路設計│ Cadence│ Protel│
│ Hadoop│ Python│ Stm32│ Cortex│ Labview│ 手機程式│ Android│ iPhone│
可查書名,作者,ISBN,3dwoo書號
詳細書籍分類

計算系統的形式語義

( 簡體 字)
作者：陸汝鈐類別：1. -> 程式設計 -> 綜合
譯者：
出版社：清華大學出版社計算系統的形式語義 3dWoo書號： 46038
詢問書籍請說出此書號！

【有庫存】
NT售價： 1990 元

出版日：1/1/2017
頁數：
光碟數：0
站長推薦：
印刷：黑白印刷語系： ( 簡體 版 )
加入購物車 │加到我的最愛
(請先登入會員)
ISBN：9787302414940
作者序　|　譯者序　|　前言　|　內容簡介　|　目錄　|　序
(簡體書上所述之下載連結耗時費功, 恕不適用在台灣, 若讀者需要請自行嘗試, 恕不保證)
作者序：

譯者序：

前言：

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

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

第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拟Milner邏輯

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拟Yao模型、可達性模型和約束系統

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拟PEPA

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的概率分支雙模擬

序：