软件开发的形式化工程方法：结构化+面向对象+形式化
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
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 Exercises
3 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 Morgans 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 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.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 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.3.1 Constructors
8.3.2 Operators
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.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 Exercises
10 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 Exercises
11 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 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.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 Exercises
14 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 Exercises
15 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 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.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 Exercises
18 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 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.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 Comments
Index
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
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 Exercises
3 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 Morgans 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 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.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 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.3.1 Constructors
8.3.2 Operators
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.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 Exercises
10 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 Exercises
11 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 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.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 Exercises
14 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 Exercises
15 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 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.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 Exercises
18 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 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.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 Comments
Index
Shaoying Liu 教授，著名计算机专家，日本法政大学教授，上海交通大学和上海大学客座教授。早年在西安交通大学获得学士和硕士学位，后在英国曼彻斯特大学获得博士学位。现为IEEE计算机学会复杂性技术委员会副主席，IEEE计算机学会、ACM、日本软件科学与技术学会成员。多年来，在计算机科学的许多领域，包括形式化方法及理论、软件开发方法学、软件检查、软件测试、可靠复杂计算机系统以及智能软件工程环境等方面做出了重要贡献。目前在著名国际杂志及仁义发表学术论文80多篇，出版研究专著4部。
《软件开发的形式化工程方法：结构化+面向对象+形式化》首次开创了一个新技术，即形式化工程方法，把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法，其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和SOFL的迫切需求。
《软件开发的形式化工程方法：结构化+面向对象+形式化》通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE 2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、2、VDM和Larch等。《软件开发的形式化工程方法：结构化+面向对象+形式化》可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。
《软件开发的形式化工程方法：结构化+面向对象+形式化》通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE 2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、2、VDM和Larch等。《软件开发的形式化工程方法：结构化+面向对象+形式化》可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。
比价列表
公众号、微信群
缺书网微信公众号
扫码进群实时获取购书优惠