軟件開發(fā)的形式化工程方法：結(jié)構(gòu)化+面向?qū)ο?形式化

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 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 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