基本信息出版社：清华大学出版社
页码：403 页
出版日期：2008年08月
ISBN：7302183171/9787302183174
条形码：9787302183174
版本：第1版
装帧：平装
开本：16
正文语种：英语
丛书名：国外经典教材/计算机科学与技术
内容简介 《软件开发的形式化工程方法》首次开创了一个新技术，即形式化工程方法，把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法，其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和SOFL的迫切需求。.
《软件开发的形式化工程方法》通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE 2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、Z、VDM、Larch等。
《软件开发的形式化工程方法》可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。..
在软件开发领域，形式化方法涉及数学符号和微积分的使用，此类方法很难应用到面临着具体局限的大型系统中，这些局限包括开发者技能有限、时间和财务预算限制以及不断变化的需求。针对这些现状，书中介绍了形式化方法，提倡在软件工程过程中采用数学符号，从而从根本上增强行业中常用开发方法的准确性、全面性和有效性。
《软件开发的形式化工程方法》对SOFL (Structured Object-Oriented Formal Language)方法进行了介绍，此方法由作者设计并已经通过行业验证。《软件开发的形式化工程方法》包含大量练习和重要的实际案例，有助于读者迅速理解并成功将这种方法运用于项目之中。
作者简介 刘少英教授 著名计算机专家，日本法政大学教授，上海交通大学、上海大学客座教授。早年在西安交通大学获得学士和硕士学位，后在英国曼彻斯特大学获得博士学位。现为IEEE计算机学会复杂性技术委员会副主席，IEEE计算机学会、ACM、日本软件科学与技术学会成员。多年来，在计算机科学的许多领域，包括形式化方法及理论、软件开发方法学、软件检查、软件测试、可靠复杂计算机系统以及智能软件工程环境等方面做出了重要贡献。目前在著名国际杂志及会议发表学术论文80多篇，出版研究专著4部。
媒体推荐 Such books are to be whole-heartedly welcomed because they are written with an acute understanding of the issues for designers of useful software.
--Cliff B. Jones
University of Newcastle upon Tyne
Probably the best coverage of any formal treatment I have seen.
--Peter Lindsay
University of Queensland
编辑推荐 唯一论述软件形式化方法与现有软件工程完美结合的英文教材，旨在增强现有软件开发技术的严密性，系统性，有效性以及工具的可支撑性，适合高年级本科生、研究生使用。
目录
1 Introduction .
1.1 Software Life Cycle
1.2 The Problem
1.3 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
2.1 Propositions
2.2 Operators
2.3 Conjunction
2.4 Disjunction
2.5 Negation
2.6 Implication
2.7 Equivalence
2.8 Tautology, Contradiction, and Contingency
2.9 Normal Forms
2.10 Sequent
2.11 Proof
2.12 Exercises
3 Predicate Logic
3.1 Predicates
3.2 Quantifiers
3.3 Substitution
3.4 Proof in Predicate Logic
3.5 Validity and Satisfaction
3.6 Treatment of Partial Predicates
3.7 Formal Specifcation with Predicates
3.8 Exercises
4 The Module
4.1 Module for Abstraction
4.2 Condition Data Flow Diagrams
4.3 Processes
4.4 Data Flows
4.5 Data Stores
4.6 Convention for Names
4.7 Conditional Structures
4.8 Merging and Separating Structures
4.9 Diverging Structures
4.10 Renaming Structure
4.11 Connecting Structures
4.12 Important Issues on CDFDs
4.13 Associating CDFD with a Module
4.14 How to Write Comments
4.15 A Module for the ATM
4.16 Compound Expressions
4.17 Function Definitions
4.18 Exercises
5 Hierarchical CDFDs and Modules
5.1 Process Decomposition
5.2 Handling Stores in Decomposition
5.3 Input and Output Data Flows
5.4 The Correctness of Decomposition
5.5 Scope
5.6 Exercises
6 Explicit Specifications
6.1 The Structure of an Explicit Specification
6.2 Assignment Statement
6.3 Sequential Statements
6.4 Conditional Statements
6.5 Multiple Choice Statements
6.6 The Block Statement
6.7 The While Statement
6.8 Method Invocation
6.9 Input and Output Statements
6.10 Example
6.11 Exercises
7 Basic Data Types
7.1 The Numeric Types
7.2 The Character Type
7.3 The Enumeration Types
7.4 The Boolean Type
7.5 An Example
7.6 Exercises
8 The Set Types
8.1 What Is a Set
8.2 Set Type Declaration
8.3 Constructors and Operators on Sets
8.4 Specification with Set Types
8.5 Exercises ..
9 The Sequence and String Types
9.1 What Is a Sequence
9.2 Sequence Type Declarations
9.3 Constructors and Operators on Sequences
9.4 Specifications Using Sequences
9.5 Exercises
10 The Composite and Product Types
10.1 Composite Types
10.2 Product Types
10.3 An Example of Specification
10.4 Exercises
11 The Map Types
11.1 What Is a Map
11.2 The Type Constructor
11.3 Operators
11.4 Specification Using a Map
11.5 Exercises
12 The union Types
12.1 union Type Declaration
12.2 A Special union Type
12.3 Is Function
12.4 A Specification with a union Type
12.5 Exercises
13 Classes
13.1 Classes and Objects
13.2 Reference and Access Control
13.3 The Reference of a Current Object
13.4 Inheritance
13.5 Polymorphism
13.6 Generic Classes
13.7 An Example of Class Hierarchy
13.8 Example of Using Objects in Modules
13.9 Exercises
14 The Software Development Process
14.1 Software Process Using SOFL
14.2 Requirements Analysis
14.3 Abstract Design
14.4 Evolution
14.5 Detailed Design
14.6 Program
14.7 Validation and Verification
14.8 Adapting the Process to Specific Applications
14.9 Exercises
15 Approaches to Constructing Specifications
15.1 The Top-Down Approach
15.2 The Middle-out Approach
15.3 Comparison of the Approaches
15.4 Exercises
16 A Case Study-Modeling an ATM
16.1 Informal User Requirements Specification
16.2 Semi-formal Functional Specification
16.3 Formal Abstract Design Specification
16.4 Formal Detailed Design Specification
16.5 Summary
16.6 Exercises
17 Rigorous Review
17.1 The Principle of Rigorous Review
17.2 Properties
17.3 Review Task Tree
17.4 Property Review
17.5 Constructive and Critical Review
17.6 Important Points
17.7 Exercises
18 Specification Testing
18.1 The Process of Testing
18.2 Unit Testing
18.3 Criteria for Test Case Generation
18.4 Integration Testing
18.5 Exercises
19 Transformation from Designs to Programs
19.1 Transformation of Data Types
19.2 Transformation of Modules and Classes
19.3 Transformation of Processes
19.4 Transformation of CDFD
19.5 Exercises
20 Intelligent Software Engineering Environment
20.1 Software Engineering Environment
20.2 Intelligent Software Engineering Environment
20.3 Ways to Build an ISEE
20.4 ISEE and Formalization
20.5 ISEE for SOFL
20.6 Exercises
References
A Syntax of SOFL
A.1 Specifications
A.2 Modules
A.3 Processes
A.4 Functions
A.5 Classes
A.6 Types
A.7 Expressions
A.8 Ordinary Expressions
A.9 Predicate Expressions
A.10 Identifiers
A.11 Character
A.12 Comments
Index
……
序言 本书以简洁明了的语言介绍了软件开发技术的最新成果——形式化工程方法，并在精确而简单的概念描述和必要的数学定义基础之上，以大量浅显易懂的案例系统地阐述了一个具体的系统建模和功能描述语言SOFL(Structured Object-Oriented Formal Language)以及在此语言基础之上建立起来的并具有代表性的形式化工程方法，称为SOFL方法。。
大家都知道，大型软件产品的开发是一个一般需要多数开发人员参加的复杂过程。它的主要环节有三个：理解、创造和确认。为了给用户提供满意而正确的软件产品，开发者首先必须正确和全面地理解用户的要求，包括功能要求。必要的数据资源。对功能与数据资源或系统行为的限制。在此基础之上，开发者必须通过系统的设计，构建软件系统的体系结构。数据结构和有效的算法，并以一定的编程语言实现其代码。这一系列的创造过程是不可能完全自动实现的，它必须依靠软件开发者来完成。然而，开发者是不能保证不出错的。实际上，大型软件系统的开发过程中一般都要出现大量的人为错误，经常造成软件产品的生产费用增大，不能按时交货，或不能保证质量。为此，完成的软件产品的质量必须得到严密的确认以后其产品才能送交用户使用。
保证软件质量的一个很重要的要素就是软件开发方法。开发方法是不是实用有效，一般取决于它是否具备三个要素：简单。可视化和精确。也就是说，该方法必须用起来简单，其表现形式要有效地发挥图形语言的可视化效果，同时所表达的内容必须精确以确保其意思能被准确理解。传统的软件开发方法，像结构化和面向对象的开发方法，基本上都用自然语言或语义不明的图形语言来描述用户的需求和系统设计文档。由于自然语言表达结构和所用术语的意思不清楚所造成的二义性，使得软件文档经常被误解或被随意解释以造成大量严重的设计或实现上的错误。这种局面也严重地影响了切实有效的支撑工具的开发和建立。.。
上世纪七十年代以来，以Hoare逻辑和Dijkstra的最弱前置谓词演算为基础发展而来的形式化开发方法为严密地开发软件系统提供了理论基础和技术，为解决上述问题迈出了重要的一步。这些技术包括形式化规范说明书写作语言，逐步求精的开发方法，以及程序正确性证明技术。但遗憾的是，这些形式化技术只重视规范说明书的精确性和软件开发的严密性，而未能在简单可行和有效的可视化方面取得可喜的进展。恰恰相反，大型软件系统的形式化规范说明书往往复杂难懂，修改花费时间，出错的可能性很大。加之，逐步求精的开发方法和正确性证明技术都对开发人员的抽象和逻辑演算能力要求很高，使得这种技术很难被一般企业的软件开发者所接受。如何才能使严密性很高的形式化开发方法融合到传统的软件工程过程和技术中以提高和促进它们的严密性。有效性以及可控制性从而最终达到提高软件生产效率和软件质量的目的就成为一个意义重大的研究课题。
形式化工程方法和SOFL方法就是在这种情况下从上世纪八十年代末逐渐形成并发展而来的。其目的就是建立起能把形式化开发方法有效地结合到传统的软件开发过程和方法中的技术，使得形式化方法能够更加简单地被一般软件开发者使用，发挥其高严密性的特长以促进传统软件开发技术的有效性和系统性，并使软件开发过程能得到更加有效的工具支撑。为建立有效的系统模型和确切的需求规范说明书，SOFL方法提供了具有简单。可视化和精确特点的形式化规范说明书语言和行之有效的建立形式化规范说明书的三步法。为有效地查出需求规范说明书中的错误，SOFL提供了严密的复审(review)和说明书测试技术。为有效地利用结构化和面向对象设计方法的各自优势，SOFL提供了把结构化和面向对象的设计方法有机结合的技术，使得结构化方法在需求分析和抽象设计方面发挥其优点以方便开发者和用户之间的交流和合作，而使面向对象方法在详细设计和编码方面发挥其特长以增强所开发系统的可维护性和重用性。它也提供了把结构化设计转化成面向对象的程序代码的方法和技术。为有效地发现程序中的错误，SOFL提供了基于形式化规范说明书的严密检查(inspection)和严密测试技术。虽然这最后两种查错技术没有包括在本书之内，但它们已形成SOFL方法的不可分割的部分。总而言之，SOFL是集结构化。面向对象和形式化方法于一身，并具有简单。可视化和精确的特点的形式化工程方法。它已被工业界和多数软件工程人员所使用，其效果正在引起更多软件工程师和研究者的兴趣和关注。
本书的内容反映了作者在为提高软件开发质量以及开创严密有效和实用可行的形式化工程方法这个新技术领域近20年来的研究成果，并为进一步彻底的解决软件危机这个一直在困扰软件工程的重大难题，提出和阐述了“智能软件工程环境”这个未来软件工程的发展方向。作为本书的作者，在2008年第29届奥运会在北京召开之际，能将此书与国内读者见面，我感到由衷的欣慰，也很感谢清华大学出版社的极大热情和努力，帮助我实现了多年来想把形式化工程方法SOFL介绍给国内软件工程界的大学生。研究生。研究者以及工程技术人员的夙愿。我衷心希望读者能通过学习本书的内容享受到形式化工程方法的新思想，掌握其应用的系统技术，并提高开发高质量软件产品的技巧和能力，为自己的学习。就业。研究以及工作创造新的生机。
文摘 插图：
