软件开发的形式化工程方法

出版时间：2008-8  出版社：清华大学出版社  作者：刘少英  页数：408  
Tag标签：无  

前言

本书以简洁明了的语言介绍了软件开发技术的最新成果——形式化工程方法，并在精确而简单的概念描述和必要的数学定义基础之上，以大量浅显易懂的案例系统地阐述了一个具体的系统建模和功能描述语言SOFL(Structured Object-Oriented Formal Language)以及在此语言基础之上建立起来的并具有代表性的形式化工程方法，称为SOFL方法。。大家都知道，大型软件产品的开发是一个一般需要多数开发人员参加的复杂过程。它的主要环节有三个：理解、创造和确认。为了给用户提供满意而正确的软件产品，开发者首先必须正确和全面地理解用户的要求，包括功能要求。必要的数据资源。对功能与数据资源或系统行为的限制。在此基础之上，开发者必须通过系统的设计，构建软件系统的体系结构。数据结构和有效的算法，并以一定的编程语言实现其代码。这一系列的创造过程是不可能完全自动实现的，它必须依靠软件开发者来完成。然而，开发者是不能保证不出错的。实际上，大型软件系统的开发过程中一般都要出现大量的人为错误，经常造成软件产品的生产费用增大，不能按时交货，或不能保证质量。为此，完成的软件产品的质量必须得到严密的确认以后其产品才能送交用户使用。保证软件质量的一个很重要的要素就是软件开发方法。开发方法是不是实用有效，一般取决于它是否具备三个要素：简单。可视化和精确。也就是说，该方法必须用起来简单，其表现形式要有效地发挥图形语言的可视化效果，同时所表达的内容必须精确以确保其意思能被准确理解。传统的软件开发方法，像结构化和面向对象的开发方法，基本上都用自然语言或语义不明的图形语言来描述用户的需求和系统设计文档。由于自然语言表达结构和所用术语的意思不清楚所造成的二义性，使得软件文档经常被误解或被随意解释以造成大量严重的设计或实现上的错误。这种局面也严重地影响了切实有效的支撑工具的开发和建立。.。 上世纪七十年代以来，以Hoare逻辑和Dijkstra的最弱前置谓词演算为基础发展而来的形式化开发方法为严密地开发软件系统提供了理论基础和技术，为解决上述问题迈出了重要的一步。这些技术包括形式化规范说明书写作语言，逐步求精的开发方法，以及程序正确性证明技术。但遗憾的是，这些形式化技术只重视规范说明书的精确性和软件开发的严密性，而未能在简单可行和有效的可视化方面取得可喜的进展。恰恰相反，大型软件系统的形式化规范说明书往往复杂难懂，修改花费时间，出错的可能性很大。加之，逐步求精的开发方法和正确性证明技术都对开发人员的抽象和逻辑演算能力要求很高，使得这种技术很难被一般企业的软件开发者所接受。如何才能使严密性很高的形式化开发方法融合到传统的软件工程过程和技术中以提高和促进它们的严密性。有效性以及可控制性从而最终达到提高软件生产效率和软件质量的目的就成为一个意义重大的研究课题。形式化工程方法和SOFL方法就是在这种情况下从上世纪八十年代末逐渐形成并发展而来的。其目的就是建立起能把形式化开发方法有效地结合到传统的软件开发过程和方法中的技术，使得形式化方法能够更加简单地被一般软件开发者使用，发挥其高严密性的特长以促进传统软件开发技术的有效性和系统性，并使软件开发过程能得到更加有效的工具支撑。为建立有效的系统模型和确切的需求规范说明书，SOFL方法提供了具有简单。可视化和精确特点的形式化规范说明书语言和行之有效的建立形式化规范说明书的三步法。为有效地查出需求规范说明书中的错误，SOFL提供了严密的复审(review)和说明书测试技术。为有效地利用结构化和面向对象设计方法的各自优势，SOFL提供了把结构化和面向对象的设计方法有机结合的技术，使得结构化方法在需求分析和抽象设计方面发挥其优点以方便开发者和用户之间的交流和合作，而使面向对象方法在详细设计和编码方面发挥其特长以增强所开发系统的可维护性和重用性。它也提供了把结构化设计转化成面向对象的程序代码的方法和技术。为有效地发现程序中的错误，SOFL提供了基于形式化规范说明书的严密检查(inspection)和严密测试技术。虽然这最后两种查错技术没有包括在本书之内，但它们已形成SOFL方法的不可分割的部分。总而言之，SOFL是集结构化。面向对象和形式化方法于一身，并具有简单。可视化和精确的特点的形式化工程方法。它已被工业界和多数软件工程人员所使用，其效果正在引起更多软件工程师和研究者的兴趣和关注。本书的内容反映了作者在为提高软件开发质量以及开创严密有效和实用可行的形式化工程方法这个新技术领域近20年来的研究成果，并为进一步彻底的解决软件危机这个一直在困扰软件工程的重大难题，提出和阐述了“智能软件工程环境”这个未来软件工程的发展方向。作为本书的作者，在2008年第29届奥运会在北京召开之际，能将此书与国内读者见面，我感到由衷的欣慰，也很感谢清华大学出版社的极大热情和努力，帮助我实现了多年来想把形式化工程方法SOFL介绍给国内软件工程界的大学生。研究生。研究者以及工程技术人员的夙愿。我衷心希望读者能通过学习本书的内容享受到形式化工程方法的新思想，掌握其应用的系统技术，并提高开发高质量软件产品的技巧和能力，为自己的学习。就业。研究以及工作创造新的生机。

内容概要

本书首次开创了一个新技术，即形式化工程方法，把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法，其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和SOFL的迫切需求。　　本书通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE 2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、2、VDM和Larch等。本书可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。

作者简介

Shaoying Liu 教授，著名计算机专家，日本法政大学教授，上海交通大学和上海大学客座教授。早年在西安交通大学获得学士和硕士学位，后在英国曼彻斯特大学获得博士学位。现为IEEE计算机学会复杂性技术委员会副主席，IEEE计算机学会、ACM、日本软件科学与技术学会成员。多年来

书籍目录

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  Exercises2 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.11.1 Inference Rules　　2.11.2 Rules for Conjunction　  2.11.3 Rules for Disjunction　  2.11.4 Rules for Negation　  2.11.5 Rules for Implication　  2.11.6 Rules for Equivalence　  2.11.7 Properties of Propositional Expressions　2.12 Exercises3 Predicate Logic　3.1  Predicates　3.2  Quantifiers　　3.2.1  The Universal Quantifier　　3.2.2  The Existential Quantifier　  3.2.3  Quantified Expressions with Multiple Bound Variables　  3.2.4  Multiple Quantifiers　  3.2.5  de Morgan's Laws　3.3  Substitution　3.4  Proof in Predicate Logic　  3.4.1  Introduction and Elimination of Existential Quantifiers　  3.4.2  Introduction and Elimination of Universal Quantifiers  3.5  Validity and Satisfaction  3.6  Treatment of Partial Predicates  3.7 Formal Specification with Predicates  3.8  Exercises4 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.12.1 Starting Processes　  4.12.2 Starting Nodes　  4.12.3 Terminating Processes　  4.12.4 Terminating Nodes　  4.12.5 Enabling and Executing a CDFD　  4.12.6 Restriction on Parallel Processes　  4.12.7 Disconnected CDFDs　  4.12.8 External Processes  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.16.1 The if-then-else Expression　  4.16.2 The let Expression　  4.16.3 The case Expression　  4.16.4 Reference to Pre and Postconditions　4.17 Function Definitions　  4.17.1 Explicit and Implicit Specifications　  4.17.2 Recursive Functions　4.18 Exercises5 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  Exercises6 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 Exercises7  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  Exercises8  The Set Types  8.1  What Is a Set　8.2  Set Type Declaration　8.3 Constructors and Operators on Sets　  8.3.1  Constructors　  8.3.2  Operators　8.4  Specification with Set Types　8.5  Exercises9 The Sequence and String Types　9.1  What Is a Sequence　9.2  Sequence Type Declarations　9.3  Constructors and Operators on Sequences　 9.3.1  Constructors　 9.3.2  Operators　9.4  Specifications Using Sequences　 9.4.1  Input and Output Module　 9.4.2  Membership Management System  9.5  Exercises10 The Composite and Product Types　10.1 Composite Types　　10.1.1 Constructing a Composite Type　　10.1.2 Fields Inheritance　　10.1.3 Constructor　　10.1.4 Operators　　10.1.5 Comparison　10.2 Product Types　10.3 An Example of Specification  10.4 Exercises11 The Map Types　11.1 What Is a Map　11.2 The Type Constructor　11.3 Operators　　11.3.1 Constructors　　11.3.2 Operators  11.4 Specification Using a Map  11.5 Exercises12 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 Exercises13 Classes　13.1 Classes and Objects　　13.1.1 Class Definition　　13.1.2 Objects　　13.1.3 Identity of Objects　13.2 Reference and Access Control　13.3 The Reference of a Current Object　13.4 Inheritance　　13.4.1 What Is Inheritance　　13.4.2 Superclasses and Subclasses　　13.4.3 Constructor　　13.4.4 Method Overloading　　13.4.5 Method Overriding　　13.4.6 Garbage Collection　13.5 Polymorphism　13.6 Generic Classes　13.7 An Example of Class Hierarchy　13.8 Example of Using Objects in Modules　13.9 Exercises14 The Software Development Process　14.1 Software Process Using SOFL　14.2 Requirements Analysis　  14.2.1 The Informal Specification　  14.2.2 The Semi-formal Specification　14.3 Abstract Design　14.4 Evolution　14.5 Detailed Design　  14.5.1 Transformation from Implicit to Explicit Specifications　  14.5.2 Transformation from Structured to Object-Oriented　Specifications　14.6 Program　14.7 Validation and Verification　14.8 Adapting the Process to Specific Applications　14.9 Exercises15 Approaches to Constructing Specifications　15.1 The Top-Down Approach　  15.1.1 The CDFD-Module-First Strategy　  15.1.2 The CDFD-Hierarchy-First Strategy　  15.1.3 The Modules and Classes　15.2 The Middle-out Approach　15.3 Comparison of the Approaches　15.4 Exercises16 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 Exercises17 Rigorous Review　17.1 The Principle of Rigorous Review　17.2 Properties　　17.2.1 Internal Consistency of a Process　  17.2.2 Invariant-Conformance Consistency　  17.2.3 Satisfiability　  17.2.4 Internal Consistency of CDFD  17.3 Review Task Tree　  17.3.1 Review Task Tree Notation　  17.3.2 Minimal Cut Sets　  17.3.3 Review Evaluation  17.4 Property Review　  17.4.1 Review of Consistency Between Process and Invariant　  17.4.2 Process Consistency Review　  17.4.3 Review of Process Satisfiability　  17.4.4 Review of Internal Consistency of CDFD  17.5 Constructive and Critical Review  17.6 Important Points  17.7 Exercises18 Specification Testing  18.1 The Process of Testing  18.2 Unit Testing　  18.2.1 Process Testing　  18.2.2 Invariant Testing  18.3 Criteria for Test Case Generation  18.4 Integration Testing　  18.4.1 Testing Sequential Constructs　  18.4.2 Testing Conditional Constructs　  18.4.3 Testing Decompositions  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.3.1 Transformation of Single-Port Processes　  19.3.2 Transformation of Multiple-Port Processes　19.4 Transformation of CDFD　19.5 Exercises20 Intelligent Software Engineering Environment　20.1 Software Engineering Environment　20.2 Intelligent Software Engineering Environment　20.3 Ways to Build an ISEE　  20.3.1 Domain-Driven Approach　  20.3.2 Method-Driven Approach　  20.3.3 Combination of Both　20.4 ISEE and Formalization　20.5 ISEE for SOFL    20.5.1 Support for Requirements Analysis　  20.5.2 Support for Abstract Design　  20.5.3 Support for Refinement　  20.5.4 Support for Verification and Validation　  20.5.5 Support for Transformation　  20.5.6 Support for Program Testing　  20.5.7 Support for System Modification　  20.5.8 Support for Process Management　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.8.1 Compound Expressions　 　 A.8.2 Unary Expressions　 　 A.8.3 Binary Expressions　 　 A.8.4 Apply Expressions　 　 A.8.5 Basic Expressions　 　 A.8.6 Constants　 　 A.8.7 Simple Variables　 　 A.8.8 Special Keywords　　  A.8.9 Set Expressions　 　 A.8.10 Sequence Expressions　 　 A.8.11 Map Expressions　 　 A.8.12 Composite Expressions　 　 A.8.13 Product Expressions    A.9 Predicate Expressions　　  A.9.1 Boolean Variables　　  A.9.2 Relational Expressions　　  A.9.3 Conjunction　　  A.9.4 Disjunction　　  A.9.5 Implication　　  A.9.6 Equivalence　　  A.9.7 Negation　　  A.9.8 Quantified Expressions　　A.10 Identifiers　　　A. 11 Character　　　A. 12 CommentsIndex

章节摘录

插图：

媒体关注与评论

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. JonesUniversity of Newcastle upon TyneProbably the best coverage of any formal treatment I have seen. 　　--Peter Lindsay　　University of Queensland

编辑推荐

《国外经典教材•计算机科学与技术•软件开发的形式化工程方法:结构化+面向对象+形式化》可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。

用户评论 (总计10条)

•   刘老师说他的书网上电子文档有的是，不用买书，我想我们都是做学问的，还是买一本，学习也方便。刘老师工作严谨，不愧为日本法政大学知名教授。
•   我买这本书的时候恰巧本书的作者再给我们上课，老师建议我们买的，有老师上课再加上这本书做指导，学习效果非常好，老师讲课很认真，从老师身上可以看出一个学者应有的治学态度，不光是为了这个老师，书也写的很不错，语言浅显易懂，配套ppt和答案在老师的官网上都有提供下载，果断给高分。
•   全是英文。
•   很好很成功
•   很容易懂！
•   作者给我们上课用的，个人感觉用处不是太大，太专业了。
•   不记得买过这本书了，找不到了，我去。。。
•   正版图书，至于内容么，还可以看看。
•   非常有幸，听过刘少英老师的软件形式化方法的课，结合这本书进行学习，可以初步掌握软件形式化的方法，而且这本书所用的英文语言都比较简单，很好阅读，词汇不是很艰深，不过内容相当丰富
•   还没有来及看，是全英文的，我想看过中文的再看这个可能会效果更好一些