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