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

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