形式语义学基础PDF电子书下载

目次 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