《形式语义学基础与形式说明》

目 录1

第一章引论1

1.1．形式语义学1

1.2．指称语义学4

1.3．代数语义学6

1.4．操作语义学7

1.5．公理语义方法8

1.6．形式说明语言8

第二章指称语义学基础9

2.1．论域问题引子9

2.2． 域的构造12

2.3． 偏序与完全偏序14

2.4． 单调函数与连续函数18

2.5． 连续泛函21

2.6．泛函不动点及递归程序27

2.7．λ－抽象及λ－演算46

2.8．指称语义定义初步53

习 题59

参考文献63

第三章程序设计语言的指称语义64

3.1．程序设计语言的基本概念64

3.2． 存贮语义71

3.3． 环境（声明）语义77

3.4． 命令语义85

3.5．表达式语义89

3.6． 连续（Continuations）93

3.7．证明技术111

3.8． 小结120

习 题121

参考文献123

第四章指称语义的一些例子124

4.1．例子1124

4.2．例子2135

4.3． 例子3142

4.4． 例子4148

习 题154

参考文献155

第五章代数语义学基础156

5.1．概述156

5.2． 范畴论159

5.3．图范畴及图文法197

5.4．类别代数理论243

5.5．抽象数据类型265

5.6．等式理论与项重写系统274

5.7． 实例292

习题312

参考文献322

6.1．操作语义概述323

第六章操作语义学与属性文法323

6.2．施用表达式（AE）的机器计算328

6.3．属性文法概述339

6.4．属性文法分类346

6.5．用属性文法进行编译程序设计374

6.6．属性文法定义语言387

6.7．实例：AGDL的语法392

习题394

参考文献394

第七章组合逻辑395

7.1．概述395

7.2． 组合子402

7.3．组合逻辑的语法理论411

7.4．组合逻辑的逻辑基础421

7.5．函数性基本理论426

7.6．范畴组合逻辑432

7.7．小结439

习题440

参考文献442

第八章公理语义方法443

8.1． 概述443

8.2． 程序正确性验证的基本概念445

8.3．程序正确性验证技术451

8.4．Hoare公理系统464

8.5．Dijkst ra的最弱前置条件471

8.6．Martin-L？f类型论480

习题510

参考文献511

第九章维也纳发展方法：Meta-Language512

9.1．概况512

9.2．在VDM中的逻辑注释521

9.3．抽象数据类型522

9.4．抽象文法536

9.5． 组合算子538

9.6．VDM与程序设计语言550

参考文献570

习 题570

第十章并发程序设计语言的语义与说明571

10.1．并行系统概述571

10.2．并发程序设计语言概述573

10.3．幂域及不确定性580

10.4．通讯顺序进程（CSP）595

10.5． 并发程序设计语言的指称语义610

10.6．通讯顺序进程的操作语义626

10.7．进程与通讯网络的抽象数据类型640

10.8．并发程序设计语言的公理语义659

习题679

参考文献681