全书正文部分共分为12章，系统地介绍了一种程序设计理论，包括基本理论、基本数据结构、函数理论、程序理论、程序设计语言、递归定义、理论设计与实现、并发和交互等内容。本书的内容既系统、丰富、连贯,又非常精练，浅显易懂。另外，本书还附有400多道有趣的练习题(全部集中在第10章)。
本书可作为高等院校计算机科学专业的高年级本科生和研究生程序理论课程的教材，也可作为对软件形式化方法有兴趣的研究人员和技术人员的参考书。
样章试读
目录
- 中译本序
第0章 绪言
0.0 引言
0.1 当前版本
0.2 快速浏览
0.3 致谢
第1章 基本理论
1.0 布尔理论
1.0.0 公理和证明规则
1.0.1 表达式和证明格式
1.0.2 单调性和反单调性
1.0.3 上下文
1.0.4 形式化
1.1 数论
1.2 字符理论
第2章 基本数据结构
2.0 束论
2.1* 集合论
2.2 串论
2.3 表论
2.3.0 多维结构
第3章 函数理论
3.0 函数
3.0.0 简化的函数记号
3.0.1 作用域和置换
3.1 量词
3.2* 函数若干点讨论
3.2.0 函数包含和相等
3.2.1 高阶函数
3.2.2 函数组合
3.3 表作为函数
3.4* 极限与实数
第4章 程序理论
4.0 规范
4.0.0 规范记号
4.0.1 规范定律
4.0.2 精化
4.0.3* 条件
4.0.4 程序
4.1 程序开发
4.1.0 精化定律
4.1.1 表求和
4.1.2 二的指数幂
4.2 时间
4.2.0 真实时间
4.2.1 递归时间
4.2.2 终止问题
4.2.3* 可靠性与完备性
4.2.4 线性查找
4.2.5 二分查找
4.2.6 快速指数运算
4.2.7 斐波那契数
4.3 空间
4.3.0 最大空间
4.3.1 平均空间
第5章 程序设计语言
5.0 作用域
5.0.0 变量说明
5.0.1 变量悬挂
5.1 数据结构
5.1.0 数组
5.1.1 记录
5.2 控制结构
5.2.0 while循环
5.2.1 包含退出的循环
5.2.2 二维查找
5.2.3 for循环
5.2.4 转向
5.3 时间与空间依赖
5.4* 断言
5.4.0 检查
5.4.1 回溯
5.5 子程序
5.5.0 result表达式
5.5.1 函数
5.5.2 过程
5.6* 别名
5.7* 概率程序设计
5.7.0 随机数产生器
5.7.1 信息
5.8* 函数式程序设计
5.8.0 函数精化
第6章 递归定义
6.0 递归数据定义
6.0.0 构造和归纳
6.0.1 最小不动点
6.0.2 递归数据构造
6.1 递归程序定义
6.1.0 递归程序构造
6.1.1 循环定义
第7章 理论设计与实现
7.0 数据理论
7.0.0 数据-堆栈理论
7.0.1 数据-堆栈实现
7.0.2 简单数据-堆栈理论
7.0.3 数据-队列理论
7.0.4 数据-树理论
7.0.5 数据-树实现
7.1 程序理论
7.1.0 程序-堆栈理论
7.1.1 程序-堆栈实现
7.1.2 复杂程序-堆栈理论
7.1.3 弱程序-堆栈理论
7.1.4 程序-队列理论
7.1.5 程序-树理论
7.2 数据转换
7.2.0 安全开关
7.2.1 取一个数
7.2.2 语法分析
7.2.3 有界队列
7.2.4* 可靠性与完备性
第8章 并发
8.0 独立组合
8.0.0 独立组合定律
8.0.1 表并发
8.1 顺序到并行的转换
8.1.0 缓冲区
8.1.1 插入排序
8.1.2 哲学家就餐问题
第9章 交互
9.0 交互变量
9.0.0 自动调温器
9.0.1 空间
9.1 通信
9.1.0 可实现性
9.1.1 输入和输出
9.1.2 通信计时
9.1.3* 递归定义的通信
9.1.4 合并
9.1.5 监控器
9.1.6 反应控制器
9.1.7 信道声明
9.1.8 死锁
9.1.9 广播
第10章 练习
10.0 基本理论
10.1 基本数据结构
10.2 函数理论
10.3 程序理论
10.4 程序设计语言
10.5 递归定义
10.6 理论设计与实现
10.7 并发
10.8 交互
第11章 参考
11.0 释疑
11.0.0 记号
11.0.1 布尔理论
11.0.2 束论
11.0.3 串论
11.0.4 函数理论
11.0.5 程序理论
11.0.6 程序设计语言
11.0.7 递归定义
11.0.8 理论设计与实现
11.0.9 并发
11.0.10 交互
11.1 来源
11.2 参考文献
11.3 词语对照与索引
11.4 公理和定律
11.4.0 布尔
11.4.1 通用符号
11.4.2 数
11.4.3 束
11.4.4 集合
11.4.5 串
11.4.6 表
11.4.7 函数
11.4.8 量词
11.4.9 极限
11.4.10 规约与程序
11.4.11 置换
11.4.12 条件
11.4.13 精化
11.5 名字
11.6 符号
11.7 优先级
11.8 分配性
译后记
京公网安备 11010102004214号