B方法

.1．3．6 若干证明
1．3．7 扩充的证明过程
1．3．8 存在量化公式
1．3．9 一些经典结果
1．4 等式
1．5 有序对
1．6 练习
第2章 集合形式
2．1 基本集合结构
2．1．1 语法
2．1．2 公理
2．1．3 性质
2．2 类型检查
2．3 派生结构
2．3．1 定义
2．3．2 实例
2．3．3 类型检查
2．3．4 性质
2．4 二元关系
2．4．1 二元关系结构：第一组
2．4．2 二元关系结构：第二组
2．4．3 二元关系结构的实例
2．4．4 二元关系结构的类型检查
2．5 函数
2．5．1 函数构造：第一组
2．5．2 函数构造：第二组
2．5．3 函数构造的示例
2．5．4 函数求值的性质
2．5．5 函数构造的类型检查
2．6 分类的性质
2．6．1 有关成员关系的法则
2．6．2 单调性法则
2．6．3 包含法则
2．6．4 相等法则
2．7 例子
2．8 练习
参考文献
第3章 数学对象
3．1 广义的交和并
3．2 构造数学对象
3．2．1 非形式的引言
3．2．2 不动点
3．2．3 归纳原理
3．3 一个集合的有穷子集的集合
3．4 有穷集合和无穷集合
3．5 自然数
3．5．1 定义
3．5．2 皮阿诺"公理"
3．5．3 最小值
3．5．4 强归纳原理
3．5．5 最大值
3．5．6 自然数上的递归函数
3．5．7 算术
3．5．8 关系的迭代
3．5．9 有穷集的势
3．5．10 关系的传递闭包
3．6 整数
3．7 有穷序列
3．7．1 归纳构造
3．7．2 直接构造
3．7．3 序列上的运算
3．7．4 排序及相关问题
3．7．5 整数序列的字典序
3．8 有穷树
3．8．1 非形式的介绍
3．8．2 形式化构造
3．8．3 归纳
3．8．4 递归
3．8．5 运算
3．8．6 树的表达
3．9 标记树
3．9．1 直接定义
3．9．2 归纳定义
3．9．3 归纳
3．9．4 递归
3．9．5 递归定义的运算
3．9．6 直接定义的运算
3．10 二叉树
3．10．1 直接的运算
3．10．2 归纳
3．10．3 递归
3．10．4 递归定义的运算
3．11 良构关系
3．11．1 定义
3．11．2 在良构集上通过归纳进行证明
3．11．3 在良构集上的递归
3．11．4 良构性的证明
3．11．5 一个良构关系实例
3．11．6 非经典递归的其他实例
3．12 练习
第二部分 抽 象 机
第4章 抽象机引论
4．1 抽象机
4．2 静态行为--描述状态
4．3 动态行为--描述操作
4．4 将前-后谓词作为规范
4．5 证明义务
4．6 代换作为规范
4．7 前条件代换(终止性)
4．8 参数化和初始化
4．9 带有输人参数的操作
4．10 带有输出参数的操作
4．11 规范的宽松风格和防御风格
4．12 多重简单代换
4．13 条件代换
4．14 约束选择代换
4．15 卫式代换(可行性)
4．16 没有任何作用的代换
4．17 上下文信息--集合和常量
4．18 无约束选择代换
4．19 显式定义
4．20 断言
4．21 具体变量和抽象常量
4．22 练习
参考文献
第5章 抽象机的定义
5．1 广义代换
5．1．1 语法
5．1．2 类型检查
5．1．3 公理
5．2 抽象机
5．2．1 语法
5．2．2 可见性规则
5．2．3 类型检查
5．2．4 关于常量
5．2．5 证明义务
5．2．6 关于给定集合和预定义常量
参考文献
第6章 抽象机理论
6．1 规范型
6．2 两个有用的性质
6．3 终止性、可行性和前-后谓词
6．3．1 终止性
6．3．2 可行性
6．3．3 前-后谓词
6．4 集合论模型
6．4．1 第一个模型--一个集合和一个关系
6．4．2 第二个模型--集合变换器
6．4．3 各种结构的集合论解释
6．5 练习
第7章 大型抽象机
7．1 多重广义代换
7．1．1 定义
7．1．2 基本性质
7．1．3 主要结果
7．2 规范的递增描述
7．2．1 非形式的介绍
7．2．2 操作调用
7．2．3 includes子句
7．2．4 可见性规则
7．2．5 传递性
7．2．6 机器的重命名
7．2．7 promotes和extends子句
7．2．8 实例
7．3 递增的规范描述和规范共享
7．3．1 非形式的介绍
7．3．2 uses子句
7．3．3 可见性规则
7．3．4 传递性
7．3．5 机器重命名
7．4 形式定义
7．4．1 语法
7．4．2 类型检查
7．4．3 includes子句的证明义务
7．4．4 uses子句的证明义务
7．5 练习
第8章 抽象机的实例
8．1 一个货单系统
8．1．1 非形式的规范
8．1．2 机器client
8．1．3 机器product
8．1．4 机器invoice
8．1．5 机器invoice_system
8．2 电话交换机
8．2．1 非形式的规范
8．2．2 机器simple_exchange
8．2．3 机器exchsnee
8．3 电梯控制系统
8．3．1 非形式的规范
8．3．2 机器lift
8．3．3 活性(liveness)的证明
8．3．4 活性证明义务的表述
8．4 练习
参考文献
第三部分 程序设计
第9章 顺序和循环
9．1 顺序
9．1．1 语法
9．1．2 公理
9．1．3 基本性质
9．2 循环
9．2．1 引论
9．2．2 定义
9．2．3 循环终止的解释
9．2．4 循环的前-后关系的解释
9．2．5 循环终止的实例
9．2．6 不变式定理
9．2．7 变动量定理
9．2．8 变动量和不变式定理的进一步实用化
9．2．9 传统循环
9．3 练习
第10章 程序设计实例
10．0 方法学
10．6 练习
参考文献
第四部分 精 化
第11章 精化
11．1 广义代换的精化
11．1．1 非形式的讨论
11．1．2 形式定义
11．1．3 广义代换的相等
11．1．4 单调性
11．1．5 广义赋值的精化
11．2 抽象机的精化
11．2．1 非形式的讨论
11．2．2 形式定义
11．2．3 充分条件
11．2．4 单调性
11．2．5 实例重温
11．2．6 最后的润色
11．2．7 精化条件的直观解释
11．2．8 对小例子的应用
11．3 形式定义
11．3．1 语法
11．3．2 类型检查
11．3．3 证明义务
11．4 练习
参考文献
第12章 构造大型抽象机
12．1 精化的实现
12．1．1 引言
12．1．2 有关引入的实际考虑
12．1．3 implementation结构
12．1．4 imports子句
12．1．5 可见性规则
12．1．6 机器重命名
12．1．7 values子句
12．1．8 imports和includes子句的比较
12．1．9 promotes和extends子句
12．1．10 再论具体常量和具体变量
12．1．11 在实现中允许出现的各种结构
12．2 共享
12．2．1 引言
12．2．2 sees子句
12．2．3 可见性
12．2．4 传递性和循环定义
12．2．5 机器重命名
12．2．6 uses子句和sees子句的比较
12．3 再论循环结构
12．4 多重精化和实现
12．5 递归定义的操作
12．5．1 引言
12．5．2 语法
12．5．3 证明规则
12．6 形式证明
12．6．1 一个implementation的语法
12．6．2 对imports子句的类型检查
12．6．3 对sees子句的类型检查
12．6．4 一个implementation的证明义务
12．6．5 对sees子句的证明义务
第13章 精化的实例
13．1 一个基本机器库
13．1．1 机器basic_constants
13．1．2 机器basic_io
13．1．3 机器basic_bool
13．1．4 机器basic_enum
13．1．5 机器basic_file_var
13．2 实例研究：数据库系统
13．2．1 有关文件的机器
13．2．2 有关对象的机器
13．2．3 一个数据库
13．2．4 界面
13．3 一个实用的抽象机库
13．3．1 机器array_var
13．3．2 机器sequence_var
13．3．3 机器set_var
13．3．4 机器array_ection
13．3．5 机器sequence_collection
13．3．6 机器set_echon
13．3．7 机器tree_var
13．4 实例研究：锅炉控制系统
13．4．1 引言
13．4．2 非形式的规范
13．4．3 系统分析
13．4．4 系统集成
13．4．5 形式化规范和设计
13．4．6 最后的体系结构
13．4．7 修改初始规范
参考文献
附 录
附录a 记法综述
附录b 语法
附录c 定义
附录d 可见性规则
附录e 规则和公理
附录f 证明义务