計算系統(tǒng)的形式語義

第1章數(shù)學(xué)基礎(chǔ)1.1λ演算1.2格論1.3范疇論1.4不動點理論1.5Petri網(wǎng)論1.6Hilbert空間和相關(guān)拓?fù)?、代?shù)結(jié)構(gòu)1.7概率和隨機(jī)過程1.8矢列演算、線性邏輯、線性類型系統(tǒng)和線性帶類型λ演算1.8.1從矢列演算講起1.8.2線性邏輯1.8.3線性類型系統(tǒng) 第2章操作語義2.1概述2.2SECD抽象機(jī)2.3維也納定義語言2.4赫斯利方法和PL／Ⅰ標(biāo)準(zhǔn)2.5W文法及其抽象機(jī)2.6變換語義學(xué)2.7結(jié)構(gòu)化的操作語義 第3章指稱語義3.1概述3.2指稱語義的描述方法3.3函數(shù)式語言的指稱語義3.4命令式語言： 直接語義和繼續(xù)語義3.5變量、說明和作用域3.6過程和函數(shù)3.7元語言META Ⅳ3.8域的遞歸理論3.9遞歸域的兩個模型3.10冪域理論3.11不確定程序的指稱語義3.12概率冪域和概率指稱語義3.13基于概率不確定冪域的指稱語義3.14計算理論的范疇論語義 第4章公理語義4.1概述4.2Hoare公理系統(tǒng)4.3分程序的公理語義4.4過程的公理語義4.5聯(lián)立子程序的公理語義4.6類程的公理語義4.7Pascal的公理語義4.8完備性和可表達(dá)性4.9過程公理的健康性和完備性4.10完全正確性4.11最弱前置條件和不確定性公理語義4.12最弱概率前置語義4.12.1概率程序的最弱前置語義4.12.2概率不確定程序的最弱前置語義4.13類型理論和程序邏輯4.14模態(tài)邏輯和時序邏輯4.15分支時序邏輯和線性時序邏輯4.16區(qū)間邏輯和時段演算4.16.1區(qū)間邏輯IL4.16.2時段演算DC4.16.3一個實例4.17動態(tài)邏輯 第5章代數(shù)語義5.1概述5.2Σ代數(shù)和初始語義5.3擴(kuò)充的公理形式5.4健康性、完備性和可判定性5.5充分完備性和層次一致性5.6理論描述語言Clear5.7代數(shù)語義的范疇論基礎(chǔ)5.8終結(jié)語義5.9格語義5.10可觀察性和觀察等價性5.11偏Σ代數(shù)5.12模型描述語言ASL5.13程序設(shè)計語言的代數(shù)語義5.14帶動態(tài)結(jié)構(gòu)的程序的語義 第6章并發(fā)和分布式程序的形式語義6.1概述6.2分布式程序設(shè)計語言CSP6.3CSP的結(jié)構(gòu)化操作語義6.4CSP的流語義6.5TCSP和失敗語義6.6并行程序的公理語義6.7CSP的公理語義6.8通信系統(tǒng)演算(CCS)6.9CCS的操作語義6.10同步樹和通信樹6.11雙模擬和行為等價性6.12SCCS和集合推導(dǎo)語義6.13CCS的偏序推導(dǎo)語義6.14CCS的Petri網(wǎng)語義6.15分布式變遷系統(tǒng)和CCS6.16CCS的真并發(fā)語義6.17HennessyMilner 邏輯6.17.1基本HM邏輯6.17.2帶遞歸HM邏輯6.18通信進(jìn)程代數(shù) ACP家族及其靜態(tài)語義6.18.1基本進(jìn)程代數(shù)BPA 6.18.2進(jìn)程代數(shù)PA6.18.3通信進(jìn)程代數(shù)ACP6.18.4ACP的擴(kuò)充6.18.5ACP的最大擴(kuò)充ACPc6.19動態(tài)ACP及其操作語義6.20ACP的指稱語義和雙模擬語義6.21抽象數(shù)據(jù)類型作為進(jìn)程代數(shù)的代數(shù)語義6.22進(jìn)程代數(shù)并發(fā)語義的比較研究 第7章移動通信和移動計算系統(tǒng)的形式語義7.1概述 7.2π演算及其操作語義7.3π演算的雙模擬語義7.4進(jìn)程代數(shù)的符號變遷語義7.4.1CCS型的進(jìn)程代數(shù)的符號語義7.4.2π演算的（強(qiáng)）符號語義7.4.3π演算的（弱）符號語義7.5多維π演算和異步π演算 7.5.1多維π演算7.5.2異步π演算7.6安全π演算SPI7.7SPI演算的環(huán)境敏感雙模擬語義 7.8Applied π演算 7.9Applied π演算的符號語義7.9.1Delaune，Kremer和Ryan的DApplied π演算及其符號語義7.9.2DolevYao模型、可達(dá)性模型和約束系統(tǒng)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演算的類型系統(tǒng)7.13分布式Ambient演算的雙模擬語義7.14安全Ambient演算及其雙模擬語義7.14.1安全Ambient演算SA7.14.2帶口令的安全Ambient演算SAP7.15封裝Ambient演算7.15.1封裝Ambient演算BA7.15.2新封裝Ambient演算NBA7.15.3密封Ambient演算SBA 第8章非規(guī)范進(jìn)程代數(shù)和微觀生命系統(tǒng)的形式語義8.1概述8.2從強(qiáng)化操作語義到因果π演算8.3概率進(jìn)程代數(shù)8.3.1部分概率進(jìn)程代數(shù)PCCS8.3.2全概率進(jìn)程代數(shù)APPA8.4性能評估進(jìn)程代數(shù)PEPA8.5隨機(jī)π演算8.6含噪π演算8.7進(jìn)程演算的拓?fù)淅碚?.8進(jìn)程序列演算CPS8.8.1CPS的語法和操作語義8.8.2CPS的序列雙模擬語義8.8.3CPS的特征序列雙模擬語義8.9CPS的序列極限雙模擬8.9.1動程的貼近雙模擬語義8.9.2CPS的極限序列雙模擬語義8.10Gillespie算法8.11π通路演算——分子水平的生物進(jìn)程代數(shù)8.11.1關(guān)于通路8.11.2π通路演算編程信號傳導(dǎo)通路8.11.3隨機(jī)π通路演算編程基因調(diào)控通路8.12κ演算——基于規(guī)則的蛋白質(zhì)相互作用語言8.12.1蛋白質(zhì)相互作用和κ演算8.12.2κ演算的操作語義和帶鉤語義8.12.3κ演算的指稱語義8.13從Gamma模型到化學(xué)抽象機(jī)8.13.1Gamma計算模型8.13.2化學(xué)抽象機(jī)8.13.3概率化學(xué)抽象機(jī)8.13.4模糊化學(xué)抽象機(jī)8.14生化抽象機(jī)和計算樹邏輯 8.15溶液級建模語言BioPEPA8.16固定生物膜計算和P系統(tǒng)8.16.1基本P系統(tǒng)及其變型8.16.2基于通信的P系統(tǒng)8.16.3面向DNA計算的H系統(tǒng)和拼接P系統(tǒng)8.16.4神經(jīng)型P系統(tǒng)和尖峰放電型P系統(tǒng)8.17基于移動生物膜的BioAmbients演算8.17.1BioAmbients演算的基本內(nèi)容8.17.2隨機(jī)BioAmbients演算8.18膜演算語言Brane 8.18.1膜演算8.18.2射影膜演算 第9章量子語言的形式語義9.1概述9.2一些基本概念9.2.1基于波動力學(xué)的量子力學(xué)公設(shè)9.2.2量子力學(xué)公設(shè)的Hilbert空間表示9.2.3量子力學(xué)公設(shè)的Dirac表示形式9.3量子隨機(jī)存取機(jī)、量子偽碼及其操作語義 9.3.1Knill的量子隨機(jī)存取機(jī)QRAM9.3.2Nagarajan等的順序量子隨機(jī)存取機(jī)SQRAM9.3.3Ado和Mateus的基于復(fù)雜性分析的QRAM設(shè)計及其操作語義9.4命令式量子語言及其操作語義9.4.1命令式量子程序設(shè)計語言QCL9.4.2命令式量子程序設(shè)計語言LanQ的抽象機(jī)語義9.4.3不確定性命令式量子語言qGCL 9.5量子λ演算及其類型系統(tǒng) 9.6函數(shù)式量子語言的框圖操作語義9.7量子程序語義的范疇論詮釋9.8量子可逆計算和不可逆計算9.8.1刻畫可逆計算的嚴(yán)格廣群語義9.8.2刻畫不可逆計算的幺半群范疇語義9.8.3函數(shù)式量子語言QML及其可逆化操作語義9.8.4從不可逆計算到可逆計算： pGCL語言的可逆化改造 9.9函數(shù)式量子語言的范疇論指稱語義9.10量子程序的最弱前置條件語義和公理語義 9.10.1Hermitian算子作為量子謂詞9.10.2最弱前置條件語義及其證明規(guī)則9.10.3量子程序的Hoare公理系統(tǒng)9.11量子進(jìn)程代數(shù)的操作語義9.11.1量子進(jìn)程代數(shù)QPALg9.11.2通信量子進(jìn)程CQP9.11.3量子多項式機(jī)器QPM9.12量子進(jìn)程代數(shù)的雙模擬語義 9.12.1qCCS1及其量子概率雙模擬語義9.12.2qCCS2及其漸近雙模擬9.12.3QPALg的概率分支雙模擬