计算系统的形式语义

　　计算系统的形式语义是目前计算机科学理论研究的两大方向之一，其研究成果对程序设计语言、编译技术、应用软件、分布式系统等分支领域有重大的实际意义。本书大体上分为三个部分。*部分是数学基础，为*章。第二部分包括第二到第五章，概述了形式语义中的操作语义、指称语义、公理语义和代数语义四大经典流派。第三部分包括第六到第九章，概述了形式语义学的现代应用， 分别介绍分布式系统、移动计算和移动通信系统、非规范进程代数和微观生命系统，以及量子程序设计语言的形式语义。全书内容丰富，结构严谨，集形式语义学理论及其应用的有关分支之大成，系统地反映了这个领域各方面的研究成果，特别是它的近代发展潮流和趋势，并对不同流派的理论和方法给予了分析和评论。本书可作为计算机科学专业研究生、本科生有关课程的教材或教学参考书，也可供有关专业或交叉学科的科研人员进修或作为工具书。

暂缺《计算系统的形式语义》作者简介

第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区间逻辑IL4.16.2时段演算DC4.16.3一个实例4.17动态逻辑 第5章代数语义5.1概述5.2Σ代数和初始语义5.3扩充的公理形式5.4健康性、完备性和可判定性5.5充分完备性和层次一致性5.6理论描述语言Clear5.7代数语义的范畴论基础5.8终结语义5.9格语义5.10可观察性和观察等价性5.11偏Σ代数5.12模型描述语言ASL5.13程序设计语言的代数语义5.14带动态结构的程序的语义 第6章并发和分布式程序的形式语义6.1概述6.2分布式程序设计语言CSP6.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分布式变迁系统和CCS6.16CCS的真并发语义6.17HennessyMilner 逻辑6.17.1基本HM逻辑6.17.2带递归HM逻辑6.18通信进程代数 ACP家族及其静态语义6.18.1基本进程代数BPA 6.18.2进程代数PA6.18.3通信进程代数ACP6.18.4ACP的扩充6.18.5ACP的最大扩充ACPc6.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安全π演算SPI7.7SPI演算的环境敏感双模拟语义 7.8Applied π演算 7.9Applied π演算的符号语义7.9.1Delaune，Kremer和Ryan的DApplied π演算及其符号语义7.9.2DolevYao模型、可达性模型和约束系统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演算SA7.14.2带口令的安全Ambient演算SAP7.15封装Ambient演算7.15.1封装Ambient演算BA7.15.2新封装Ambient演算NBA7.15.3密封Ambient演算SBA 第8章非规范进程代数和微观生命系统的形式语义8.1概述8.2从强化操作语义到因果π演算8.3概率进程代数8.3.1部分概率进程代数PCCS8.3.2全概率进程代数APPA8.4性能评估进程代数PEPA8.5随机π演算8.6含噪π演算8.7进程演算的拓扑理论8.8进程序列演算CPS8.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溶液级建模语言BioPEPA8.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的量子随机存取机QRAM9.3.2Nagarajan等的顺序量子随机存取机SQRAM9.3.3Ado和Mateus的基于复杂性分析的QRAM设计及其操作语义9.4命令式量子语言及其操作语义9.4.1命令式量子程序设计语言QCL9.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量子进程代数QPALg9.11.2通信量子进程CQP9.11.3量子多项式机器QPM9.12量子进程代数的双模拟语义 9.12.1qCCS1及其量子概率双模拟语义9.12.2qCCS2及其渐近双模拟9.12.3QPALg的概率分支双模拟