《计算系统的形式语义》陆汝钤 | PDF下载|ePub下载

第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的概率分支双模拟
· · · · · ·