第0章 绪言 1
0.0 引言 1
0.1 当前版本 2
0.2 快速浏览 2
0.3 致谢 3
第1章 基本理论 5
1.0 布尔理论 5
1.0.0 公理和证明规则 8
1.0.1 表达式和证明格式 9
1.0.2 单调性和反单调性 11
1.0.3 上下文 13
1.0.4 形式化 15
1.1 数论 16
1.2 字符理论 17
第2章 基本数据结构 18
2.0 束论 18
2.1 集合论 21
2.2 串论 22
2.3 表论 25
2.3.0 多维结构 28
第3章 函数理论 30
3.0 函数 30
3.0.0 简化的函数记号 32
3.0.1 作用域和置换 33
3.1 量词 34
3.2 函数若干点讨论 37
3.2.0 函数包含和相等 38
3.2.1 高阶函数 39
3.2.2 函数组合 39
3.3 表作为函数 41
3.4 极限与实数 42
第4章 程序理论 44
4.0 规范 44
4.0.0 规范记号 46
4.0.1 规范定律 48
4.0.2 精化 50
4.0.3 条件 50
4.0.4 程序 52
4.1 程序开发 54
4.1.0 精化定律 54
4.1.1 表求和 55
4.1.2 二的指数幂 57
4.2 时间 58
4.2.0 真实时间 58
4.2.1 递归时间 60
4.2.2 终止问题 63
4.2.3 可靠性与完备性 64
4.2.4 线性查找 65
4.2.5 二分查找 66
4.2.6 快速指数运算 72
4.2.7 斐波那契数 74
4.3 空间 78
4.3.0 最大空间 80
4.3.1 平均空间 81
第5章 程序设计语言 84
5.0 作用域 84
5.0.0 变量说明 84
5.0.1 变量悬挂 85
5.1 数据结构 86
5.1.0 数组 86
5.1.1 记录 88
5.2 控制结构 88
5.2.0 while循环 88
5.2.1 包含退出的循环 90
5.2.2 二维查找 92
5.2.3 for循环 94
5.2.4 转向 96
5.3 时间与空间依赖 97
5.4 断言 98
5.4.0 检查 98
5.4.1 回溯 98
5.5 子程序 99
5.5.0 result表达式 99
5.5.1 函数 100
5.5.2 过程 101
5.6 别名 102
5.7 概率程序设计 104
5.7.0 随机数产生器 107
5.7.1 信息 110
5.8 函数式程序设计 111
5.8.0 函数精化 113
第6章 递归定义 116
6.0 递归数据定义 116
6.0.0 构造和归纳 116
6.0.1 最小不动点 120
6.0.2 递归数据构造 121
6.1 递归程序定义 124
6.1.0 递归程序构造 124
6.1.1 循环定义 126
第7章 理论设计与实现 128
7.0 数据理论 128
7.0.0 数据-堆栈理论 128
7.0.1 数据-堆栈实现 129
7.0.2 简单数据-堆栈理论 130
7.0.3 数据-队列理论 131
7.0.4 数据-树理论 133
7.0.5 数据-树实现 133
7.1 程序理论 135
7.1.0 程序-堆栈理论 136
7.1.1 程序-堆栈实现 136
7.1.2 复杂程序-堆栈理论 136
7.1.3 弱程序-堆栈理论 137
7.1.4 程序-队列理论 137
7.1.5 程序-树理论 138
7.2 数据转换 139
7.2.0 安全开关 141
7.2.1 取一个数 142
7.2.2 语法分析 144
7.2.3 有界队列 146
7.2.4 可靠性与完备性 149
第8章 并发 150
8.0 独立组合 150
8.0.0 独立组合定律 152
8.0.1 表并发 153
8.1 顺序到并行的转换 154
8.1.0 缓冲区 155
8.1.1 插入排序 156
8.1.2 哲学家就餐问题 157
第9章 交互 160
9.0 交互变量 160
9.0.0 自动调温器 162
9.0.1 空间 163
9.1 通信 166
9.1.0 可实现性 167
9.1.1 输入和输出 168
9.1.2 通信计时 169
9.1.3 递归定义的通信 170
9.1.4 合并 171
9.1.5 监控器 172
9.1.6 反应控制器 173
9.1.7 信道声明 175
9.1.8 死锁 176
9.1.9 广播 178
第10章 练习 185
10.0 基本理论 185
10.1 基本数据结构 193
10.2 函数理论 196
10.3 程序理论 201
10.4 程序设计语言 219
10.5 递归定义 223
10.6 理论设计与实现 230
10.7 并发 237
10.8 交互 239
第11章 参考 245
11.0 释疑 245
11.0.0 记号 245
11.0.1 布尔理论 245
11.0.2 束论 246
11.0.3 串论 247
11.0.4 函数理论 248
11.0.5 程序理论 248
11.0.6 程序设计语言 250
11.0.7 递归定义 251
11.0.8 理论设计与实现 252
11.0.9 并发 252
11.0.10 交互 253
11.1 来源 253
11.2 参考文献 255
11.3 词语对照与索引 259
11.4 公理和定律 265
11.4.0 布尔 265
11.4.1 通用符号 269
11.4.2 数 270
11.4.3 束 271
11.4.4 集合 273
11.4.5 串 273
11.4.6 表 274
11.4.7 函数 274
11.4.8 量词 276
11.4.9 极限 280
11.4.10 规约与程序 280
11.4.11 置换 281
11.4.12 条件 281
11.4.13 精化 282
11.5 名字 282
11.6 符号 283
11.7 优先级 285
11.8 分配性 286
译后记 287