本书以简洁明了的语言介绍了软件开发技术的最新成果——形式化工程方法，并在精确而简单的概念描述和必要的数学定义基础之上，以大量浅显易懂的案例系统地阐述了一个具体的系统建模和功能描述语言SOFL（Structured Object-Oriented Formal Language）以及在此语言基础之上建立起来的并具有代表性的形式化工程方法，即SOFL方法。

全书共20章，分别为Introduction，Propositional Logic，Predicate Logic，The Module，Hierarchical CDFDs and Modules，Explicit Specifications，Basic Data Types，The Set Types，The Sequence and String Types，The Composite and Product Types，The Map Types，The Union Types，Classes，The Software Development Process，Approaches to Constructing Specifications，A Case Study-Modeling an ATM，Rigorous Review，Specification Testing，Transformation from Designs to Programs，Intelligent Software Engineering Environment。

本书首次开创了一个新技术，即形式化工程方法，把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法，其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和SOFL的迫切需求。

本书通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE 2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、Z、VDM和Larch等。本书可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。

1 Introduction

  1.1 Software Life Cycle

  1.2 The Problem

  1.3 Formal Methods

 1.3.1 What Are Formal Methods

 1.3.2 Some Commonly Used Formal Methods

 1.3.3 Challenges to Formal Methods

  1.4 Formal Engineering Methods

  1.5 What Is SOFL

  1.6 A Little History of SOFL

  1.7 Comparison with Related Work

  1.8 Exercises

2 Propositional Logic

3 Predicate Logic

4 The Module

5 Hierarchical CDFDs and Modules

6 Explicit Specifications

7 Basic Data Types

8 The Set Types

9 The Sequence and String Types

10 The Composite and Product Types

11 The Map Types

12 The Union Types

13 Classes

14 The Software Development Process

15 Approaches to Constructing Specifications

16 A Case Study-Modeling an ATM

17 Rigorous Review

18 Specification Testing

19 Transformation from Designs to Programs

20 Intelligent Software Engineering Environment

References

Index