《实用程序设计理论》正文部分共分为12章，系统地介绍了一种程序设计理论，包括基本理论、基本数据结构、函数理论、程序理论、程序设计语言、递归定义、理论设计与实现、并发和交互等内容，《实用程序设计理论》的内容既系统、丰富、连贯，又非常精练，浅显易懂，另外，《实用程序设计理论》还附有400多道有趣的练习题（全部集中在第10章）。<br>    《实用程序设计理论》可作为高等院校计算机科学专业的高年级本科生和研究生程序理论课程的教材，也可作为对软件形式化方法有兴趣的研究人员和技术人员的参考书。

    本节解释了本书在选择和提供材料方面所作的一些取舍，只关心学习这些材料的学生可能对此不感兴趣，但教师和研究者也许会感兴趣。<br>    在标准的记号和新的完美的记号之间，我选择了标准的记号。例如，在表示两个数。x和y的最大值时，使用了函数max：max。y。x因为最大值是对称和结合的，所以可以引入一个更好的像T的对称符号作为中缀操作符：x，y我个人总是这样做，但在本书中我所选择的符号尽量保持数量少且符合传统。大多数人在看到maxz可时不需要预先作任何解释就会明白它的含义，但对x，y就不是这样。<br>    在选择操作符的优先次序时遵循两个准则：括号的使用量最少和容易记忆。后者可通过沿袭传统、将相关符号放在一起和使用尽可能少的优先级别来实现。这两个准则有时是相矛盾的，传统有时也是相矛盾的，并且以上帮助记忆的三个建议有时也是相矛盾的，最后我们必须作一个选择并一直使用它。额外的括号总是可以使用的，特别是在优先级结构不清晰时更应当使用。为了结构清晰，给v和v相同的优先级应该更好，但我还是保持了传统。本书采用的优先级比我预想的要多。

中译本序<br>第0章 绪言<br>0.0 引言<br>0.1 当前版本<br>0.2 快速浏览<br>0.3 致谢<br><br>第1章 基本理论<br>1.0 布尔理论<br>1.0.0 公理和证明规则<br>1.0.1 表达式和证明格式<br>1.0.2 单调性和反单调性<br>1.0.3 上下文<br>1.0.4 形式化<br>1.1 数论<br>1.2 字符理论<br><br>第2章 基本数据结构<br>2.0 束论<br>2.1 集合论<br>2.2 串论<br>2.3 表论<br>2.3.0多维结构<br><br>第3章 函数理论<br>3.0 函数<br>3.0.0 简化的函数记号<br>3.0.1 作用域和置换<br>3.1 量词<br>3.2 +函数若干点讨论<br>3.2.0函数包含和相等<br>3.2.1 高阶函数<br>3.2.2 函数组合<br>3.3 表作为函数<br>3.4 极限与实数<br><br>第4章 程序理论<br>4.0 规范<br>4.0.0 规范记号<br>4.0.1 规范定律<br>4.0.2 精化<br>4.0.3 条件<br>4.0.4 程序<br>4.1 程序开发<br>4.1.0精化定律<br>4.1.1 表求和<br>4.1.2 二的指数幂<br>4.2 时间<br>4.2.0真实时间<br>4.2.1 递归时间<br>4.2.2 终止问题<br>4.2.3 可靠性与完备性<br>4.2.4 线性查找<br>4.2.5 二分查找<br>4.2.6 快速指数运算<br>4.2.7 斐波那契数<br>4.3 空间<br>4.3.0 最大空间<br>4.3.1 平均空间<br><br>第5章 程序设计语言<br>5.0 作用域<br>5.0.0 变量说明<br>5.0.1 变量悬挂<br>5.1 数据结构<br>5.1.0 数组<br>5.1.1 记录<br>5.2 控制结构<br>5.2.0 while循环<br>5.2.1 包含退出的循环<br>5.2.2 二维查找<br>5.2.3 for循环<br>5.2.4 转向<br>5.3 时间与空间依赖<br>5.4 断言<br>5.4.0 检查<br>5.4.1 回溯<br>5.5.子程序<br>5.5.0 result表达式<br>5.5.1 函数<br>5.5.2 过程<br>5.6 别名<br>5.7 概率程序设计<br>5.7.0随机数产生器<br>5.7.1 信息<br>5.8 函数式程序设计<br>5.8.0 函数精化<br><br>第6章 递归定义<br>6.0 递归数据定义<br>6.0.0 构造和归纳<br>6.0.1 最小不动点<br>6.0.2 递归数据构造<br>6.1 递归程序定义<br>6.1.0 递归程序构造<br>6.1.1 循环定义<br><br>第7章 理论设计与实现<br>7.0 数据理论<br>7.0.0 数据-堆栈理论<br>7.0.1 数据-堆栈实现<br>7.0.2 简单数据-堆栈理论<br>7.0.3 数据-队列理论<br>7.0.4 数据-树理论<br>7.0.5 数据-树实现<br>7.1 程序理论<br>7.1.0 程肛堆栈理论<br>7.1.1.程序-堆栈实现<br>7.1.2 复杂程序堆栈理论<br>7.1.3 弱程肛堆栈理论<br>7.1.4 程序-队列理论<br>7.1.5 程序-树理论<br>7.2 数据转换<br>7.2.0 安全开关<br>7.2.1 取一个数<br>7.2.2 语法分析<br>7.2.3 有界队列<br>7.2.4 可靠性与完备性<br><br>第8章 并发<br>8.0 独立组合<br>8.0.0 独立组合定律<br>8.0.1 表并发<br>8.1 顺序到并行的转换<br>8.1.0 缓冲区<br>8.1.1 插入排序<br>8.1.2 哲学家就餐问题<br><br>第9章 交互<br>9.0 交互变量<br>9.0.0 自动调温器<br>9.0.1 空间<br>9.1 通信<br>9.1.0 实现性<br>9.1.1 输入和输出<br>9.1.2 通信计时<br>9.1.3 递归定义的通信<br>9.1.4 合并<br>9.1.5 监控器<br>9.1.6 反应控制器<br>9.1.7 信道声明<br>9.1.8 死锁<br>9.1.9 广播<br>……<br>第10章 练习<br>第11章 参考<br>译后记