计算系统的形式语义 上PDF|Epub|txt|kindle电子书版本下载

计算系统的形式语义 上PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第1章 数学基础1

1.1 λ演算1

1.2 格论14

1.3 范畴论32

1.4 不动点理论56

1.5 Petri网论64

1.6 Hilbert空间和相关拓扑、代数结构82

1.7 概率和随机过程95

1.8 矢列演算、线性逻辑、线性类型系统和线性带类型λ演算107

1.8.1 从矢列演算讲起107

1.8.2 线性逻辑111

1.8.3 线性类型系统118

第2章 操作语义125

2.1 概述125

2.2 SECD抽象机133

2.3 维也纳定义语言142

2.4 赫斯利方法和PL／I标准161

2.5 W文法及其抽象机174

2.6 变换语义学184

2.7 结构化的操作语义199

第3章 指称语义207

3.1 概述207

3.2 指称语义的描述方法225

3.3 函数式语言的指称语义229

3.4 命令式语言：直接语义和继续语义234

3.5 变量、说明和作用域243

3.6 过程和函数252

3.7 元语言META Ⅳ264

3.8 域的递归理论278

3.9 递归域的两个模型287

3.10 幂域理论303

3.11 不确定程序的指称语义316

3.12 概率幂域和概率指称语义322

3.13 基于概率不确定幂域的指称语义332

3.14 计算理论的范畴论语义344

第4章 公理语义351

4.1 概述351

4.2 Hoare公理系统361

4.3 分程序的公理语义373

4.4 过程的公理语义382

4.5 联立子程序的公理语义395

4.6 类程的公理语义412

4.7 Pascal的公理语义420

4.8 完备性和可表达性431

4.9 过程公理的健康性和完备性440

4.10 完全正确性451

4.11 最弱前置条件和不确定性公理语义461

4.12 最弱概率前置语义472

4.12.1 概率程序的最弱前置语义472

4.12.2 概率不确定程序的最弱前置语义479

4.13 类型理论和程序逻辑483

4.14 模态逻辑和时序逻辑498

4.15 分支时序逻辑和线性时序逻辑505

4.16 区间逻辑和时段演算518

4.16.1 区间逻辑IL518

4.16.2 时段演算DC522

4.16.3 一个实例527

4.17 动态逻辑531

第5章 代数语义539

5.1 概述539

5.2 Σ代数和初始语义545

5.3 扩充的公理形式556

5.4 健康性、完备性和可判定性565

5.5 充分完备性和层次一致性577

5.6 理论描述语言Clear583

5.7 代数语义的范畴论基础591

5.8 终结语义605

5.9 格语义613

5.10 可观察性和观察等价性620

5.11 偏Σ代数635

5.12 模型描述语言ASL648

5.13 程序设计语言的代数语义657

5.14 带动态结构的程序的语义667

第6章 并发和分布式程序的形式语义679

6.1 概述679

6.2 分布式程序设计语言CSP707

6.3 CSP的结构化操作语义716

6.4 CSP的流语义727

6.5 TCSP和失败语义734

6.6 并行程序的公理语义743

6.7 CSP的公理语义751

6.8 通信系统演算（CCS）768

6.9 CCS的操作语义772

6.10 同步树和通信树779

6.11 双模拟和行为等价性786

6.12 SCCS和集合推导语义797

6.13 CCS的偏序推导语义802

6.14 CCS的Petri网语义814

6.15 分布式变迁系统和CCS820

6.16 CCS的真并发语义830

6.17 Hennessy-Milner逻辑848

6.17.1 基本HM逻辑848

6.17.2 带递归HM逻辑853

6.18 通信进程代数ACP家族及其静态语义859

6.18.1 基本进程代数BPA859

6.18.2 进程代数PA860

6.18.3 通信进程代数ACP862

6.18.4 ACP的扩充864

6.18.5 ACP的最大扩充ACP870

6.19 动态ACP及其操作语义873

6.20 ACP的指称语义和双模拟语义883

6.21 抽象数据类型作为进程代数的代数语义892

6.22 进程代数并发语义的比较研究913

第7章 移动通信和移动计算系统的形式语义927

7.1 概述927

7.2 π演算及其操作语义952

7.3 π演算的双模拟语义975

7.4 进程代数的符号变迁语义986

7.4.1 CCS型的进程代数的符号语义986

7.4.2 π演算的（强）符号语义995

7.4.3 π演算的（弱）符号语义999

7.5 多维π演算和异步π演算1001

7.5.1 多维π演算1001

7.5.2 异步π演算1010

7.6 安全π演算SPI1020

7.7 SPI演算的环境敏感双模拟语义1039

7.8 Appliedπ演算1059

7.9 Applied π演算的符号语义1072

7.9.1 Delaune， Kremer和Ryan的DAppliedπ演算及其符号语义1072

7.9.2 Dolev-Yao模型、可达性模型和约束系统1082

7.9.3 刘佳和林惠民的符号LAppliedπ演算语义1085

7.10 对称π演算：x演算和Fusion演算1092

7.10.1 x演算1092

7.10.2 Fusion演算1098

7.11 移动Ambient演算1106

7.11.1 基本Ambient演算——移动Ambient演算1107

7.11.2 完整Ambient演算——通信Ambient演算1116

7.12 Ambeint演算的类型系统1119

7.13 分布式Ambient演算的双模拟语义1133

7.14 安全Ambient演算及其双模拟语义1142

7.14.1 安全Ambient演算SA1142

7.14.2 带口令的安全Ambient演算SAP1146

7.15 封装Ambient演算1155

7.15.1 封装Ambient演算BA1155

7.15.2 新封装Ambient演算NBA1161

7.15.3 密封Ambient演算SBA1165

第8章 非规范进程代数和微观生命系统的形式语义1169

8.1 概述1169

8.2 从强化操作语义到因果π演算1199

8.3 概率进程代数1210

8.3.1 部分概率进程代数PCCS1211

8.3.2 全概率进程代数APPA1226

8.4 性能评估进程代数PEPA1233

8.5 随机π演算1252

8.6 含噪π演算1261

8.7 进程演算的拓扑理论1275

8.8 进程序列演算CPS1296

8.8.1 CPS的语法和操作语义1296

8.8.2 CPS的序列双模拟语义1299

8.8.3 CPS的特征序列双模拟语义1309

8.9 CPS的序列极限双模拟1315

8.9.1 动程的贴近双模拟语义1315

8.9.2 CPS的极限序列双模拟语义1318

8.10 Gillespie算法1331

8.11 π通路演算——分子水平的生物进程代数1336

8.11.1 关于通路1336

8.11.2 π通路演算编程信号传导通路1338

8.11.3 随机π通路演算编程基因调控通路1345

8.12 κ演算——基于规则的蛋白质相互作用语言1352

8.12.1 蛋白质相互作用和κ演算1352

8.12.2 κ演算的操作语义和带钩语义1360

8.12.3 κ演算的指称语义1364

8.13 从Gamma模型到化学抽象机1367

8.13.1 Gamma计算模型1367

8.13.2 化学抽象机1368

8.13.3 概率化学抽象机1375

8.13.4 模糊化学抽象机1378

8.14 生化抽象机和计算树逻辑1380

8.15 溶液级建模语言Bio-PEPA1393

8.16 固定生物膜计算和P系统1405

8.16.1 基本P系统及其变型1407

8.16.2 基于通信的P系统1413

8.16.3 面向DNA计算的H系统和拼接P系统1414

8.16.4 神经型P系统和尖峰放电型P系统1419

8.17 基于移动生物膜的BioAmbients演算1426

8.17.1 BioAmbients演算的基本内容1426

8.17.2 随机BioAmbients演算1434

8.18 膜演算语言Brane1442

8.18.1 膜演算1442

8.18.2 射影膜演算1452

第9章 量子语言的形式语义1459

9.1 概述1459

9.2 一些基本概念1494

9.2.1 基于波动力学的量子力学公设1494

9.2.2 量子力学公设的Hilbert空间表示1496

9.2.3 量子力学公设的Dirac表示形式1498

9.3 量子随机存取机、量子伪码及其操作语义1509

9.3.1 Knill的量子随机存取机QRAM1509

9.3.2 Nagarajan等的顺序量子随机存取机SQRAM1512

9.3.3 Adao和Mateus的基于复杂性分析的QRAM设计及其操作语义1515

9.4 命令式量子语言及其操作语义1519

9.4.1 命令式量子程序设计语言QCL1519

9.4.2 命令式量子程序设计语言LanQ的抽象机语义1526

9.4.3 不确定性命令式量子语言qGC L1535

9.5 量子λ演算及其类型系统1537

9.6 函数式量子语言的框图操作语义1546

9.7 量子程序语义的范畴论诠释1557

9.8 量子可逆计算和不可逆计算1575

9.8.1 刻画可逆计算的严格广群语义1576

9.8.2 刻画不可逆计算的么半群范畴语义1579

9.8.3 函数式量子语言QML及其可逆化操作语义1583

9.8.4 从不可逆计算到可逆计算：pGCL语言的可逆化改造1583

9.9 函数式量子语言的范畴论指称语义1588

9.10 量子程序的最弱前置条件语义和公理语义1599

9.10.1 Hermitian算子作为量子谓词1599

9.10.2 最弱前置条件语义及其证明规则1605

9.10.3 量子程序的Hoare公理系统1609

9.11 量子进程代数的操作语义1613

9.11.1 量子进程代数QPALg1613

9.11.2 通信量子进程CQP1620

9.11.3 量子多项式机器QPM1624

9.12 量子进程代数的双模拟语义1630

9.12.1 qCCS1及其量子概率双模拟语义1630

9.12.2 qCCS2及其渐近双模拟1640

9.12.3 QPALg的概率分支双模拟1649

参考文献1655

中英名词索引1745

英中名词索引1801