第一章 引言 1
1．1 形式化方法 1
1．2 B语言的历史 9
1．3 B与其他形式化方法的关系 12
1．4 本章小结 15
第二章 B AMN基础 16
2．1 数学符号表示法 16
2．2 定义操作 22
2．3 抽象机 32
2．4 机器组成机制 48
2．5 细化 55
2．6 实现 65
2．7 本章小结 91
2．8 习题 92
第三章 分析和规格说明 95
3．1 需求分析 95
3．2 规格说明开发 96
3．3 动画 139
3．4 内部一致性法则的证明 141
3．5 船载实例研究-规格说明 142
3．6 重命名 150
3．7 聚集（aggregation） 150
3．8 本章小结 152
3．9 习题 153
第四章 设计和实现 159
4．1 分层开发范型 160
4．2 细化举例 165
4．3 细化的证明 186
4．4 分解实现 191
4．5 船载实例研究——实现 193
4．6 本章小结 204
4．7习题 204
第五章 实例研究 205
5．1 人事系统开发 205
5．2 矿井水泵控制 227
5．3 自动售货机 243
5．4 习题 259
第六章 结束语 260
附A．1 第2．8节习题解答 264
附录A 习题解答 264
附A．2 第3．9节习题解答 268
附A．3 第4．7节习题解答 274
附录B 最弱前置条件特性 279
附B．1 终止和可行性 281
附B．2 集合论的语义 283
附B．3 细化 285
附B．4 良好形式的法则 287
附B．5 正规形式 289
附B．6 操作符||的规则 290
附B．7 :=的定义 290
附录C 证明技术 292
参考文献 297
索引 303