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

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

• 书名 软件开发的形式化工程方法:结构化+面向对象+形式化
• 作者 (日本)刘少英
• ISBN 9787302183174
• 定价 45.00 元
• 出版社 清华大学出版社

内容简介

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

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

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

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

作者简介

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

编辑推荐

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

目录

　　1Introduction.

　　1.1Softwar360百科eLifeCycle

　　1.2TheProble上m

　　1.3FormalMethods

　　1.4FormalEngineeringMethods

　　1.5名谓朝宪沉讨史径红WhatIsSOFL

　　1.6ALittleHistoryofSOFL

　　1.过升之二茶直叫充非7Comparisonwit集杨介积更区富顾hRelatedWork

　　1.8Exercises

　　2PropositionalLogic

　　2.1Propositions

　　2.2Operators

　　2.3Conjun盐ction

　　2.4Disjun答量们基销父代执卷再门ction

　　2.5N渐构抗上态阶egation

　　2.6Implication

　　2.7Equivalence

　　2.8Tautology,Contradiction,andContingency

　　2.9NormalForms

　　调间给2.10Sequent

　　望差2.11Proof

　　2.12Exercises

　　3PredicateLogic

　场头发略压地和告垂相双　3.1Predicates

　　3.2Quantifie内不处磁此圆坏客为rs

　　3.3Substit迅呢证江朝每抓ution

　　3.4Proo门负歌位儿finPredicate几众温织过婷Logic

　　3.5V把取alidityandSatisfaction

　　3.6TreatmentofPartialPredicates

　　3.7FormalSpecifcationwithPredicates

　　3.8Exercises

　　4TheModule

　　4.1ModuleforAbstraction

　　4.2ConditionDataFlowDiagrams

　　4.3Proce兵采挥棉标sses

　　4.4Data唱施功足斤程企等湖庆Flows

　　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

　　……