目 次 1
导论 1
0.1 本书的结构 1
0.2程序设计方法学发展回顾 3
第一部分程序逻辑基础 7
第一章程序规范与程序正确性 9
1.1断言与规范 9
1.2程序的执行状态 11
1.3数组的解释 13
1.4程序正确性证明梗概 14
练 习 17
第二章最弱前置谓词与程序语言￡的语义 18
2.1最弱前置谓词 18
2.2基本语句的定义 19
2.2.1 空语句 20
2.2.2赋值语句 20
2.2.3顺序复合 21
2.2.4 选择语句 21
2.2.5循环语句 22
*2.3多重赋值语句的定义 26
*2.4过程调用的定义 27
练 习 30
第三章程序设计基本方法 33
3.1面向目标的程序设计 34
3.2选择语句的设计 34
3.3循环程序的设计 35
3.4不变式构造 37
3.4.1 削弱ψ就ρ：删除合取分量 37
3.4.2削弱ψ就ρ：变量替换常量 37
3.4.3削弱ψ就ρ：扩大变量变化范围 38
3.4.4联合？与ψ就ρ 39
3.5界函数 39
*3.6略述大型程序之设计 40
练 习 42
第四章程序正确性验证：公理学方法 45
4.1程序正确性与部分正确性 45
4.2 Hoare系统 45
4.3“正向”证明和“反向”证明 47
*4.4协调性与完全性 49
*4.5关于“完全”正确性的证明系统 50
练习 51
*4.6 Hoare系统的扩充 51
第五章并行程序验证：时态逻辑方法 53
5.1 引言 53
5.2时态逻辑一般概念 54
5.2.1模态逻辑框架 55
5.2.2时态逻辑框架 56
5.2.3程序时态逻辑 57
5.2.4模型 58
5.3.1并行程序模型 60
5.2.5若干有效时态公式 60
5.3并行程序及其执行 60
5.3.2并行性及其交叉模拟 62
5.3.3信号灯 64
5.3.4公正性 65
5.4并行程序性质的时态描述 66
5.4.1不变性 68
5.4.2活动性 72
5.4.3优先性质 74
练 习 76
*第六章并行程序的时态证明系统 78
6.1时态逻辑系统 78
6.1.1时态命题逻辑 78
6.1.2时态谓词逻辑 82
6.1.3带等词的时态谓词逻辑 83
6.1.4框架公理和规则 84
6.2论域系统 85
6.3程序公理和推理规则 86
6.4.1分布计算最大公约数 88
6.4举例子 88
6.4.2信号灯 90
6.4.3互斥 91
6.5证明原理 92
6.5.1不变性原理 92
6.5.2活动性原理 93
6.5.3优先性质证明原理 96
练习 97
第一部分参考文献 97
第二部分模型规范与程序开发 99
7.1软件开发的形式化 101
第七章概论 101
7.2软件系统规范描述的一般原则 102
7.3模型抽象与多步开发过程 105
7.4偏函数逻辑 106
7.4.1 问题的背景 106
7.4.2偏函数逻辑的模型理论 106
7.4.3偏函数逻辑的证明理论 108
练 习 113
8.1.1 函数的规范 115
8.1运算的规范描述 115
第八章模型抽象与规范描述 115
8.1.2运算的规范 117
8.2结构归纳法与集合抽象 118
8.2.1结构归纳法 119
8.2.2集合表示及其推理 120
8.2.3规范描述举例 122
8.3模型规范：基于状态的数据类型 124
8.4结构类型、映射抽象及序列抽象 125
8.4.1结构类型与规范描述 125
8.4.2映射抽象与规范描述 129
8.4.3序列抽象与规范描述 132
8.5表示抽象的重要性：关于模型构造方法的一点讨论 134
练习 136
第九章模型具体化与程序开发 139
9.1数据类型的精化 139
9.1.1抽象函数与充分性 140
9.1.2数据精化的正确性 142
9.1.3数据精化的例 144
9.2模型的实现偏倾及讨论 146
9.3运算的分解 148
9.3.1分而治之与组装式开发方法 149
9.3.2关于运算分解的证明规则 149
9.3.3运算分解的例 150
练习 151
第二部分参考文献 151
第三部分大型程序设计 153
第十章大型程序设计与抽象数据类型 155
10.1大型程序设计概述 155
10.1.1大型程序的特点 155
10.1.3模块分解准则 156
10.1.2什么是大型程序设计 156
10.2数据抽象发展的背景与动机 157
10.3 Ada 中的数据抽象模块——程序包 161
10.3.1 程序包的基本特点 161
10.3.2程序包的三种模块形式 165
10.4类属程序包与抽象数据类型的参数化 170
10.5 Ada程序结构 173
练 习 176
11.1抽象数据类型的规范描述 178
第十一章抽象数据类型的形式规范描述 178
*11.2 Hoare公理方法 179
11.3代数公理方法 182
11.3.1 举例 183
11.3.2代数规范描述的形式定义 185
11.3.3 代数规范描述的设计 186
11.4代数规范描述的协调性与完全性 191
11.4.1协调性 191
11.4.2完全性 193
练习 194
12.1.1 ∑——代数 196
12.1代数与范畴 196
*第十二章代数规范描述的语义模型 196
12.1.2范畴与函子 199
12.2语义模型的选择 201
12.3初始代数语义 202
12.4终止代数语义 203
12.5关于语义模型的几点评注 204
12.6 正确性 205
12.7实现 207
12.7.1 直接实现 208
12.7.2非直接实现 211
12.8参数化规范描述及语义模型 213
练 习 216
第十三章大型程序的组装 218
13.1界面、实现、模块 219
*13.2 Pebble语言简介 224
13.2.1基本特征 225
13.2.2 相关类型 227
*13.3模块的组装 229
练 习 232
第三部分参考文献 232