第一部分 基本控制结构 2
第一章 有限状态模型 2
1.1 有限状态机 2
目录 11
前言 11
1.2 非确定的FSM 11
1.3 语言和正规表达式 16
1.4 正规表达式与FSM的等价性 20
1.5 计算模型“能力”的描述 25
1.6 文献概述 27
第二章 其它控制模型：框图和程序 39
2.1 框图 39
2.2 简单程序设计语言的控制结构 44
2.3 框图与程序的等价性 46
2.4 文献概述 48
第三章 其它控制结构 54
3.1 选择结构 55
3.2 重复结构 57
3.3 程式 59
3.5 文献概述 67
3.4 小结：等价性、能力和方便性 67
第四章 控制的表示 73
4.1 FCL/2结构的表示 74
4.2 其它控制结构的表示 76
4.3 程式的表示 78
4.4 文献概述 80
第五章 程序的形式描述与证明 88
5.1 程序的功能描述 89
5.2 程序证明 92
5.3 计算wp：语言的语义 93
5.4 正确性论证的脆弱性 116
5.5 确认：测试与验证 118
5.6 文献概述 119
第六章 计算效率的测定 130
6.1 两个简单例子 131
6.2 阶算法 135
6.3 效率信息的收集和应用 138
6.4 性能的实验测定 139
6.5 性能的分析测定 143
6.6 文献概述 157
7.1 引言 163
第七章 数据的数学模型 163
第二部分 基本数据结构 163
7.2 存贮器、变量、名字和值 164
7.3 类型 169
7.4 类型的描述 171
7.5 文献概述 177
第八章 程序设计语言中的数据 184
8.1 纯量类型 184
8.2 名字和引用 187
8.3 构造类型 193
8.4 程序设计语言中出现的与数据有关的其它问题 198
8.5 文献概述 205
第九章 抽象构造类型 214
9.1 线性结构 214
9.2 非线性结构 225
9.3 文献概述 233
第十章 数据的表示 242
10.1 数据的表示技术 243
10.2 栈的表示 253
10.3 双排队与排队的表示 254
10.4 树与图的表示 260
10.5 集合的表示 264
10.6 多维数组的表示 269
10.7 文献概述 276
第十一章 数据表示的正确性 291
11.1 一个例子：栈类型的证明 292
11.2 一般方法 298
11.3 间接引用赋值的最弱前置条件 300
11.4 文献概述 302
第十二章 空间要求 305
12.1 静态空间要求 305
12.2 动态空间要求 309
12.3 设计判定和表示权衡 311
12.4 文献概述 312
第三部分 控制与数据的相互作用 316
第十三章 计算模型和文法 316
13.1 下推自动机 317
13.2 图灵机 324
13.3 元语言和产生式 330
13.4 文献概述 341
第十四章 递归及其有关问题 350
14.1 动态数据类型 350
14.2 递归 351
14.3 递归的能力 354
14.4 分而治之 357
14.5 动态类型上的递归操作：遍历树 359
14.6 文献概述 366
第十五章 标识符的解释 371
15.1 标识符的作用域（续） 371
15.2 存贮作用期（续） 374
15.3 标识符与值的结合 377
15.4 文献概述 381
16.1 具有静态存贮管理的语言 388
第十六章 高级语言的运行时表示 388
16.2 “基于栈的”语言 390
16.3 外层寻址和层次显示表 391
16.4 数组的存贮分配 396
16.5 分程序结构 396
16.6 过程参数 397
16.7 参数机构 398
16.8 堆式存贮分配 400
16.9 文献概述 401
17.1 递归程序的证明 406
第十七章 有关递归的推理 406
17.2 结构归纳法 407
17.3 文献概述 409
第十八章 递归算法的分析 411
18.1 递归程序代价函数的例子 411
18.2 几个熟悉的数学递归关系 412
18.3 代价函数例子的解答 413
18.4 解答分而治之递归的一般规则 414
18.5 文献概述 415
19.1 背景 419
第十九 章在程序设计中使用FSM：一个例子 419
第四部分 实例研究 419
19.2 问题的提出 420
19.3 基于FSM的解答 422
19.4 用于解答的抽象程序 428
19.5 用于解答的具体程序 432
19.6 词法分析程序的正确性 441
19.7 词法分析程序的性能 447
第二十章 集合的快速实现：一个例子 455
20.1 背景 455
20.2 问题的提出 456
20.3 使用表与树的一种实现 458
20.4 SetofElts类型的使用 462
20.5 用于解答的程序 463
20.6 SetofElts类型的正确性 475
20.7 SetofElts类型的性能 479
20.8 表示的选择 483
第二十一章 生成程序：编写在集合上操作的循环 492
21.1 对集合元素操作的循环 492
21.2 用穿线树实现的一种解答 494
21.3 用于解答的程序 496
21.4 集合操作的再实现 498
第二十二章 公式处理：定义数据类型的一个练习 502
22.1 一些定义 502
22.2 Expression抽象类型 505
22.3 原问题的解答 507
22.4 表达式数据类型的实现 512
22.5 性能问题及其解答 513
22.6 小结 518
第二十三章 产生式系统和简化 522
23.1 产生式系统 523
23.2 用模式和替换式扩充Expression类型 528
23.3 简化程式 534
23.4 小结 536
参考文献 539
附录A 术语与记号 543
A.1 标准的数学与逻辑记号 543
A.2 离散数学中的标准定义 544
A.3 本书中引入的记号 545
附录B 评价程序的标准 548
B.1 引言 548
B.2 程序是由人读的 549
B.3 如何编写好程序？ 549
附录C 本书所用的程序设计语言 555
附录D 一台简单的计算机 557
D.1 存贮器 558
D.2 输入输出设备 559
D.3 中央处理机 559
D.4 指令集 560
附录E 第四部分程序的汇集 562
E.1 词法分析程序 562
E.2 SetofElts类型与SetGen类型 566
E.3 求导程序与简化程序 571
汉英名词索引 578