《軟體開發的形式化工程方法》首次開創了一個新技術，即形式化工程方法，把傳統的形式化方法和軟體工程有機結合起來。它提供了一個嚴密、系統、有效的軟體開發方法，其實用性超過了目前所有形式化方法。這正好可以滿足學術界、軟體工程類學生對學習形式化工程方法和SOFL的迫切需求。.
基本介紹
- 書名：軟體開發的形式化工程方法:結構化+面向對象+形式化
- 作者：(日本)劉少英
- ISBN：9787302183174
- 定價：45.00 元
- 出版社：清華大學出版社
- 出版時間： 2008
- 開本： 16
內容簡介,作者簡介,編輯推薦,目錄,
內容簡介
《軟體開發的形式化工程方法》通俗易懂，實例豐富，可滿足讀者即學即用的需要。書中對軟體開發中的形式化工程方法進行了介紹和討論，內容涵蓋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
……
