《形式语义学基础》求取 ⇩

目次1

前言1

1　基本概念1

1.1　为什么需要形式描述1

1.2　程序与数学3

1.3　语义描述的主要方法6

2　数学基础知识10

2.1　命题和谓词演算10

2.2　集合和关系12

2.3　函数15

2.4　结构归纳20

3　语法24

3.1　抽象语法24

3.2　基于抽象语法的语义定义31

3.3　抽象语法的数学基础33

4　λ演算38

4.1　非形式介绍38

4.2　λ表示法的形式定义41

4.3　β变换和Church-Rosser定理45

4.4　λ演算中的算术47

4.5　类型化的λ演算49

5　指称语义的基础53

5.1　概述53

5.2　静态语义54

5.3　动态语义的基础58

5.4　表达式的含义59

5.5　命令的含义64

5.6　Kernel的完整规范68

6.1　约定73

6　指称语义的深入讨论73

6.2　记录74

6.3　数组82

6.4　指针83

6.5　输入和输出84

6.6　分程序结构87

6.7　例程92

6.8　类和继承98

7　递归的数学101

7.1　递归定义的问题101

7.2　递归定义的解释105

7.3　迭代方法107

7.4　部分序集合109

7.5　最小不动点115

7.6　连续函数121

7.7　使用全函数126

8　不确定性和并行性129

8.1　不确定性129

8.2　并行性133

9.2　有关理论的概念137

9.1　概述137

9　公理语义137

9.3　实例：带类型的λ演算142

9.4　公理化程序设计语言144

9.5　对断言的深入考察146

9.6　前后断言语义的基础148

9.7　Kernel的前后断言语义150

9.8　最弱前条件的演算159

9.9　不确定性164

9.10　例程和递归165

9.11　断言指导下的程序构造过程176

10　语义定义的一致性193

10.1　两种方法的比较193

10.2　解释断言193

10.3　谓词语义197

10.4　一致性要求198

10.5　一致性证明201

11　代数规范的初始语义210

11.1　基本例子210

11.2　基调和基调代数212

11.3　规范和规范代数215

11.4　项代数和商项代数218

11.5　商项代数的性质220

11.6　抽象数据类型223

12　等词逻辑程序的说明语义227

12.1　基本知识227

12.2　等词逻辑程序229

12.3　模型理论231

12.4　程序的最小不动点表征236

参考文献237