计算机语言的形式语义PDF电子书下载

第一章 数学基础 1

1.1 λ演算 1

1.2 格论 16

1.3 范畴论 34

1.4 不动点理论 60

1.5 Petri网论 71

第二章 操作语义 95

2.1 概述 95

2.2 SECD抽象机 105

2.3 维也纳定义语言 116

2.4 赫斯利方法和PL/I标准 139

2.5 W文法及其抽象机 156

2.6 变换语义学 168

2.7 结构化的操作语义 186

第三章 指称语义 196

3.1 概述 196

3.2 指称语义的描述方法 206

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

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

3.5 变量、说明和作用域 228

3.6 过程和函数 239

3.7 元语言METAIV 254

3.8 域的递归理论 270

3.9 递归域的两个模型 283

3.10 幂域理论 303

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

4.1 概述 327

第四章 公理语义 327

4.2 Hoare公理系统 339

4.3 分程序的公理语义 353

4.4 过程的公理语义 364

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

4.6 类程的公理语义 399

4.7 Pascal的公理语义 409

4.8 完备性和可表达性 423

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

4.10 完全正确性 448

4.11 最弱前置谓词和不确定性公理语义 461

4.12 类型理论和程序逻辑 474

4.13 模态逻辑和时序逻辑 492

4.14 支时序逻辑和线性时序逻辑 500

4.15 动态逻辑 516

第五章 代数语义 527

5.1 概述 527

5.2 ∑代数和初始语义 536

5.3 扩充的公理形式 549

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

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

5.6 理论描述语言Clear 584

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

5.8 终结语义 610

5.9 格语义 621

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

5.11 偏∑代数 648

5.12 模型描述语言ASL 666

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

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

第六章 并发和分布式程序的形式语义 700

6.1 概述 700

6.2 分布式程序设计语言CSP 716

6.3 CSP的结构化操作语义 727

6.4 CSP的流语义 740

6.5 TCSP和失败语义 749

6.6 并行程序的公理语义 761

6.7 CSP的公理语义 770

6.8 通信系统演算（CCS） 791

6.9 CCS的操作语义 797

6.10 同步树和通信树 806

6.11 双模拟和行为等价性 815

6.12 SCCS和集合推导语义 830

6.13 CCS的偏序推导语义 837

6.14 CCS的Petri网语义 851

6.15 分布式变迁系统和CCS 859

参考文献 872