软件开发的形式化工程方法：结构化+面向对象+形式化

图书标准信息

• 作者 [日]刘少英 著
• 出版社 清华大学出版社
• 出版时间 2008-08
• 版次 1
• ISBN 9787302183174
• 定价 45.00元
• 装帧 平装
• 开本 16开
• 纸张 胶版纸
• 页数 408页
• 字数 534千字

【内容简介】

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

【作者简介】

ShaoyingLiu教授，著名计算机专家，日本法政大学教授，上海交通大学和上海大学客座教授。早年在西安交通大学获得学士和硕士学位，后在英国曼彻斯特大学获得博士学位。现为IEEE计算机学会复杂性技术委员会副主席，IEEE计算机学会、ACM、日本软件科学与技术学会成员。多年来，在计算机科学的许多领域，包括形式化方法及理论、软件开发方法学、软件检查、软件测试、可靠复杂计算机系统以及智能软件工程环境等方面做出了重要贡献。目前在著名国际杂志及仁义发表学术论文80多篇，出版研究专著4部。

【目录】

1Introduction
1.1SoftwareLifeCycle
1.2TheProblem
1.3FormalMethods
1.3.1WhatAreFormalMethods
1.3.2SomeCommonlyUsedFormalMethods
1.3.3ChallengestoFormalMethods
1.4FormalEngineeringMethods
1.5WhatIsSOFL
1.6ALittleHistoryofSOFL
1.7ComparisonwithRelatedWork
1.8Exercises

2PropositionalLogic
2.1Propositions
2.2Operators
2.3Conjunction
2.4Disjunction
2.5Negation
2.6Implication
2.7Equivalence
2.8Tautology，Contradiction，andContingency
2.9NormalForms
2.10Sequent
2.11Proof
2.11.1InferenceRules
2.11.2RulesforConjunction
2.11.3RulesforDisjunction
2.11.4RulesforNegation
2.11.5RulesforImplication
2.11.6RulesforEquivalence
2.11.7PropertiesofPropositionalExpressions
2.12Exercises

3PredicateLogic
3.1Predicates
3.2Quantifiers
3.2.1TheUniversalQuantifier
3.2.2TheExistentialQuantifier
3.2.3QuantifiedExpressionswithMultipleBoundVariables
3.2.4MultipleQuantifiers
3.2.5deMorgansLaws
3.3Substitution
3.4ProofinPredicateLogic
3.4.1IntroductionandEliminationofExistentialQuantifiers
3.4.2IntroductionandEliminationofUniversalQuantifiers
3.5ValidityandSatisfaction
3.6TreatmentofPartialPredicates
3.7FormalSpecificationwithPredicates
3.8Exercises

4TheModule
4.1ModuleforAbstraction
4.2ConditionDataFlowDiagrams
4.3Processes
4.4DataFlows
4.5DataStores
4.6ConventionforNames
4.7ConditionalStructures
4.8MergingandSeparatingStructures
4.9DivergingStructures
4.10RenamingStructure
4.11ConnectingStructures
4.12ImportantIssuesonCDFDs
4.12.1StartingProcesses
4.12.2StartingNodes
4.12.3TerminatingProcesses
4.12.4TerminatingNodes
4.12.5EnablingandExecutingaCDFD
4.12.6RestrictiononParallelProcesses
4.12.7DisconnectedCDFDs
4.12.8ExternalProcesses
4.13AssociatingCDFDwithaModule
4.14HowtoWriteComments
4.15AModulefortheATM
4.16CompoundExpressions
4.16.1Theif-then-elseExpression
4.16.2TheletExpression
4.16.3ThecaseExpression
4.16.4ReferencetoPreandPostconditions
4.17FunctionDefinitions
4.17.1ExplicitandImplicitSpecifications
4.17.2RecursiveFunctions
4.18Exercises

5HierarchicalCDFDsandModules
5.1ProcessDecomposition
5.2HandlingStoresinDecomposition
5.3InputandOutputDataFlows
5.4TheCorrectnessofDecomposition
5.5Scope
5.6Exercises

6ExplicitSpecifications
6.1TheStructureofanExplicitSpecification
6.2AssignmentStatement
6.3SequentialStatements
6.4ConditionalStatements
6.5MultipleChoiceStatements
6.6TheBlockStatement
6.7TheWhileStatement
6.8MethodInvocation
6.9InputandOutputStatements
6.10Example
6.11Exercises

7BasicDataTypes
7.1TheNumericTypes
7.2TheCharacterType
7.3TheEnumerationTypes
7.4TheBooleanType
7.5AnExample
7.6Exercises

8TheSetTypes
8.1WhatIsaSet
8.2SetTypeDeclaration
8.3ConstructorsandOperatorsonSets
8.3.1Constructors
8.3.2Operators
8.4SpecificationwithSetTypes
8.5Exercises

9TheSequenceandStringTypes
9.1WhatIsaSequence
9.2SequenceTypeDeclarations
9.3ConstructorsandOperatorsonSequences
9.3.1Constructors
9.3.2Operators
9.4SpecificationsUsingSequences
9.4.1InputandOutputModule
9.4.2MembershipManagementSystem
9.5Exercises

10TheCompositeandProductTypes
10.1CompositeTypes
10.1.1ConstructingaCompositeType
10.1.2FieldsInheritance
10.1.3Constructor
10.1.4Operators
10.1.5Comparison
10.2ProductTypes
10.3AnExampleofSpecification
10.4Exercises

11TheMapTypes
11.1WhatIsaMap
11.2TheTypeConstructor
11.3Operators
11.3.1Constructors
11.3.2Operators
11.4SpecificationUsingaMap
11.5Exercises

12TheUnionTypes
12.1UnionTypeDeclaration
12.2ASpecialUnionType
12.3IsFunction
12.4ASpecificationwithaUnionType
12.5Exercises

13Classes
13.1ClassesandObjects
13.1.1ClassDefinition
13.1.2Objects
13.1.3IdentityofObjects
13.2ReferenceandAccessControl
13.3TheReferenceofaCurrentObject
13.4Inheritance
13.4.1WhatIsInheritance
13.4.2SuperclassesandSubclasses
13.4.3Constructor
13.4.4MethodOverloading
13.4.5MethodOverriding
13.4.6GarbageCollection
13.5Polymorphism
13.6GenericClasses
13.7AnExampleofClassHierarchy
13.8ExampleofUsingObjectsinModules
13.9Exercises

14TheSoftwareDevelopmentProcess
14.1SoftwareProcessUsingSOFL
14.2RequirementsAnalysis
14.2.1TheInformalSpecification
14.2.2TheSemi-formalSpecification
14.3AbstractDesign
14.4Evolution
14.5DetailedDesign
14.5.1TransformationfromImplicittoExplicitSpecifications
14.5.2TransformationfromStructuredtoObject-OrientedSpecifications
14.6Program
14.7ValidationandVerification
14.8AdaptingtheProcesstoSpecificApplications
14.9Exercises

15ApproachestoConstructingSpecifications
15.1TheTop-DownApproach
15.1.1TheCDFD-Module-FirstStrategy
15.1.2TheCDFD-Hierarchy-FirstStrategy
15.1.3TheModulesandClasses
15.2TheMiddle-outApproach
15.3ComparisonoftheApproaches
15.4Exercises

16ACaseStudy-ModelinganATM
16.1InformalUserRequirementsSpecification
16.2Semi-formalFunctionalSpecification
16.3FormalAbstractDesignSpecification
16.4FormalDetailedDesignSpecification
16.5Summary
16.6Exercises

17RigorousReview
17.1ThePrincipleofRigorousReview
17.2Properties
17.2.1InternalConsistencyofaProcess
17.2.2Invariant-ConformanceConsistency
17.2.3Satisfiability
17.2.4InternalConsistencyofCDFD
17.3ReviewTaskTree
17.3.1ReviewTaskTreeNotation
17.3.2MinimalCutSets
17.3.3ReviewEvaluation
17.4PropertyReview
17.4.1ReviewofConsistencyBetweenProcessandInvariant
17.4.2ProcessConsistencyReview
17.4.3ReviewofProcessSatisfiability
17.4.4ReviewofInternalConsistencyofCDFD
17.5ConstructiveandCriticalReview
17.6ImportantPoints
17.7Exercises

18SpecificationTesting
18.1TheProcessofTesting
18.2UnitTesting
18.2.1ProcessTesting
18.2.2InvariantTesting
18.3CriteriaforTestCaseGeneration
18.4IntegrationTesting
18.4.1TestingSequentialConstructs
18.4.2TestingConditionalConstructs
18.4.3TestingDecompositions
18.5Exercises

19TransformationfromDesignstoPrograms
19.1TransformationofDataTypes
19.2TransformationofModulesandClasses
19.3TransformationofProcesses
19.3.1TransformationofSingle-PortProcesses
19.3.2TransformationofMultiple-PortProcesses
19.4TransformationofCDFD
19.5Exercises

20IntelligentSoftwareEngineeringEnvironment
20.1SoftwareEngineeringEnvironment
20.2IntelligentSoftwareEngineeringEnvironment
20.3WaystoBuildanISEE
20.3.1Domain-DrivenApproach
20.3.2Method-DrivenApproach
20.3.3CombinationofBoth
20.4ISEEandFormalization
20.5ISEEforSOFL
20.5.1SupportforRequirementsAnalysis
20.5.2SupportforAbstractDesign
20.5.3SupportforRefinement
20.5.4SupportforVerificationandValidation
20.5.5SupportforTransformation
20.5.6SupportforProgramTesting
20.5.7SupportforSystemModification
20.5.8SupportforProcessManagement
20.6ExercisesReferences
ASyntaxofSOFL
A.1Specifications
A.2Modules
A.3Processes
A.4Functions
A.5Classes
A.6Types
A.7Expressions
A.8OrdinaryExpressions
A.8.1CompoundExpressions
A.8.2UnaryExpressions
A.8.3BinaryExpressions
A.8.4ApplyExpressions
A.8.5BasicExpressions
A.8.6Constants
A.8.7SimpleVariables
A.8.8SpecialKeywords
A.8.9SetExpressions
A.8.10SequenceExpressions
A.8.11MapExpressions
A.8.12CompositeExpressions
A.8.13ProductExpressions
A.9PredicateExpressions
A.9.1BooleanVariables
A.9.2RelationalExpressions
A.9.3Conjunction
A.9.4Disjunction
A.9.5Implication
A.9.6Equivalence
A.9.7Negation
A.9.8QuantifiedExpressions
A.10Identifiers
A.11Character
A.12Comments
Index