软件开发的形式化工程方法--结构化+面向对象+形式化(英文影印版)
基本信息
- 作者: (日)Shaoying Liu [作译者介绍]
- 丛书名: 国外经典教材.计算机科学与技术
- 出版社:清华大学出版社
- ISBN:9787302183174
- 上架时间:2008-8-18
- 出版日期:2008 年8月
- 开本:16开
- 页码:408
- 版次:1-1
- 所属分类:
计算机 > 软件工程及软件方法学 > 软件方法/软件工程
教材 > 研究生/本科/专科教材 > 工学 > 计算机
教材 > 教材汇编分册 > 高等理工
本版教材征订号:00450965389
编辑推荐
唯一论述软件形式化方法与现有软件工程完美结合的英文教材,旨在增强现有软件开发技术的严密性,系统性,有效性以及工具的可支撑性,适合高年级本科生、研究生使用。...
内容简介回到顶部↑
本书首次开创了一个新技术,即形式化工程方法,把传统的形式化方法和软件工程有机结合起来。它提供了一个严密、系统、有效的软件开发方法,其实用性超过了目前所有形式化方法。这正好可以满足学术界、软件工程类学生对学习形式化工程方法和sofl的迫切需求。
本书通俗易懂,实例丰富,可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论,内容涵盖se 2004中关于“软件的形式化方法”的知识点,主要包括:有限状态机、statechart、petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、2、vdm和larch等。本书可作为计算机、软件工程等专业高年级本科生或研究生的教学用书,也可供相关领域的研究人员和工程技术人员参考。
本书通俗易懂,实例丰富,可满足读者即学即用的需要。书中对软件开发中的形式化工程方法进行了介绍和讨论,内容涵盖se 2004中关于“软件的形式化方法”的知识点,主要包括:有限状态机、statechart、petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、2、vdm和larch等。本书可作为计算机、软件工程等专业高年级本科生或研究生的教学用书,也可供相关领域的研究人员和工程技术人员参考。
作译者回到顶部↑
本书提供作译者介绍
Shaoying Liu 教授,著名计算机专家,日本法政大学教授,上海交通大学和上海大学客座教授。早年在西安交通大学获得学士和硕士学位,后在英国曼彻斯特大学获得博士学位。现为IEEE计算机学会复杂性技术委员会副主席,IEEE计算机学会、ACM、日本软件科学与技术学会成员。多年来,在计算机科学的许多领域,包括形式化方法及理论、软件开发方法学、软件检查、软件测试、可靠复杂计算机系统以及智能软件工程环境等方面做出了重要贡献。目前在著名国际杂志及仁义发表学术论文80多篇,出版研究专著4部。
.. << 查看详细
.. << 查看详细
目录回到顶部↑
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
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
前言回到顶部↑
本书以简洁明了的语言介绍了软件开发技术的最新成果——形式化工程方法,并在精确而简单的概念描述和必要的数学定义基础之上,以大量浅显易懂的案例系统地阐述了一个具体的系统建模和功能描述语言SOFL(Structured Object-Oriented Formal Language)以及在此语言基础之上建立起来的并具有代表性的形式化工程方法,称为SOFL方法。.
大家都知道,大型软件产品的开发是一个一般需要多数开发人员参加的复杂过程。它的主要环节有三个:理解、创造和确认。为了给用户提供满意而正确的软件产品,开发者首先必须正确和全面地理解用户的要求,包括功能要求、必要的数据资源、对功能与数据资源或系统行为的限制。在此基础之上,开发者必须通过系统的设计,构建软件系统的体系结构、数据结构和有效的算法,并以一定的编程语言实现其代码。这一系列的创造过程是不可能完全自动实现的,它必须依靠软件开发者来完成。然而,开发者是不能保证不出错的。实际上,大型软件系统的开发过程中一般都要出现大量的人为错误,经常造成软件产品的生产费用增大,不能按时交货,或不能保证质量。为此,完成的软件产品的质量必须得到严密的确认以后其产品才能送交用户使用。
保证软件质量的一个很重要的要素就是软件开发方法。开发方法是不是实用有效,一般取决于它是否具备三个要素:简单、可视化和精确。也就是说,该方法必须用起来简单,其表现形式要有效地发挥图形语言的可视化效果,同时所表达的内容必须精确以确保其意思能被准确理解。传统的软件开发方法,像结构化和面向对象的开发方法,基本上都用自然语言或语义不明的图形语言来描述用户的需求和系统设计文档。由于自然语言表达结构和所用术语的意思不清楚所造成的二义性,使得软件文档经常被误解或被随意解释以造成大量严重的设计或实现上的错误。这种局面也严重地影响了切实有效的支撑工具的开发和建立。..
上世纪七十年代以来,以Hoare逻辑和Dijkstra的最弱前置谓词演算为基础发展而来的形式化开发方法为严密地开发软件系统提供了理论基础和技术,为解决上述问题迈出了重要的一步。这些技术包括形式化规范说明书写作语言,逐步求精的开发方法,以及程序正确性证明技术。但遗憾的是,这些形式化技术只重视规范说明书的精确性和软件开发的严密性,而未能在简单可行和有效的可视化方面取得可喜的进展。恰恰相反,大型软件系统的形式化规范说明书往往复杂难懂,修改花费时间,出错的可能性很大。加之,逐步求精的开发方法和正确性证明技术都对开发人员的抽象和逻辑演算能力要求很高,使得这种技术很难被一般企业的软件开发者所接受。如何才能使严密性很高的形式化开发方法融合到传统的软件工程过程和技术中以提高和促进它们的严密性、有效性以及可控制性从而最终达到提高软件生产效率和软件质量的目的就成为一个意义重大的研究课题。
形式化工程方法和SOFL方法就是在这种情况下从上世纪八十年代末逐渐形成并发展而来的。其目的就是建立起能把形式化开发方法有效地结合到传统的软件开发过程和方法中的技术,使得形式化方法能够更加简单地被一般软件开发者使用,发挥其高严密性的特长以促进传统软件开发技术的有效性和系统性,并使软件开发过程能得到更加有效的工具支撑。为建立有效的系统模型和确切的需求规范说明书,SOFL方法提供了具有简单、可视化和精确特点的形式化规范说明书语言和行之有效的建立形式化规范说明书的三步法。为有效地查出需求规范说明书中的错误,SOFL提供了严密的复审(review)和说明书测试技术。为有效地利用结构化和面向对象设计方法的各自优势,SOFL提供了把结构化和面向对象的设计方法有机结合的技术,使得结构化方法在需求分析和抽象设计方面发挥其优点以方便开发者和用户之间的交流和合作,而使面向对象方法在详细设计和编码方面发挥其特长以增强所开发系统的可维护性和重用性。它也提供了把结构化设计转化成面向对象的程序代码的方法和技术。为有效地发现程序中的错误,SOFL提供了基于形式化规范说明书的严密检查(inspection)和严密测试技术。虽然这最后两种查错技术没有包括在本书之内,但它们已形成SOFL方法的不可分割的部分。总而言之,SOFL是集结构化、面向对象和形式化方法于一身,并具有简单、可视化和精确的特点的形式化工程方法。它已被工业界和多数软件工程人员所使用,其效果正在引起更多软件工程师和研究者的兴趣和关注。
本书的内容反映了作者在为提高软件开发质量以及开创严密有效和实用可行的形式化工程方法这个新技术领域近20年来的研究成果,并为进一步彻底的解决软件危机这个一直在困扰软件工程的重大难题,提出和阐述了“智能软件工程环境”这个未来软件工程的发展方向。作为本书的作者,在2008年第29届奥运会在北京召开之际,能将此书与国内读者见面,我感到由衷的欣慰,也很感谢清华大学出版社的极大热情和努力,帮助我实现了多年来想把形式化工程方法SOFL介绍给国内软件工程界的大学生、研究生、研究者以及工程技术人员的夙愿。我衷心希望读者能通过学习本书的内容享受到形式化工程方法的新思想,掌握其应用的系统技术,并提高开发高质量软件产品的技巧和能力,为自己的学习、就业、研究以及工作创造新的生机。
Shaoying Liu(刘少英)
日本法政大学计算机科学系
2008年8月...
大家都知道,大型软件产品的开发是一个一般需要多数开发人员参加的复杂过程。它的主要环节有三个:理解、创造和确认。为了给用户提供满意而正确的软件产品,开发者首先必须正确和全面地理解用户的要求,包括功能要求、必要的数据资源、对功能与数据资源或系统行为的限制。在此基础之上,开发者必须通过系统的设计,构建软件系统的体系结构、数据结构和有效的算法,并以一定的编程语言实现其代码。这一系列的创造过程是不可能完全自动实现的,它必须依靠软件开发者来完成。然而,开发者是不能保证不出错的。实际上,大型软件系统的开发过程中一般都要出现大量的人为错误,经常造成软件产品的生产费用增大,不能按时交货,或不能保证质量。为此,完成的软件产品的质量必须得到严密的确认以后其产品才能送交用户使用。
保证软件质量的一个很重要的要素就是软件开发方法。开发方法是不是实用有效,一般取决于它是否具备三个要素:简单、可视化和精确。也就是说,该方法必须用起来简单,其表现形式要有效地发挥图形语言的可视化效果,同时所表达的内容必须精确以确保其意思能被准确理解。传统的软件开发方法,像结构化和面向对象的开发方法,基本上都用自然语言或语义不明的图形语言来描述用户的需求和系统设计文档。由于自然语言表达结构和所用术语的意思不清楚所造成的二义性,使得软件文档经常被误解或被随意解释以造成大量严重的设计或实现上的错误。这种局面也严重地影响了切实有效的支撑工具的开发和建立。..
上世纪七十年代以来,以Hoare逻辑和Dijkstra的最弱前置谓词演算为基础发展而来的形式化开发方法为严密地开发软件系统提供了理论基础和技术,为解决上述问题迈出了重要的一步。这些技术包括形式化规范说明书写作语言,逐步求精的开发方法,以及程序正确性证明技术。但遗憾的是,这些形式化技术只重视规范说明书的精确性和软件开发的严密性,而未能在简单可行和有效的可视化方面取得可喜的进展。恰恰相反,大型软件系统的形式化规范说明书往往复杂难懂,修改花费时间,出错的可能性很大。加之,逐步求精的开发方法和正确性证明技术都对开发人员的抽象和逻辑演算能力要求很高,使得这种技术很难被一般企业的软件开发者所接受。如何才能使严密性很高的形式化开发方法融合到传统的软件工程过程和技术中以提高和促进它们的严密性、有效性以及可控制性从而最终达到提高软件生产效率和软件质量的目的就成为一个意义重大的研究课题。
形式化工程方法和SOFL方法就是在这种情况下从上世纪八十年代末逐渐形成并发展而来的。其目的就是建立起能把形式化开发方法有效地结合到传统的软件开发过程和方法中的技术,使得形式化方法能够更加简单地被一般软件开发者使用,发挥其高严密性的特长以促进传统软件开发技术的有效性和系统性,并使软件开发过程能得到更加有效的工具支撑。为建立有效的系统模型和确切的需求规范说明书,SOFL方法提供了具有简单、可视化和精确特点的形式化规范说明书语言和行之有效的建立形式化规范说明书的三步法。为有效地查出需求规范说明书中的错误,SOFL提供了严密的复审(review)和说明书测试技术。为有效地利用结构化和面向对象设计方法的各自优势,SOFL提供了把结构化和面向对象的设计方法有机结合的技术,使得结构化方法在需求分析和抽象设计方面发挥其优点以方便开发者和用户之间的交流和合作,而使面向对象方法在详细设计和编码方面发挥其特长以增强所开发系统的可维护性和重用性。它也提供了把结构化设计转化成面向对象的程序代码的方法和技术。为有效地发现程序中的错误,SOFL提供了基于形式化规范说明书的严密检查(inspection)和严密测试技术。虽然这最后两种查错技术没有包括在本书之内,但它们已形成SOFL方法的不可分割的部分。总而言之,SOFL是集结构化、面向对象和形式化方法于一身,并具有简单、可视化和精确的特点的形式化工程方法。它已被工业界和多数软件工程人员所使用,其效果正在引起更多软件工程师和研究者的兴趣和关注。
本书的内容反映了作者在为提高软件开发质量以及开创严密有效和实用可行的形式化工程方法这个新技术领域近20年来的研究成果,并为进一步彻底的解决软件危机这个一直在困扰软件工程的重大难题,提出和阐述了“智能软件工程环境”这个未来软件工程的发展方向。作为本书的作者,在2008年第29届奥运会在北京召开之际,能将此书与国内读者见面,我感到由衷的欣慰,也很感谢清华大学出版社的极大热情和努力,帮助我实现了多年来想把形式化工程方法SOFL介绍给国内软件工程界的大学生、研究生、研究者以及工程技术人员的夙愿。我衷心希望读者能通过学习本书的内容享受到形式化工程方法的新思想,掌握其应用的系统技术,并提高开发高质量软件产品的技巧和能力,为自己的学习、就业、研究以及工作创造新的生机。
Shaoying Liu(刘少英)
日本法政大学计算机科学系
2008年8月...
媒体评论回到顶部↑
Such books are to be whole-heartedly welcomed because they are written with an acute understanding of the issues for designers of useful software. .
--Cliff B. Jones
University of Newcastle upon Tyne
Probably the best coverage of any formal treatment I have seen. ...
--Peter Lindsay
University of Queensland
--Cliff B. Jones
University of Newcastle upon Tyne
Probably the best coverage of any formal treatment I have seen. ...
--Peter Lindsay
University of Queensland







点击看大图
加载中...

