本书是关于程序设计方法学方面新的关键基础课题的最新技术水平的综述，汇集了国际上一流的计算机科学家、程序设计人员和软件系统设计人员研究出的宝贵资料。本书是先进的软件理论和实践方面的权威性指导书，适合计算机科学家、开发人员、程序设计人员和软件工程师作为参考。

本书重点介绍新的和正在出现的构造先进应用程序的技术，解决软件设计人员开发高度复杂的应用程序时必须要面临的问题。本书的主要内容包括：模型与正确性、程序设计技术以及应用和自动机理论。同时，给出了几个来自不同领域的应用实例，例如，安全、电话和电路设计等。

本书是先进的计算机软件理论和实践方面的权威性指导书，适合作为计算机科学家、程序设计人员和软件工程师的参考书。

撰稿者名单

译者序

前言

第一部分　模型与正确性

Section A　并行与交互

第1章　需要：并行性的组构方法

 1.1 组构性

 1.2　并发性的本质是干扰

 1.3　推理干扰

 1.4　关于假设/承诺推理的一些问题

 1.5　寄生变量的作用

 1.6　粒度所关心的事情

 1.7　抽象的原子性及其精化

 1.8　结论

 1.9　致谢

 参考文献

第2章　用契约强制行为

 2.1 引言

 2.2　契约

2.2.1　状态与状态变化

2.2.2　契约

2.2.3 操作语义

2.2.4　契约举例

2.2.5　行动系统

2.2.6　行动系统举例

 2.3　利用契约达到目标

2.3.1　最弱的前置条件

2.3.2　正确性与成功策略

2.3.3　契约的精化

 2.4　强制行为属性

2.4.1 分析行为

2.4.2　构造解释程序

　　……

第二部分　程序设计技术

第三部分　应用和自动机理论