計(jì)算系統(tǒng)的形式語(yǔ)義

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