版权信息

内容简介

作者简介

编辑推荐

目录

版权信息

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

作　者：(日本)刘少英

出版社： 清华大学出版社

出版时间： 2008

ISBN: 9787302183174

开本： 16

定价: 45.00 元

内容简介

《软件开发的形式化工程方法》首次开创了一个新技术，即形式化工程方法，把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法，其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和SOFL的迫切需求。.

《软件开发的形式化工程方法》通俗易懂，实例丰富，可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论，内容涵盖SE2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statechart、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、Z、VDM、Larch等。

《软件开发的形式化工程方法》可作为计算机、软件工程等专业高年级本科生或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。..

在软件开发领域，形式化方法涉及数学符号和微积分的使用，此类方法很难应用到面临着具体局限的大型系统中，这些局限包括开发者技能有限、时间和财务预算限制以及不断变化的需求。针对这些现状，书中介绍了形式化方法，提倡在软件工程过程中采用数学符号，从而从根本上增强行业中常用开发方法的准确性、全面性和有效性。

《软件开发的形式化工程方法》对SOFL(StructuredObject-OrientedFormalLanguage)方法进行了介绍，此方法由作者设计并已经通过行业验证。《软件开发的形式化工程方法》包含大量练习和重要的实际案例，有助于读者迅速理解并成功将这种方法运用于项目之中。

作者简介

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

编辑推荐

唯一论述软件形式化方法与现有软件工程完美结合的英文教材，旨在增强现有软件开发技术的严密性，系统性，有效性以及工具的可支撑性，适合高年级本科生、研究生使用。

目录

1Introduction.

1.1SoftwareLifeCycle

1.2TheProblem

1.3FormalMethods

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.12Exercises

3PredicateLogic

3.1Predicates

3.2Quantifiers

3.3Substitution

3.4ProofinPredicateLogic

3.5ValidityandSatisfaction

3.6TreatmentofPartialPredicates

3.7FormalSpecifcationwithPredicates

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.13AssociatingCDFDwithaModule

4.14HowtoWriteComments

4.15AModulefortheATM

4.16CompoundExpressions

4.17FunctionDefinitions

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.4SpecificationwithSetTypes

8.5Exercises..

9TheSequenceandStringTypes

9.1WhatIsaSequence

9.2SequenceTypeDeclarations

9.3ConstructorsandOperatorsonSequences

9.4SpecificationsUsingSequences

9.5Exercises

10TheCompositeandProductTypes

10.1CompositeTypes

10.2ProductTypes

10.3AnExampleofSpecification

10.4Exercises

11TheMapTypes

11.1WhatIsaMap

11.2TheTypeConstructor

11.3Operators

11.4SpecificationUsingaMap

11.5Exercises

12TheUnionTypes

12.1UnionTypeDeclaration

12.2ASpecialUnionType

12.3IsFunction

12.4ASpecificationwithaUnionType

12.5Exercises

13Classes

13.1ClassesandObjects

13.2ReferenceandAccessControl

13.3TheReferenceofaCurrentObject

13.4Inheritance

13.5Polymorphism

13.6GenericClasses

13.7AnExampleofClassHierarchy

13.8ExampleofUsingObjectsinModules

13.9Exercises

14TheSoftwareDevelopmentProcess

14.1SoftwareProcessUsingSOFL

14.2RequirementsAnalysis

14.3AbstractDesign

14.4Evolution

14.5DetailedDesign

14.6Program

14.7ValidationandVerification

14.8AdaptingtheProcesstoSpecificApplications

14.9Exercises

15ApproachestoConstructingSpecifications

15.1TheTop-DownApproach

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.3ReviewTaskTree

17.4PropertyReview

17.5ConstructiveandCriticalReview

17.6ImportantPoints

17.7Exercises

18SpecificationTesting

18.1TheProcessofTesting

18.2UnitTesting

18.3CriteriaforTestCaseGeneration

18.4IntegrationTesting

18.5Exercises

19TransformationfromDesignstoPrograms

19.1TransformationofDataTypes

19.2TransformationofModulesandClasses

19.3TransformationofProcesses

19.4TransformationofCDFD

19.5Exercises

20IntelligentSoftwareEngineeringEnvironment

20.1SoftwareEngineeringEnvironment

20.2IntelligentSoftwareEngineeringEnvironment

20.3WaystoBuildanISEE

20.4ISEEandFormalization

20.5ISEEforSOFL

20.6Exercises

References

ASyntaxofSOFL

A.1Specifications

A.2Modules

A.3Processes

A.4Functions

A.5Classes

A.6Types

A.7Expressions

A.8OrdinaryExpressions

A.9PredicateExpressions

A.10Identifiers

A.11Character

A.12Comments

Index

……