高级搜索 书名 作者 ISBN

软件工程卷1：抽象与建模

图书分类   计算机考试类图书   计算机等级考试 软件资格水平考试 计算机类认证考试 数学   基础数学教材 数学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 物理   基础物理教材 物理专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 力学   基础力学教材 力学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 化学化工   基础化学 化学 化工 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 机械材料汽车能源   机械 仪器仪表 材料 汽车 能源与动力工程 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 工业工程   国外大学优秀教材-工业工程系列(影印版) 国外大学优秀教材-工业工程系列(翻译版) 物流供应链丛书 其他 普通高等学校物流管理专业系列教材 工业设计   工业设计 建筑土木水利   建筑学（教材） 建筑设计及建筑文化 土木工程 水利工程 工程管理 环境与给排水   环境科学与环境工程 给排水 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 生物与医学   医学与生物学教材 教学辅导及考试用书 引进版图书 专业工具书和手册 医学专业参考书 生物学专业参考书 大众读物 电工基础与电气工程   电工基础 电气工程 专著、工具书及其他参考书 多媒体课件及网络教学资源 科普读物   院士科普第一辑 院士科普第二辑 院士科普第三辑 院士科普第四辑 走进科学殿堂 华裔科学家科普文集 其他 辞书   辞书 社会职业培训   工程技术操作技能类 城市服务业基础技能类 就业素质教育类 其他 航空航天   航空航天 计算机基础   计算机文化基础 办公自动化 应用基础 公共基础 软件技术基础 计算机导论 计算机组成与原理   计算机组成 计算机原理 接口技术 操作系统 算法与程序设计   C程序设计 数据结构 C++语言 编译原理 Visual Basic Java 汇编语言 FoxPro Delphi 算法 pb 计算机技术及应用   计算机技术及应用 计算机网络   Internet TCP/IP 计算机网络 网页制作 电子商务 网络安全 图形图像与多媒体   图形学 多媒体 图形图像 计算机辅助设计   计算机辅助设计 AutoCAD CATIA 数据库   SQL Server FoxPro Access Oracle 数据库原理 数据挖掘 PowerBuilder 软件工程   软件工程导论 软件工程 数理基础   数字逻辑 离散数学 线性代数 数理基础 信息安全   密码学 概论 病毒防护 电子信息   电子信息基础 通信工程 微电子 光电子 自动化 电子信息与计算机 计算机--其他   其他 经济管理   人力资源管理 物流 工商管理 市场营销 经济学 经济读物 金融学 财政学 国际经济贸易 会计学 旅游管理 公共管理 电子商务 考试用书 其他 管理科学与工程 人文社科   伦理学 教育学 心理学 哲学 语言文学 史学 新闻传播学 体育 其他 政治学 社会学 清华校史读物 综合 法律   司法考试用书 法律知识读物 宪法与行政法 法理法史 刑法 诉讼法 经济法 民商法 国际法 知识产权法 司法案例 比较法 艺术   服装艺术设计 工业设计 环境艺术设计 建筑 染织艺术设计 摄影艺术设计 视觉传达艺术设计 书法 陶瓷艺术设计 信息艺术与设计 绘画 雕塑 工艺美术 艺术设计学 艺术类基础教学 非英语专业本科教材   非英语专业本科教材 非英语专业研究生教材   非英语专业研究生教材 专升本教材   专升本教材 英语专业教材   英语专业教材 选修课系列教材   选修课系列教材 专门用途英语教材   商务英语 其他 学术类图书   学术类图书 考试类用书   国内考试用书 国外考试用书 工具书   工具书 娱乐休闲英语   娱乐休闲英语 英语学习方法   英语学习方法 非英语语种图书   日语 德语 外语--其他   其他 高职高专--公共基础课   公共基础课系列 高职高专--人文社科类   法律专业 新闻 高职高专--计算机类   计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 电子商务专业 嵌入式设计 高职高专--电子信息类   电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 高职高专--机电类   机电一体化专业 汽车专业 机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 高职高专--工科类   建筑专业 工程管理专业 高职高专--经济管理类   经济管理基础系列 市场营销专业 财务会计专业 企业管理专业 物流管理专业 财政金融专业 电子商务专业 国际商务专业 人力资源管理专业 高职高专--服务类   旅游专业 饭店管理专业 文秘专业 艺术设计专业 物业管理专业 基础教育--英语   教材教辅 课外读物 综合知识 基础教育--信息技术   教材教参 课外读物 教师培训 科普读物 中职教育--计算机类   计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 中职教育--公共课   公共基础课系列 中职教育--经济管理类   经济管理基础类 物流管理专业 财政金融专业 市场营销专业 企业管理专业 国际商务专业 财务会计专业 中职教育--电子信息类   电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 中职教育--机电类   机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 机电一体化专业 汽车专业 中职教育--服务类   旅游专业 饭店管理专业 文秘专业 艺术设计专业 软件工程卷1：抽象与建模 作者：Dines Bjorner著、刘伯超等 图书详细信息： ISBN：9787302208907 定价：79元 印次：1-1 装帧：平装 印刷日期：2009-11-26 图书简介： 本书是世界著名的计算机科学家Dines Bjorner教授对其所从事的软件工程研究 的总结。 这几卷书主要讲述了如何使用形式方法指导软件工程的开发，特别是作者独创性 地提出了领域工程这一全新的研究领域并在第~3~卷中予以系统的论述。作者结合~ RAISE（工业软件开发的严格方法）规约语言，详细阐释了在软件的领域分析、 需求分析、软件设计和开发的各个阶段，如何采用形式方法来指导软件开发模式， 来保证软件开发的可靠性和正确性。 前言： 023236-01.txt 本书是世界著名的计算机科学家Dines Bj\orner教授对其所从事的软件工程研究 的总结。 这几卷书主要讲述了如何使用形式方法指导软件工程的开发，特别是作者独创性 地提出了领域工程这一全新的研究领域并在第3卷中予以系统的论述。作者结合 RAISE（工业软件开发的严格方法）规约语言，详细阐释了在软件的领域分析、 需求分析、软件设计和开发的各个阶段，如何采用形式方法来指导软件开发模式， 来保证软件开发的可靠性和正确性。 在翻译的过程中，译者得到了Dines Bj\orner教授的大力支持。他非常关心中 国学者在软件工程这一领域的研究，热心推动我们将他的三卷著作介绍给中国读 者。 陈潇怡翻译了前言和第1章，李鑫翻译了第2、8、9章，向剑文翻译了第10、 11、12、13、\linebreak 14章和附录B的F-M的部分，孔维强翻译了第3、4、15、16、 17、18章，刘伯超翻译了第5、6、7、19、20、21、22章和附录A、附录B 的A-E与N-Z的部分，李国强审阅了全书。参加翻译和校对工作的还有田璟、王明华、袁春阳、李智伟、周琼琼、楚国华、齐亮、司慧勇、陈永然、李佳。 限于译者水平，译文中难免会出现 一些错误和不妥之处，敬请读者和专家予以批评指正。 前言 ------ 第1-3卷 本前言涵盖软件工程三卷书的内容，其中本册是第1卷。 软件工程 ------ 艺术、规范、工艺、科学、逻辑: 软件工程是艺术 \citeDEKnuth1,DEKnuth2,DEKnuth3\aindexknuth、 规范\citeEWD1\aindexdijkstra 、 工艺\citeReynolds81\aindexreynolds、 科学\citeGries81a\aindexgries 、 逻辑\citeECRHehner\aindexhehner， 以及下列的实 践\citeECRHehner93： 基于科学的洞察对软件（即技术）的综合 (即构建、 构造)，以及 为了探清和发现现有软件技术的可能的科学内容，对 其的分析 (即学习、研究)。 为了做到这一点， 软件工程 ------ 抽象与规约: 软件工程运用抽象和规约。 抽象 被用于把开发分割成可管理的小部分，从时期、阶段和步 骤中的高层抽象到低层抽象（即具体化）。 规约 记录并关联所有层次的抽象。 三卷中的第1、2卷详细地探讨了抽象和规约。 软件工程 ------ 三部曲: 软件工程包括应用领域的 分析，(对新软件的)需求综合和分析，以及该软件的 设计（即综合和分析）。因此，软件工程由以下组成： 领域工程，正如这几卷所展示给你的一样，它涵盖了许多学科 的丰富领域， 需求工程，正如我们在这几卷中将再次看到的一样，它有教科 书通常所没有探讨过的许多方面， 软件设计， 涉及软件体系结构、构件复合和设计等。 第3卷详细地探讨了该三部曲。 软件工程 ------ 实际问题: 另外，软件工程包含许 多实际问题：项目和产品管理；原则、技术和工具，它们被用于确保 可能在地理上分散的人员能够有效地一起工作，被用于依据多种开发处理模型 中的一种来选择、调节、监测和控制工作；计划、调度和分配开发资源(人、材 料、资金和时间)；相关的事务，包括成本预算、遗留系统、合法性等。 在本书中，我们将不涉及软件工程面向管理的那些刻面。 \treprikker 本卷中的每章以及其他几卷，都以一个提要开始。与本前言相关的一个例子如下：\newpage 假设： 你拿起这本书，是由于你有兴趣了解软件工程并可能学习 一种软件工程的新方法。 目标: 这几卷的主要目标是向你展示理解软件的崭新方式：它强调(I) 软件工程是信息科学的一部分，而信息科学是基于(i) 数学，(ii)计算机与计算科学，(iii)语言学，(iv) 硬信息技术（计算机与通信、传感器与执行器）的可用性，以及(v)应用。 进一步来说(II)该信息科学取决于许多通常以下列名字为人所熟知的哲学问题，如 认识论、本体论、部分关系学。 效果: 帮助你成为真正的专业软件开发工程师，并且是在该术语最宽泛 的意义上，正如这几卷所倡导的那样。 方式: 非技术的、推理的。 开发大规模软件系统是很困难的。构建它们且使得它们(i) 解决真正的问题，(ii)正确、人性化，而且 (iii) 良好地服务于需方组织，都是非常困难的。 本套丛书提供了业已被证明具有下列性质的技术：(i)能够使大规模软件系统的 开发比绝大多数当前的软件工程师所了解的要简单许多， (ii) 能够产生比通常所 遇到的系统更高质量的系统，并且 (iii)能够准时交付。 因此，我们强调本套丛书所针对的软件工程的下列性质：值得信任和可信的方法、 更高质量的软件产品、更高质量的软件开发项目、开发者和需求方的个人满意，也就 是说，软件工程师及其管理和用户及其管理。我们的目标是，如果有挫折，那 么也要少些挫折，并多些魅力和欢乐! \section*丛书的成因 \addcontentslinetocsection丛书成因 \labelf.4 关于为什么必须写这几卷，可以给出许多原因\footnote通常，当为某一“错误” 给出诸多“辩解”的时候，它们都不成立。不过本套丛书却绝不是个错误。： 形式技术应用于软件工程的所有阶段、时期和步骤，应用于各种 各样的软件开发中。 但是却没有已出版的按照如下方式涵盖软件工程的教科 书：就如我们稍后将对软件工程该术语的描述那样的，（除了其他的“非形式” 基础之外）也基于形式技术基础的教科书。 形式开发(即规约、精化、验证)的书籍更像专著而非教材，并且它们所涵 盖的主题相当狭隘： 通常只是软件规约，也即抽象软件设计及其具体化的规 约。这几卷中的形式规约，不只应用到软件，也应用到它们的需求规 定，而且作为（在任何书籍或讲义集中）全新的贡献，它也应用到了领域描述。 本套丛书的作者对于现有教材声称涵盖软件工程主题的方式长久以来感 到不太满意。 现今“所有”有关软件工程的教材就程序设计方法学的非常基础的问题 而言都是失败的\footnote一个显著的例外 是\citeGhezziJazayeriMandrioli。，特别是对于形式技术来说。如果 它们确实给出了所谓的“形式方法”的材料，其中有一些也确实这样做了，则 该材料典型地被“隐藏”在一个独立的章节中（如其名所示）。 在我们看 来，非形式技术和形式技术的相互作用，也即非形式描述和形式描述之间、非 形式推理和形式验证之间的相互作用等等，遍布软件工程的全部。（使用）形 式技术潜在的能力塑造开发的所有时期、阶段和步骤。传统的软件工程问题， 诸如软件过程、项目管理、需求、原型、确认（更不用说验证了)、测试、 质量保证和控制、遗留系统以及版本控制和配置管理，我们通过非形式和 形式技术的合理混合展示出这些辅助但关键的软件工程问题可以得到更好的处理。 勿容质疑，本套丛书将会解决这些“抱怨”。 在我们看来，现今所有的教材都没有适当地考虑软件开发者并没能充 分地理解软件所嵌入的领域，也即产生希望拥有“该新软件”的领域！正如 上面所提到的，我们的书的一个主要的新“特点”是将软件开发过程中所说明的 这些问题进行分离------在这一期间开发者首先花费大量的时间和精力去理解应 用领域，并为该应用领域的理解编制文档。 在我们看来，现今所有的教材都没能系统地给出“始终贯彻”和“扩展” 的原则、技术和工具。通过“始终贯彻”指那些通过大量的例子给出涵盖 开发所有的主要时期、阶段和步骤的原则、技术和工具。通过“扩展”指可以 应用到最大型规模软件开发项目的原则、技术和工具。 在我们看来，现今一些教材完全忽略了程序设计，即设计问题。从程序 设计方法学的角度来看，没有对软件开发的任何方法论方法的假 设。\footnote通过程序设计方法学的角度，我们指其本 身关注于诸如以下问题的角度：当规约循环时建立不变式，使用例程（过程、 函数）等确保适当的程序设计抽象。 在我们看来，现今的其他教材，没能做到逐步精化（即实现之间的关系的 开发观点）。\footnote通过逐步精化的观点，我们指如下的考虑：抽象，即使当 非形式表达时，也能够得到正确的具体化 ------ 当表达为代码时。 现今还有其他的教材没有设计的观点。\footnote通过设计观点，我们指 选择适当的算法和数据结构及其合理性和有效性的程序设计考虑。 最后，我们认为现今所有的教材都没能适当地将上述尽管更加理论性的观 点与诸如以下的普通的、工程问题的观点结合起来：(i) 开发过程模 型 （“瀑布模型”、“螺旋模型”、“迭代模型”、“进化模型”、“极 限程序设计”等等)，(ii) 质量管理， (ii) 测试和确认， (iv) 遗留 系统， (v) 软件再工程，等等。 \section*丛书的不足 \addcontentslinetocsection丛书的不足 这三卷书的主要不足在于我们过于简单地探讨了正确性问题，也即单一和成对 （开发步骤相关）规约的性质验证(定理证明、模型检查)。 在这几卷的其他地方和适当之处，我们会解释为何我们不引入与验证相关的大量 资料。 寻找这一知识的读者，可以参阅大量的教材（书籍、期刊和会议论文集的文章），或 等我们觉得能够胜任为该主题编写一本足够一般性的教材。现今的教材更多地 与一个特定的记法系统（即规约语言）相关。 \treprikker 显然我们并不知道有关如何开发所有可能种类的软件所需要知道的全部，而这几 卷中也并非包括我们所知的全部。通常软件开发用到多种多样的技术和工具。 任何我们所讨论的特殊技术和工具，我们对其讨论都达到了某个相当的深度，但 是还没有达到对一个专业的工程师在相关领域的足够深度。例如： 编译器开发: 我们谈到了许多对于真正的专业编译器开发者所 必需的内容，但并不是全部。我们探讨了我们认为所有的软件工程师应当知晓的 内容。并且我们对它的探讨采用了我们所发现的所有编译器教材都严重遗漏的方 式。请参见卷2，第16至20章。 操作和分布式系统开发：我们仅探讨了规约并发系统的一般原 则和技术。 嵌入式、安全关键和实时系统： 基本上与操作和分布式系统讨论的内容一样：我们强调卷2探讨了规约嵌入式、 安全关键和实时系统的技术。这些技术及其基本记法是：佩特里 网\citepetrinets、消息\citemscs和活序列图\citelscs、状态图 \citescs、时态逻辑\citetls及时段演算\citedc。 不过，在卷3第28章领域特定的体系结构 将在一定深度上给出应用下列 的开发上的原则、技术和工具：翻译系统（解释器和编译器）、信息系统（数 据库管理系统）、反应系统（即嵌入式、实时及安全关键系统)、 工件系统（工单系统）、客户/服务器系统、工作流系统等等。该章的讨 论是新颖的，并且受到Michael Jackson的问题框架概念\aindexjacksonma\citemja2001a的很大影响。 因此我们讨论了我们认为所有的软件工程师，无论其专业是什么，都应当了解 的内容。并且我们认为他们应当了解的内容要远远多于绝大多数的软件工程教材 所提供的内容。 正如其他地方所解释的那样，这几卷建议上面提及的专业领域中的教育和训练可 以在学习完卷3后进行。并且那些专业领域教材的许多内容实际上应当重写：改写 为形式规约等等。\vspace*-1.5mm \section*着手方法 \addcontentslinetocsection着手方法 我们的教学方法寻求找到“问题的根本”。我们认为这些根本由对下列问题的 基本理解构成：(i)“如何描述”的语言学，(ii)“描述什么”的近乎于哲学的 问题，(iii)语用、语义和句法的语言学（即符号学）问题， 以及(iv)使用数学（即使用形式规约语言）构造简明、客观的系统描述（因此也 要理解其语用、语义和句法 ------ 独立于应用现象的语用、语义和句法)。 所以本书从探究以上四个问题入手。在卷2中，我们以四个独立章节（第6 章到第9章）来探讨符号学（语用、语义和句法)这一主题。 同样这也是全新的：现有的有关软件工程的教材完全忽略了对这些问题的提及。 对毕业于任一具有良好声誉的学术机构的一个现代的、专业的软件工程师来说， 若没有掌握这四个教育基础（i--iv），对作者来说都是难以想象的！唉！ 而这并不是例外，而是现在的惯例：他们根本就没有了解过这些问题！\vspace*-1.5mm \section*软件新观 \addcontentslinetocsection软件新观 这几卷将为读者提供看待软件和开发软件过程的全新方式。它们将为读者提供一 个用于理解和开发软件的完全显著不同的方法。可能最好这样来描述该“新观”：软件 不仅是一件融合思考（分析）、描述（综合）和推敲（推理）这些智力过程的产品，更 是艺术品。软件，更容易作为知识的量化，如与应用领域的关联度（也许它是，也 许它不是正确的产品），人使用的适合度（人机交互），正确性（产品正确或错 误）等。 而难以找到作为产品的可量化（如便宜、快、小等标准用语）材料和标准。 掌握抽象------这几卷的一个主要论题，相对没有掌握抽象而言，它给任一 开发者提供了更好的机会来得到正确的产品和令产品正确 ------ 即使同样是这 些人并没有使用这几卷中许多的形式技术。绝大多数的从业软件工程师都没有掌握 抽象。但从其本质上来讲，软件是而且也必然是抽象的：当自动化软件用于支持 过去常常是人类工作过程的自动化时，该自动化软件不是“那些人类的过程”， 而仅仅是它们的一个模型、近似和抽象。 我们希望将软件开发的观点看作某事物，它在开发的时期、阶段和步骤中进行， 而且对于其来说，现在已有将这些时期、阶段和步骤相互关联的明确的技术。但 是这样的开发几乎没有在有关软件工程的标准教材中予以探讨。 我们希望采取这样一个软件开发的观点，其中可以形式地给出这些时期、阶段和步骤 的规约，可以形式化关系，并且在得到保证的时候，甚至可以形式地验证该关系。 至少在小规模和中等规模软件开发中，并且至少20年来，这一观点已经是可行 的了。但是这样的开发几乎没有在有关软件工程的标准教材中予以探讨。 我们希望推进一个软件开发的观点，其中开发者创建抽象、培养抽象的能力和使 用抽象。就仿佛这里所有层次中的程序设计者踌躇满志、饶有兴趣地“离析”美妙的抽 象并让他们找到对于程序的方式。最后，这些程序设计者让那些抽象来确定系统 的主要结构、确定美：正如用户所感，简洁和精确！ 这样的开发可以扩展到大规模系统。现在它成为可行的、可管理的和可提供的。 可以把它教授给绝大多数的在学术上可以教育的学生们，他们也可以对其进行学 习。\vspace*-1mm \section*“轻量级”形式技术 \addcontentslinetocsection“轻量级”形式技术 许多从业的程序设计者避开形式推理\footnote例如：使用一些数理逻辑证明程 序性质的一些引理。 或者说就是避开形式规约\footnote例如：非形式 但简明地描述某领域，或者使用某形式规约语言形式地规定某需求或规约某软件设计。 ，并且一些学术界人士也表达了对其的保留态度。 我们的方法是一个更实际的方法。我们考虑到了一系列的开发：从系统开 发，\indexcind系统开发% \indexcind开发!系统的% 经过严格开发，\indexcind严格开发% \indexcind开发!严格的% 到达形式开发。\indexcind形式的!开发% \indexcind开发!形式的% 通过系统开发，我们指形式地规约开发中一些步骤的开发。通过严格开发，我们 指表达和形式地证明系统开发中一些证明义务的开发。通过形式开发，我们指形 式地证明大多数重要的证明义务和严格开发的其他引理和定理的开发。 \begyndgraabox %\beginboxitparabox 0.7 setgray fill 为了遵循这几卷的原则和技术，我们建议“轻量”前进：系统化的开始。形式地 规约你的应用领域、需求和软件设计的最为重要的刻面。然后从那里开始程序设 计（即编写代码）！ \slutgraabox %\endboxitpara 从实践来看\citeClem84\aindexoest\aindexclemmensen，软件开发正确性 的最为重要的改善是系统化的积累。这几卷主要，可能也是几乎完全地关注于 系统化。某些特定种类的应用保证更高层次的信任，因此似乎严格开发实现了可 信性的下一个更高的阶段。最后，也有少数的客户愿意接受现今形式开发相当高 的成本：心脏起搏器、助听器植入、核动力装置的混合控制器、无人驾驶地铁及 诸如此类。 \Volchapsec3322讨论了相当数量的有关所谓的“形式方法”的信条、错误 理解和错误观念。本卷的 第\ref1ch1meth.misnomer节和\volchapsec331讨论了为什么方法不可 以是形式的，但一些技术却可以是。\vspace*-1mm \section*“超级程序设计师” \addcontentslinetocsection“超级程序设计师” 许多从业程序设计人员和一些学术界人士坚信程序设计人员无限制的个人主义： 他们担心，不得不遵循许多方法原则和形式技术可能会压制“超级程序设计师” 的创造性和生产力。我们并不担心。 我们已经造就了超过100名的理学硕士论 文研究生。绝大多数在丹麦的不到8个的软件公司工作。所有人都或多或少 的遵循这几卷中的许多原则和技术。他们当中的绝大多数都是超级程序设计师。 下文是其他学者和我以前的学生，同样还有和我一样在教授和传播类似于这几卷 中的方法和技术的在世界各地的同事们所表达的。我在此强调： \begyndgraabox%\beginboxitparabox 0.7 setgray fill \qquad 这几卷中的原理和技术，即使只是“轻量级”遵循，即使很难显式地遵循，但只 要你在学习这几卷的时候掌握了它们，它们将改变你对软件工程的态度。而这将是 不一样的。 \slutgraabox%\endboxitpara 我们确信，从现在起，你将更多的去享受“超级程序设计”，享受成为一名程序 设计者，并且“在许多小的方面聪明伶俐，设计聪明的小技巧来把事情 做的更好、更快。” 我们不能否认在低层的聪明伶俐的核心作用\footnote本 段中这两个楷体的引文源自电子邮件，2002年1月20日，来自Bertrand Meyer教授\citez:abri80a,z:meye85a,Meyer88, \aindexabrial\aindexmeyer% 瑞士苏黎世ETH和美国加利福尼亚圣巴巴拉ISE。 。我们将用许多可传授 的工程原则和技术来增强你在这个方面可能已有的任何技能。“成功的 程序设计者既是野兽也是天使。” 我们断言我们同样能够给出几个中等规模的软件开发，其中对这几卷的原则的知晓 似乎在设计优雅、优美的产品方面提供了巨大的帮助。而且 “美就是 我们的工作”\citebeauty90。\vspace*-1.5mm\aindexdijkstra \section*何为软件工程 \addcontentslinetocsection何为软件工程 我们继续在本前言的第1页所开启的对软件工程的刻画。 软件工程:\ \ 对我们来说，在最一般的意义上，“软件工程”和其 他各种各样的工程一样，是一个专业的集合，这些专业基于科学的洞察力构造 的技术，或者分析技术以探究其科学的内容（包括价值），或者通常两者兼而 有之。 “软件工程师”：\ \ 因此软件工程师（但请参见下文有关对该术 语的批评）“跨越”了一方面是计算机科学与计算科学和另一方面是 软件人工制品（软件技术）之间的“桥梁”，基于从计算机和计算科 学的许多学科所建立的知识体所获得的洞察力对后者进行构造（或研究）。 更通俗地说，软件工程包含用于下列目的的一般和特定的原则、技术和工 具：(i)分析那些易于通过计算给出解决方案或支持的问题；(ii)综合这样的（诸 如软件的程序的）解决方案；(iii)在大的项目（即涉及到多于一个开发者的项目， 和/或结果软件将被其他（人员）使用而非开发者自己的项目）中进行该分析和综 合；以及 (iv) 管理这样的项目和产品（包括计划、预算、监督和控制该项目和 产品）。 但是我们可以把一个主题称作软件工程并不必然意味着我们可以谈到“软件工程 师”。如上所述，同时我们希望这几卷的读者都能清楚的明白，软件工程是由我 们可能本来希望称之为“软件工程师”的人来利用的一组原理、技术和工具。但 是对任何人来说，在没有进一步、更加“狭窄”的鉴定的时候某人就被冠之以软 件工程师似乎是有问题的。它将会给这条那个人是一个软件工程师消息 的接受者传递这样的信念，这里所述的人能够专业地处理几乎任何软件的开发。 与Jackson\citeMJPMS\aindexjacksonma 一致，我们断言并不存在软件工程 师！有编译工程师、嵌入式系统（软件）工程师、信息（和数据库）系统（软件） 工程师、银行业务软件工程师等等，就如同我们说起汽车工程师和电力工程师而 非机械或电气工程师一样。 因此我们断言这几卷中的原则、技术和工具适用于广泛的专业范围内的软件工程 师。这几卷给出了这些跨越最广泛的可能范围的原则、技术和工具的应用示例。 原则、技术和工具一般来说是有用的且能够被应用到行业和应用的广阔领域中， 这一事实只是意味着学生们必须另外学习所选定职业的专门教材，如编译器开发、 安全关键的实时软件开发、数据库系统等等，以成为适当的专业软件工程师。 \section*作者的愿望 \labelf.8 \addcontentslinetocsection作者的愿望 因此我的希望如下：给你提供一本不同种类的教材；将超过30年的精彩的程序 设计方法研究和控制实验实践放到更广阔的软件工程的舞台上来；为你展示当遵 循语言学、哲学、符号学和数学的教学基础，软件开发将会是怎样一个美妙绝伦 的世界；以及将超过25年的逐渐发展的课堂讲义变为一套连贯的、一致的和相 对完全的三卷书。 \beginquote 我写下了这几卷，是因为我曾想理解如何开发大规模软件系统。当我开始的时 候，大概25年以前当我开始为这个主题书写课程讲义的时候，我所知道的比 现在要少的多。同时我对于许多聪明好学的学生参与到该实践中来感到无比的 高兴。我发起了为诸如\textttCHILL \citeHaff87,CCITT81\aindexhaff\ 和\textttAda \citep:db:Bj80g,e:db:Bj80f,Clem84 \aindexclemmensen\aindexoest\ 这 些不易使用的程序设计语言的编译器的大规模商业开发，由此我斟酌和修正了 我的想法。在测试这些想法的同时对有关软件工程的写作已是一个变得清醒的 经历。软件工程中仍存在许多我不得不写、考虑和体验的边边角角。同时，这 就是你所得到的了！ \endquote 这几卷是我的代表作。 \section*这几卷在软件工程教育课程中的作用 \addcontentslinetocsection这几卷在软件工程教育课程中的作用 \labelf.9 这几卷的目标读者是谁呢？ 下文中间接地回答了这个问题。 在产生硕士学位的学术性软件工程教育这一更大的环境中，我们如何看待这几 卷书所扮演的角色呢？图1将帮助我们回答这个问 题。\figuresemantics1pre1:courses1图1中的标号框指代成为软件工程师 日常实践的主题，因此是值得学习的主题。在图1中，标号框中的双向箭头表 示能够同步学习所指代的主题。标号框间的有向（单向）箭头指代这些主题学 习的适当的、建议的优先关系。一个“扇入”（多源）箭头表示一个主题可能 需要（即作为前提条件）一个或多个（先导）主题的知识。一个“扇出”（可 能多目标）箭头表示箭头源头的主题对于一个或多个后继主题来说是“必须” 的。 我们强调这里将这几卷放在学术性的软件工程理学硕士教育课程的上下文 中 ------ 不要与计算机科学理学硕士教育混淆。前者的目标是工业界的程序 设计者：商业软件的开发者。后者的目标是在学术性研究机构中有用的理论家。 关于一个类似的在（理论）计算机科学理学硕士学位的学术性课程的上下文中的 场景，有关另一个图的另一个解释也可以给出，以及为学术性软件工程理学学士教 育课程的本科生教育的另一个解释。 前提条件或者“并行”课程： 我们假定这几卷的读者 ------ 或 者正在上基于这几卷的卷1的课程的读者逐渐 ------ 熟悉命令式、函数式、逻 辑、并行和机器程序设计的一般性主题。 这些主题的教学必须涵盖有关特定语言的技巧学习和训练，比如 函数式程序设计的\textttSML\indexpindStandard ML\indexpindSML （标准ML） \citeMRHansen+HRischel,SML-Milner1， \aindexmilner\aindexharper\aindextofte% \aindexrischel\aindexhansenmr% 逻辑程序设计的\textttProlog\indexpindProlog \citeProlog2,Prolog1 ，\aindexlloyd% 模块（即面向对象）程序设计的\textttModula-3 \citeModula3.2,Modula3.1\indexpindModula-3, \aindexwirth% \textttOberon \citeOberon3\indexpindOberon\ 和\ \aindexwirth% \textttJava \indexpindJava \citejava，以及 \textttoccam \citeoccambook82\indexpindoccam \aindexmay% 和某一精选的“流行技术”的硬件（比如类似于Intel）的芯片。 它们的教学也必须涵盖 ------ 在基本的程度上------ 有关于这些程序设计方式 和语言的理论背景的知识获得：递归函数理论 \citeRogers67,Boolos89\aindexrogers、逻辑程序设计的逻辑 \citeProlog1,Prolog2、命令式程序设计的Hoare逻 辑\citeApt81,Apt84\aindexapt\ 以及并发进程代数（\textttCSP \citecsp\ 和佩特里网\citepetrinets）。机器程序设计主题 \citejava-vm-97a,java-vm-99a,pentium-98 是唯一真正面向硬件但并不是面 向硬件设 计\citecomp-arch-95,comp-org-98\aindexpatterson\aindexhennesy 的课程。 没有涵盖协同设计\citeco-design-97，即组合的硬件/软件系统设计（典型的 比如嵌入式系统，见下文）。但是可以“添加其他的框”！在上述几种的课程中 包含或是另外的一些课程，我们期盼读者具有一些算法和数据结构的能够实际应 用的知识，即熟悉这些经典和现代的算法和数据结构和具体复杂性度 量\citeUHA,Lyncha,Melhorn,Tarjan83,Wir76。% \aindexwirth\aindexhopcroft\aindexullman\aindexaho\aindextarjan% \aindexmelhorn\aindexlynch \vspace3mm \begincenter \epsfigfile=t-1.eps\vspace2mm \small 图1\quad 基于这几卷的课程：第一个场景 \endcenter\vspace1mm 辅助课程： 结合软件工程的学习，这几卷也是它的一部分，我们假 定读者对达到学士程度的所列科目的数学觉得轻松自在，或变得有此感觉。我 们建议\citeWoodcock88\aindexwoodcock，一个让人高兴的“短小的”介绍， 以及对离散数学的大量介绍\citeSSEpp。我们发现\citeSSEpp对于该主 题的一个完全独立并且是主修的课程来说，是一本非常好的教材。一本假定每 个软件工程师都有的书。类似地，但是更多地被看作是学期项目的一部分和实 验室（包括自学）工作的其他形式，我们期望读者对实际的、已有的平台技术（软件工具试 验箱）感到适度轻松。 主要课程： 在尝试后续课程的广度和深度之前，这几卷也用于有关 软件工程的三个主要课程中。另外我们建议得到这两本书 \citeRSL,RaiseMethod，\aindexgeorge\aindexprehn% \aindexstorbank\aindexmilne\aindexhughes\aindexwagner\aindexnielsencb\ 第一本作为辅助材料，第二本特别是用于填补这几卷中没有讨论的验证（即设 计演算）部分。 后续课程： 传统的软件工程更多地关注于“过份的自省”，即计算 系统的内省部分：编译器、数据库系统、分布式系统、操作系统、实时（容错 和）嵌入式系统等等。理想上现在对这些主题的探讨应当基于形式规约和设计 演算并从它们的角度来进行。（给定1$\sim$3个单元的工作量的）嵌入式系统的主 题可以深入到包括硬件/软件协同设计\citeco-design-97 ，并且在其他方 面相当依赖于其他系统工程的问题。\vspace2mm \begincenter \epsfigfile=t-2.eps\vspace2mm \small 图2\quad 基于这几卷的课程：第二个场景 \endcenter\vspace2mm \small 图3\quad 基于这几卷的课程：第三个场景 \endcenter\vspace3mm 另外，我们恳请每位软件工程的学生进行两个“实践”：一个大项目的，面向讨 论/研究小组的“系统编程” 课程和一个类似“应用系统”课程，分别进行实验 性和探索性的研究和开发一个非常重要的硬件/软件控制系统和一个商业的、工 业的或其他的应用，这几卷中提示了很多这样的例子！ \rb 提示的最后一个软件工程课程：“软件工程管理”。我们有许多关于这个 主题的课程材料。暂请参考Hans van Vliet的杰出著 作\citeHansVanVliet2000。 \re 形式语言的语言学，包括形式语义的理论，是专业的工程师应当具备的非常重要 的知识。与之有关的两门课程：图3最左边第三行和第四行的框。举例来说，语言学 课程可以基于David A.\ Schmidt或John Reynolds的著作。参考资料 是\citeD.A.Schmidt-94\aindexschmidtda和\citeReynolds1998。 \aindexreynolds\ 举例来说，语义学课程可以基于\citesemantics中的任意一 个。 \section*为什么这么多材料 \addcontentslinetocsection为什么这么多材料 这几卷某种程度上是完备的。我们期待这几卷用于大学和学院的课程，以及由读 者自学。一些大学和学院在一些课程中涵盖了部分材料，这些课程在我们同样也 给出的这些课程材料中是较早的部分。因此它可以被假定而省略掉吗？不，不完全是这样， 因为其他的大学和学院没有涵盖这些作为前提条件的材料。因此这几卷必须反反 复复地涉及这些内容。由于这几卷严重地依赖于数学 ------ 不是任何高级的东 西，也不是需要了解或使用任何高深定理的东西 ------ 我们需要在 第\ref1ch3$\sim$\ref1ch8章简要重述这些材料中的一部分。 这里我们也要解 释和说明$\lambda$演算。 由于现实生活现象无论其是否显然都必须被感觉到，也就是说，必须被概念化， 在卷3的第3、 5、 6、 7章，我们将深入探讨什么构成了方法学，什么是定 义，什么是现象和概念，以及什么是描述。 由于语言对于我们在软件工程中所做的一切来说是那样重要的基础，而且由于我 们不能依赖于那些已经学到（即知晓）的必需知识，因此我们也同样需要去深入 地探讨语用、语义和句法，总体来说，就是语言符号学，无论其是形式的还是非 形式的。 由于自动机和有限状态机类似地构成我们的科学和工程中不可缺少的组 成部分，我们也同样需要在卷2的第11章讨论该主题。在探讨所有这些辅助概 念的时候， 我们改变对其的讨论方式：我们从非传统的角度来介绍它们。由此我 们期望读者对其获得一个完全不同的视角，它与工程更加相关而可能不是科学， 它与实践更加相关而不是理论。在任何实际的课程中，教师因此可以基于当地的 课程来省略一些“深入探讨”的材料。 \section*课程中如何使用这套丛书 \addcontentslinetocsection课程中如何使用这套丛书 与这几卷一起，我们计划通过因特网： \texttthttp://www.imm.dtu.dk/\db/The-SE-Books 提供内容详尽的一组电子文档： 各种建议的课程结构（有对各卷的章节和幻灯片的参考） 小组项目描述 ------ 一些带有解答 大型开发示例 形式方法的URL 形式方法工具的URL 自本书出版之日起，真实身份的教师可以通过出版社获得 几千页的postscript/pdf课程幻灯片 选定练习的解答 有代表性的（学生）项目报告 幻灯片将涵盖这几卷文本的一个很大的子集。通过绝大多数计算机上的阅读软件， 教师可以亲自选择那些涵盖适当课程的幻灯片。 \section*本书的简要介绍 \addcontentslinetocsection本书的简要介绍 本书分为三卷。每卷分为若干部分。绝大部分由若干章或附录构成。 绝大多数章都提供了练习。一组特定的练习给出了系统的描述。它们的给出几乎贯穿 整个卷1。这些练习在附录\ref1pt0中予以介绍。 所有的卷都有大量的交叉引用的索引和文献引用。在卷1中，有术语表附录B。 它用于涵盖整个三卷。该术语表的阅读可以独立于这几卷的其他部分。 卷2的附录A给出了类型、值、函数、变量、通道、对象和模式以及在它 们其中大多数之上的参数的命名习惯。 \section*本卷的简要介绍 \addcontentslinetocsection本卷的简要介绍 本卷有若干章节。这些章节被编组为部分。图4提炼出这些章节之间的 优先关系。这也是对学习本卷大致顺序的建议。 第1章是学习所有其他章的前提。 第2$\sim$4章可以被在学校学习过一定离散数学的读者略过。 第5$\sim$6章可以被在学校学习过更多离散数学的读者略过。 第7$\sim$9章只能被熟练掌握所提及主题的读者略过。 第10$\sim$16章组成卷1的核心部分。 在第1章之后，如果你继续学习第2章，则你应当学习第2$\sim$9章的全部。 在第1章后，如果你继续学习第5章，则你应当学习第5$\sim$9章的全部。 在第1章后，如果你继续学习第7章，则你应当学习第7$\sim$9章的全部。 在继续学习19$\sim$21章之前，你可以略过第17和/或18章。 在完成第16$\sim$21章中的任一章后，你可以结束本卷的学习。 学习第22章没有任何害处。 大多数章节中的小节可以略过。特别是那些具有较大的例子，或是结束章节的部 分。 这样教师和读者能够组织许多适当的课程和学习。 \begincenter \epsfigfile=t-4.eps\vspace2mm \centerline\small 图4\quad 章节优先顺序图 \endcenter\vspace1mm \re \section*致谢 \addcontentslinetocsection致谢 作者真挚地感谢以下同事，他们中的绝大多数都曾经与我共事，并且多年以来他 们在很大程度上影响了我的思想和行动： Cai Kindberg， Jean Paul Jacob， Gerald M.\ Weinberg， Peter Lucas， Gene Amdahl， John W.\ Backus， Lotfi Zadeh， (the late) E.F.\ (Ted) Codd， Cliff B.\ Jones， (the late) Hans Beki\vc， Heinz Zemanek， Dana Scott， (the late) Andrei Petrovich Ershov， Hans Langmaack， Andrzej Blikle， Neil D.\ Jones， J\orgen Fischer Nilsson， David Harel， Bo Stig Hansen， S\oren Prehn， Sir Tony Hoare， M\'\iche\'al Mac an Airchinnigh， Michael Jackson， Zhou ChaoChen， Chris George， Jim Woodcock， Kokichi Futatsugi， Joseph A.\ Goguen， Larry Druffel和 Wolfgang Reisig ------ 大致按时间顺序排列。 特别地我希望向S\oren Prehn和Chris George表达我最真诚的谢意和感激 ------ 为了这多于四分之一个世纪的灵感的激发。 我也要向IFIP工作组WG\,2.2和 WG\,2.3的（上面没有提及的）成员致以我 的感激之情。这些工作组的会议，其讨论和辩论对所有主题都是“自 由的”，帮助我细化和关注于这几卷的内容： Jean-Raymond Abrial， Jaco W.\ de Bakker， Manfred Broy， (the late) Ole-Johan Dahl， (the late) Edsger W.\ Dijkstra， % Jim Horning, Leslie Lamport， Zohar Manna， John McCarthy， Bertrand Meyer， Peter D.\ Mosses， Ernst-R\"udiger Olderog， Amir Pnueli， John Reyn\-olds， Willem-Paul de Roever 和 Wlad Turski ------ 按字母序排列。 关于这几卷写作（和文字编辑）阶段， 极其感谢我以前的学生Christian Krog Madsen（完成了卷2的第12$\sim$14章），Steffen Holmslykke（完成了卷2的 节10.3），Martin P\veni\vcka（基本上完成了 卷2的节12.3.4、14.4.1和14.4.2），以及Hugh Anderson。 \rb 最后，致以我在施普林格的编辑最亲切和热诚的感谢。首先是Ingeborg Mayer，然后是Ronan Nugent。同样也非常感谢文字编辑Tracey Wilbourn ------ 非常感谢您严格彻底的工作。 \it Dines Bj\orner 目录： 023236-01.txt 原著作者为中文版所作的序 译者序v\\[1mm] 前言\hfill vii\\[1mm] 丛书成因viii 丛书的不足ix 着手方法x 软件新观x “轻量级”形式技术xi “超级程序设计师”xi 何为软件工程xii 作者的愿望xiii 这几卷在软件工程教育课程中的作用xiii 为什么这么多材料xvi 课程中如何使用这套丛书xvi 本书的简要介绍xvii 本卷的简要介绍xvii 致谢xviii 开篇1 开篇1 1绪论3 1.1准备3 1.2软件工程三部曲5 1.2.1软件和系统开发6 1.2.2三部曲引出6 1.2.3领域工程6 1.2.4需求工程7 1.2.5软件设计8 软件：代码和文档8 软件设计，I8 开发时期、阶段和步骤9 软件设计，II9 1.2.6讨论9 一般问题9 1.3文档10 1.3.1文档种类10 1.3.2时期、阶段和步骤文档11 1.3.3信息文档11 当前情况文档编制11 需要文档编制11 产品概念和措施11 设计概要12 范围和区间描述12 纲要12 合同12 讨论12 1.3.4描述文档13 描述文档种类和类型13 粗略描述13 术语14 叙述14 形式模型15 讨论15 1.3.5分析文档16 粗略描述分析和概念形成16 描述、规定和规约的确认16 规约属性的验证17 开发时期、阶段或步骤变迁的正确性17 讨论18 1.4形式技术和形式工具18 1.4.1关于形式技术和语言18 1.4.2软件工程教材中的形式技术19 1.4.3一些程序设计语言19 1.4.4一些形式规约语言19 关于面向模型的规约语言19 关于面向性质的规约语言20 关于面向性质\面向模型的规约语言20 再论程序设计语言20 规约语言续20 1.4.5目前形式语言的不足21 1.4.6其他的形式工具21 1.4.7为什么要形式技术和形式工具22 一些理由22 轶事和类比证据22 1.5方法和方法学23 1.5.1方法23 1.5.2方法学23 1.5.3讨论23 1.5.4元方法学24 1.6软件基础24 1.6.1教学法和范式25 1.6.2语用、语义和句法25 语用25 语义25 句法27 1.6.3规约和程序设计范式28 1.6.4描述、规定和规约28 软件规约、需求规定和领域描述29 1.6.5元语言29 1.6.6总结29 1.7目标和效果29 1.7.1目标29 主要目标29 一些其他的目标30 1.7.2效果30 主要效果30 一些其他的效果30 1.7.3讨论30 1.8文献评注30 1.9练习31 离散数学33 2数35 2.1引言35 2.2数符和数35 2.3数的子集36 2.3.1自然数：\bf Nat36 对一些 结构的解释37 2.3.2整数: \textbf Int37 性质37 \texttt RSL 的整数代数38 2.3.3实数：\textbf Real38 有理数39 实数上的操作39 2.3.4无理数39 2.3.5代数数39 2.3.6超越数40 2.3.7复数和虚数40 2.4类型定义：数40 2.5总结41 2.6文献评注41 2.7练习42 3集合44 3.1背景44 3.2数学的集合45 3.3特殊集合46 3.3.1外延公理46 3.3.2划分46 3.3.3幂集47 3.4分类和类型定义：集合47 3.4.1集合抽象47 3.4.2集合类型表达式和类型定义47 3.4.3分类47 3.5\texttt RSL\ 中的集合48 3.6文献评注48 3.7练习48 4笛卡尔50 4.1要点50 4.2笛卡尔值表达式50 4.3笛卡尔类型51 4.4笛卡尔的目52 4.5笛卡尔的相等52 4.6一些构造的例子52 4.7分类和类型定义：笛卡尔54 4.7.1笛卡尔抽象54 4.7.2笛卡尔类型表达式和类型定义54 4.8\texttt RSL 中的笛卡尔55 4.9文献评注55 4.10练习55 5类型57 5.1值和类型58 5.2现象和概念类型58 5.2.1现象和概念58 5.2.2实体：原子和复合59 5.2.3属性和值59 原子实体属性和值59 复合实体属性和值59 讨论61 5.3程序设计语言类型概念62 一些例子62 讨论63 5.4分类或抽象类型64 5.5内建和具体类型64 5.6类型检查65 5.6.1类型确定的变量和表达式66 5.6.2类型错误66 5.6.3类型错误检测67 5.7类型作为集合，类型作为格67 5.8总结67 5.9练习67 6函数69 6.1概述70 本章的结构70 特别注释71 6.2要点71 6.2.1背景71 6.2.2一些函数概念71 函数定义72 函数“映射”（图）73 函数空间和函数基调类型74 函数类别74 6.3函数是如何产生的75 6.4关于求值概念的题外话76 6.4.1求值，解释和细化76 6.4.2两个求值的例子76 6.4.3函数调用77 6.5函数代数78 6.5.1代数78 6.5.2函数类型78 6.5.3高阶函数类型79 6.5.4非确定性函数79 6.5.5常量函数79 6.5.6严格函数80 6.5.7严格函数和严格函数调用80 6.5.8函数上的操作81 6.6Curry 化和 记法82 6.6.1Curry 化82 6.6.2$\lambda $ 记法82 6.6.3Curry 化和 记法的例子83 6.7关系和函数83 6.7.1谓词84 6.7.2通过关系搜索的函数求值84 6.7.3非确定性函数85 6.8类型定义85 6.9结论85 6.10文献评注85 6.11练习86 7$\lambda $ 演算87 7.1非形式介绍87 7.2“纯” 演算句法88 7.3$\lambda $ 演算的语用89 7.4“纯” 演算语义89 7.4.1自由和约束变量90 7.4.2绑定和辖域90 7.4.3变量的冲突和混淆90 7.4.4代入90 7.4.5$\alpha $ 转换和 $\beta $ 转换规则91 7.4.6$\lambda $ 转换91 7.5名调用和值调用93 7.6Church--Rosser 定理 ------ 非形式版本93 7.7\texttt RSL 记法 93 7.7.1扩展 表达式93 7.7.2\bf “let ... in ... end” 结构94 7.8不动点94 7.8.1要点94 7.8.2非形式概述95 7.8.3不动点操作符 \textbf Y95 7.8.4不动点求值96 7.9讨论97 7.9.1概述97 7.9.2关于最小、最大、全部不动点97 7.9.3强调97 7.9.4原则、技术和工具98 7.10文献评注98 7.10.1参考文献98 7.10.2Alonzo Church, 1903--199598 7.11练习98 8代数101 8.1引言101 8.2代数概念的形式定义101 8.3代数是如何产生的102 8.4代数的种类103 8.4.1具体代数103 8.4.2抽象代数104 8.4.3异构代数104 8.4.4泛代数105 态射概念105 特定种类的态射105 8.5规约代数106 8.5.1表达代数的句法方式106 8.5.2一个栈代数的例子106 一些 结构的非形式解释107 8.5.3一个队列代数的例子107 一些记法：\bf hide108 8.5.4“类”表达式的语义模型108 8.6代数规约的 句法109 8.6.1“类”表达式109 8.6.2“模式”声明109 8.7讨论110 8.7.1概述110 8.7.2原则、技术与工具110 8.8文献评注110 8.9练习111 9数理逻辑112 9.1要点112 9.1.1布尔基项语言113 9.1.2命题表达式语言113 9.1.3谓词表达式语言113 9.1.4布尔值表达式114 9.1.5“chaos” ------ 未定义的表达式求值114 9.1.6公理系统和推理规则114 公理和公理系统115 推理规则115 9.1.7证明系统115 9.1.8有关两个公理系统的注解116 9.1.9“if ... then ... else ... end” 联结词116 9.1.10讨论117 9.2证明论和模型论117 9.2.1句法117 9.2.2语义118 9.2.3句法和语义118 9.2.4形式逻辑：句法和语义118 关于形式逻辑系统的更多讨论119 关于形式逻辑系统句法的更多讨论119 关于实质蕴涵的意义，$\supset $119 元语言变量120 9.2.5和证明相关的问题121 证明121 定理和形式系统理论121 一致性121 可判定性121 9.2.6联系证明论和模型论121 解释122 模型122 可满足性、衍推：$\models $ 和永真123 可靠性和完全性，$\vdash $ 和 $\models $123 9.2.7讨论123 9.3布尔基项语言123 9.3.1句法和语义123 9.3.2联结词：$\sim $, $\wedge $, $\vee $, $\Rightarrow $, $=$, $\not =$, $\equiv $124 否定，$\sim $124 合取，$\wedge $124 析取，$\vee $125 相等，=125 蕴涵，$\Rightarrow $125 恒等，$\equiv $125 9.3.3三值逻辑125 $\equiv $\ 和 =126 推理规则的形式126 真值和假值的（句法）标志符以及语义值126 布尔联结词的非交换性127 9.3.4基项和它们的求值127 布尔基项的句法，BGT128 布尔基项求值， \sf \CJKfamily heiEval\_BGT129 9.3.5“句法” 和 “语义的语义”130 9.3.6讨论131 9.4命题逻辑语言131 9.4.1命题表达式， \sf \CJKfamily heiPRO131 命题表达式的例子131 命题表达式的句法， \sf \CJKfamily heiPRO131 9.4.2例子132 9.4.3命题求值， \sf \CJKfamily heiEval\_PRO133 9.4.4二值命题演算134 前言134 一些证明概念134 公理和一条推理规则，I135 公理和推理规则，II135 9.4.5讨论136 9.5谓词逻辑语言136 9.5.1动机136 9.5.2非形式介绍137 9.5.3例138 9.5.4量词和量化表达式140 句法140 自由和约束变量141 复合量化表达式141 9.5.5谓词表达式的句法， \sf \CJKfamily heiPRE142 谓词演算的符号142 一个谓词演算的项语言142 一个谓词演算的原子公式语言142 一个谓词演算的良构公式143 谓词表达式的非形式 BNF 语法143 9.5.6一个谓词演算143 公理模式144 推理规则144 9.5.7谓词表达式求值145 求值上下文145 谓词表达式的意义和值146 求值程序， \sf \CJKfamily heiEval\_PRE146 项求值146 公式求值146 9.5.8一阶和高阶逻辑147 9.5.9永真、可满足性和模型148 上下文和解释148 永真和可满足性148 模型149 上下文、解释和模型149 9.5.10讨论149 9.6公理系统149 9.6.1概述150 9.6.2公理150 9.6.3公理系统151 9.6.4一致性和完全性151 9.6.5面向性质的规约152 定义 \sf \CJKfamily heiS = A\bf -set 的形式公理系统概述154 定义 \sf \CJKfamily heiL = A$^\ast $ 的形式公理系统的概述155 分析句法156 合成句法157 9.6.6讨论157 9.7总结157 9.8文献评注158 9.9练习159 \contentsline part\ III\hskip \betweenumberspace 简单 \texttt RSL161 简单 \texttt RSL161 \vspace *2mm 概要161 \texttt RSL 与 \texttt VDM-SL、Z 以及 \texttt B161 句法上什么构成了规约162 一个关于\texttt RSL的“标准”162 \texttt RSL 工具163 10\texttt RSL 中的原子类型和值165 10.1引言165 10.1.1数学与企业建模165 10.1.2“原始的” 模型构造块166 10.2\texttt RSL\ 中的数166 10.2.1三种数的类型166 自然数： \sf \CJKfamily heiNat166 整数： \sf \CJKfamily heiInt166 实数： \sf \CJKfamily heiReal166 10.2.2\texttt RSL\ 中数的操作167 10.3枚举标记167 10.3.1动机167 10.3.2一般理论167 10.3.3标识上的操作169 10.3.4抽象模型中的枚举标记169 10.3.5用枚举标记来建模170 枚举标记和有限状态设备170 枚举标记和 Linux 命令171 10.4字符和文本171 10.4.1动机171 10.4.2字符和文本数据类型171 10.5标识符与一般标记172 10.5.1标识符172 \texttt RSL\ 标识符172 论域标识符173 10.5.2一般标记上的操作173 10.5.3一般标记173 10.6讨论174 10.6.1概要174 10.6.2对原子实体建模174 10.7练习175 11\texttt RSL 中的函数定义177 11.1函数类型177 11.1.1函数类型的句法177 11.1.2$\rightarrow $ 和 \unhbox \voidb@x \hbox $\mathrel \mathop \rightarrow \limits ^\sim $ 的非形式语义178 11.2面向模型的显式定义178 11.3面向模型的公理定义179 11.4面向模型的前置/后置条件定义 180 11.5面向性质的公理定义181 11.6面向性质的代数定义182 11.7\texttt RSL\ 函数定义风格的小结183 11.8讨论184 11.9练习184 12面向性质与面向模型的抽象186 12.1抽象187 12.1.1关键问题187 建模与模型187 12.1.2抽象与规约187 12.1.3论抽象188 \hbox to\hsize \hss ``\rm \CJKfamily kai抽象作为一种基本的工具。''\hss 188 12.2面向性质的抽象189 12.2.1面向性质的规约的语用189 12.2.2面向性质的规约的符号关系学190 非形式文档190 类型和值------非形式描述190 类型和值------形式描述190 操作：192 形式描述192 12.2.3面向性质的规约的语义193 12.2.4讨论193 概要193 原则，技术与工具193 12.3模型与性质抽象193 12.3.1表示与操作抽象194 12.3.2面向性质与面向模型的抽象194 关键问题194 进一步描述194 12.3.3定义195 12.3.4表示抽象的例子195 面向性质的表示196 面向模型的表示197 12.3.5操作抽象的例子198 面向性质的规约198 面向模型的规约200 12.3.6讨论200 概述200 详细说明： \CJKfamily kai``总之，区别到底是什么？''201 12.4面向模型的抽象201 12.4.1后续六章的一个极短概述201 12.4.2模型与模型202 面向性质的规约的模型202 面向模型的规约的模型202 12.4.3不充分规约202 重点202 为什么需要不充分规约？203 12.4.4确定性和不确定性203 确定性表达式203 不确定性表达式203 12.4.5为什么需要宽松规约204 12.4.6讨论204 概要204 数学结构的顺序204 \texttt RSL 语言结构204 12.5原则、技术与工具204 12.5.1面向性质与面向模型的规约205 何时面向性质205 何时面向模型205 12.5.2面向性质的规约的风格205 混合规约风格206 12.5.3面向模型的规约的风格206 混合规约风格207 12.5.4隐函数和显函数207 12.5.5请不要混淆！207 12.5.6有关观测器函数的注释208 第一个原则：假定208 第二个原则：不“自引用”208 第三个原则：标识209 [1] 集合元素标识209 [2] 固定结构元素标识210 [3] 序列元素标识210 12.6练习210 13\texttt RSL 中的集合212 13.1集合：关键问题213 13.2集合数据类型213 13.2.1集合类型：定义和表达式213 13.2.2集合值表达式214 集合的枚举214 集合值操作符/操作数表达式215 集合操作基调和例子215 集合操作符的数学含义216 集合内涵217 集合------确定性和非确定性的回顾218 集合 ------ 模型、值和 $\equiv $\ 操作218 13.2.3集合绑定模式与匹配219 13.2.4非确定性220 13.3基于集合的抽象的例子220 13.3.1表示 I220 13.3.2文件系统 I221 13.3.3表示 II222 13.4使用集合进行抽象和建模223 13.4.1网络建模223 扁平网络的叙述：223 扁平网络的形式化224 超网络的叙述224 超网络的形式化224 13.4.2伪层次建模225 单图的叙述225 单图的形式化225 超图的叙述225 超图的形式化225 13.4.3对电话系统的建模227 \CJKfamily kai状态的叙述227 \CJKfamily kai状态的形式化228 \CJKfamily kai有效状态的叙述228 \CJKfamily kai有效状态的形式化228 \CJKfamily kai用户动作的叙述228 动作类型的形式化228 题外话：类型并和变体记录229 叙述： \CJKfamily kai多方呼叫229 \CJKfamily kai多方呼叫的形式化229 叙述： \CJKfamily kai终止呼叫230 \CJKfamily kai终止呼叫的形式化230 叙述： \CJKfamily kai用户忙230 \CJKfamily kai用户忙的形式化231 13.5集合的归纳定义231 13.5.1集合类型的归纳定义231 13.5.2集合值的归纳定义232 13.6关于变化的集合的注释234 13.7原则、技术和工具235 13.8讨论236 13.9文献评注236 13.10练习236 14\texttt RSL 中的笛卡尔240 14.1笛卡尔：关键问题240 14.2笛卡尔数据类型241 14.2.1笛卡尔类型和笛卡尔表达式241 14.2.2笛卡尔值表达式242 14.2.3笛卡尔操作，I243 14.2.4笛卡尔绑定模式和匹配243 14.2.5笛卡尔操作，II244 14.3笛卡尔抽象的例子244 14.3.1文件系统 II244 14.3.2库拉托夫斯基（Kuratowski）：对和集合245 14.4用笛卡尔进行抽象与建模247 14.4.1句法结构建模247 叙述------句法（笛卡尔）范畴248 题外话------并类型操作符：$|$248 另一段题外话------笛卡尔文本类型248 形式化------句法（笛卡尔）范畴248 形式化------（笛卡尔的）良构性249 一条迂回之路：\texttt RSL“case”结构249 笛卡尔模式250 笛卡尔模式、拟合和绑定250 \hfill \texttt RSL\ \bf case 结构迂回之路的结束251 14.4.2笛卡尔“\bf let ... \bf in ... \bf end”绑定251 14.4.3语义结构建模252 叙述------语义类型252 程序点252 格局252 程序指针堆栈252 形式化------语义类型252 叙述------计算机程序解释253 形式化------语义函数253 14.4.4笛卡尔：初步的讨论254 14.5归纳笛卡尔定义255 14.5.1归纳笛卡尔类型定义255 14.5.2笛卡尔值的归纳定义255 14.6讨论257 14.6.1概述257 14.6.2原则、技术和工具258 14.7练习258 15\texttt RSL\ 中的列表262 15.1与列表相关的一些观点262 15.2列表数据类型263 15.2.1列表类型263 15.2.2列表值表达式264 列表的枚举264 列表值操作符/操作数表达式265 操作符基调及其非形式的含义：265 列表操作的操作式及非形式定义：265 列表的内涵266 15.2.3列表的绑定模式与匹配267 15.2.4列表：确定性和非确定性的回顾268 15.3基于列表的抽象的小例子268 15.3.1表示268 15.3.2堆栈和队列269 15.3.3文件系统 III270 15.3.4排序算法272 15.4使用列表进行抽象与建模273 15.4.1使用列表对书进行建模273 实体叙述273 形式化274 操作叙述274 形式化274 15.4.2“上下文中的关键字（KeyWord-In-Context，KWIC）”的建模274 给定的问题：275 非形式问题描述的讨论：275 一些辅助函数：276 模型：277 15.5列表的归纳定义279 15.5.1列表类型的归纳定义279 15.5.2列表值的归纳定义280 15.6列表抽象和模型的回顾281 15.7列表：讨论282 15.8练习282 16\texttt RSL 中的映射286 16.1关键问题286 16.2映射数据类型287 16.2.1映射类型：定义和表达式287 16.2.2映射值表达式288 映射的枚举288 确定的和非确定的映射值288 映射操作符/操作数表达式288 \textup \CJKfamily kai映射操作基调和例子289 \textup \CJKfamily kai映射操作符的含义289 映射的内涵290 16.2.3映射的绑定模式与匹配291 16.2.4非确定性292 16.3基于映射抽象的例子292 16.3.1排序292 16.3.2等价关系292 16.4使用映射进行抽象与建模293 16.4.1图293 16.4.2结构化的表295 \textup \CJKfamily kai描述 ------ 类型295 \textup \CJKfamily kai形式化 ------ 类型296 \textup \CJKfamily kai描述 ------ 不变式296 \textup \CJKfamily kai形式化 ------ 不变式296 16.4.3层次结构297 \textup \CJKfamily kai描述 ------ 层次结构297 \textup \CJKfamily kai形式化 ------ 层次结构297 \textup \CJKfamily kai描述 ------ 路径298 \textup \CJKfamily kai形式化 ------ 路径298 \textup \CJKfamily kai描述 ------ 路径操作299 \textup \CJKfamily kai形式化 ------ 路径操作299 16.4.4关系文件系统 (IV) 和数据库300 16.4.5复杂指针数据结构303 讨论312 16.4.6数据结构的良构性312 讨论315 16.4.7讨论316 16.5映射的归纳定义316 16.5.1映射类型的归纳定义316 16.5.2映射值的归纳定义317 16.6映射抽象和建模的回顾319 16.7映射：讨论321 16.8练习321 17\texttt RSL\ 中的高阶函数325 17.1函数：关键问题325 17.2使用基于函数的抽象的例子326 17.2.1泛函326 17.2.2讨论327 17.3用函数进行抽象与建模327 17.3.1函数作为概念327 句法类型327 语义类型：328 语义确立函数328 高阶函数作为指称329 17.3.2操作符提升330 操作符提升的例子330 描述与分析：类型331 形式化：类型332 描述：操作333 讨论335 描述：提升的函数335 形式化：提升的函数336 17.4函数的归纳定义336 17.4.1函数类型的归纳定义336 17.4.2函数值的归纳定义337 17.5函数抽象与建模的回顾337 17.6讨论338 17.7练习338 \contentsline part\ IV\hskip \betweenumberspace 规约类型339 规约类型339 18\texttt RSL 中的类型341 18.1关键问题341 18.2类型范畴342 18.2.1抽象类型：分类342 18.2.2具体类型342 18.2.3讨论343 18.3枚举标记类型的回顾343 18.4记录：构造器和析构器344 18.4.1概要344 18.4.2变体记录值的归纳公理345 非递归记录类型的定义345 递归记录类型的定义345 18.4.3一个例子346 18.5联合类型的定义347 18.6短记录类型的定义347 18.7类型表达式，回顾348 18.8子类型348 18.9类型定义，回顾349 18.10关于递归类型定义349 18.11讨论349 18.11.1概要349 18.11.2原则、技术和工具350 18.12文献评注350 18.13练习350 \contentsline part\ V\hskip \betweenumberspace 规约程序设计353 规约程序设计353 \vspace *2mm 关于规约程序设计353 关于问题与练习354 19应用式规约程序设计355 19.1作用域与绑定355 19.1.1绑定模式 ------ 非形式说明356 19.1.2“let” 结构的作用域和绑定 [1\hbox ]357 19.1.3函数定义作用域与绑定[2\hbox ]358 19.1.4“case”结构的作用域和绑定[3\hbox ]358 19.1.5内涵：作用域和绑定[4\hbox ]359 19.1.6量化：作用域和绑定 [5\hbox ] 360 19.2直观理解360 19.2.1简单“let \textrm a = $\mathcal E_d$ in $\mathcal E_b$\textrm (a) end”360 19.2.2递归“let\ \textrm f(a) = $\mathcal E_d$\textrm (f) in\ $\mathcal E_b$\textrm (f,a) end”360 19.2.3直谓 “let\ \textrm a:A $\bullet \ \mathcal P$\textrm (a) in\ $\mathcal E$\textrm (a) end”361 19.2.4多个 ``let\ \textrm a$_i$ = $\mathcal E_d_i$ in\ $\mathcal E_b$\textrm (a$_i$) end''361 19.2.5文字和标识符362 文字362 标识符362 19.3操作符/操作数表达式362 19.4枚举和内涵表达式363 19.5条件表达式363 19.6绑定、确定类型、模式和匹配365 19.6.1问题365 句法便利问题365 19.6.2绑定和模式的本质366 绑定366 模式366 绑定和模式：明显的不同366 绑定和确定类型367 19.6.3绑定模式367 较早内容回顾367 记录绑定模式368 绑定模式的一般形式369 \rm 注释371 \rm 进一步的介绍371 19.6.4给定类型371 19.6.5选择模式和绑定372 注释373 一些观察377 19.6.6总结378 19.7回顾和讨论378 19.7.1概述378 19.7.2原则和技术378 19.8文献评注379 19.9练习379 20命令式规约程序设计388 20.1直观理解388 20.2命令式组合子：一个 演算389 20.2.1[0] “变量”声明389 20.2.2[1] 赋值: “var := expression”391 20.2.3[9] 状态表达式391 20.2.4[2] “skip”: 无动作 391 20.2.5[3] 语句序列 (;)391 20.2.6[4] ``if ... then ... else ... end''391 20.2.7[5--6] ``while ... do ... end''和 ``do ... until ... end''392 20.2.8[7] ``case ... of ... end''392 20.2.9[8] ``for... in ... do... end''392 20.3变量引用：指针393 20.3.1简单引用的介绍393 20.3.2动态分配和引用393 直观理解394 位置和值的类型395 存储不变式395 语义操作396 句法形式396 语义397 20.3.3讨论：先语义，后句法398 20.3.4讨论：类型同态398 20.3.5状态的概念398 20.4函数定义和表达式399 20.4.1\bf Unit 类型表达式， I399 20.4.2命令式函数399 20.4.3读/写访问描述400 20.4.4局部变量400 20.4.5\bf Unit 类型表达式， II400 20.4.6纯表达式401 20.4.7只读表达式401 状态量化 ($\Box $)402 20.4.8等价 ($\equiv $) 和相等 (=)402 等价 （$\equiv $）402 条件等价403 相等 （=）403 20.5转化：应用式到命令式403 20.5.1应用式到命令式的转化403 20.5.2递归到迭代的转化404 20.5.3应用式到命令式的模式405 模式406 20.5.4正确性、原则、技术、工具412 20.6配置建模的风格412 20.6.1应用式上下文和状态412 句法和语义类型412 \textup \CJKfamily kai句法类型413 \textup \CJKfamily kai语义类型：413 辅助函数413 简单解释函数414 复合解释函数414 上下文创建解释函数414 总结、应用式上下文和状态415 20.6.2应用式上下文和命令式状态416 元状态和辅助函数416 简单解释函数416 复合解释函数417 上下文创建解释函数417 总结、应用式上下文和命令式状态418 20.6.3命令式上下文和状态418 元状态418 辅助函数419 简单解释函数419 复合解释函数419 上下文创建解释函数420 总结、命令式上下文和状态420 20.6.4顺序模型的总结421 20.7回顾和讨论421 20.7.1回顾421 20.7.2讨论421 20.8文献评注422 20.8.1计算理论422 20.8.2$\lambda $ 演算的类型理论422 20.8.3源程序转换著作422 20.8.4命令式程序设计原理423 20.9练习423 21并发式规约程序设计426 21.1行为和进程抽象427 21.1.1引言427 21.1.2关于进程和其他的抽象427 21.2直观介绍428 21.2.1说明性的会合场景428 模式的“会合”规约1--2--3430 模式的“会合”规约 4431 21.2.2图和记法总结431 21.2.3关于迹语义432 21.2.4一些描述：进程，等等433 21.2.5进程建模原则434 构件 $\equiv $进程434 21.2.6非形式的例子435 21.2.7一些建模评论------题外话439 21.2.8例（续）439 21.2.9一些系统的通道格局441 21.2.10并发概念------总结441 21.3通信顺序进程，CSP443 21.3.1导言：进程和事件443 21.3.2进程组合子等等444 \bf stop：基本进程444 前缀444 定义444 $\unhbox \voidb@x \hbox $\delimiter "4264306 \tmspace -\thinmuskip .1667em\delimiter "5265307 \tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace -\thinmuskip .1667em\tmspace +\thickmuskip .2777em\delimiter "4262304 \tmspace -\thinmuskip .1667em\delimiter "5263305 $$： 外部非确定性选择444 $\unhbox \voidb@x \hbox $\delimiter "4264306 \tmspace -\thinmuskip .1667em\delimiter "5265307 $$：内部非确定性选择444 CSP 定律 （I）445 复合事件445 输入和输出445 \unhbox \voidb@x \hbox $\parallel $：并行组合446 共享事件446 CSP 定律（II）446 21.3.3讨论447 21.4\texttt RSL/CSP 进程组合子447 21.4.1类 \texttt RSL 通道447 21.4.2\texttt RSL 通信子句448 简单输入/输入出子句448 21.4.3\texttt RSL 进程448 简单进程定义448 进程及其定义449 进程调用449 数组通道进程定义450 21.4.4并行进程组合子450 21.4.5非确定性外部选择451 21.4.6非确定性内部选择451 21.4.7互锁组合子451 21.4.8总结452 21.4.9提示452 21.5翻译模式452 21.5.1阶段 I：应用式模式453 21.5.2阶段 II：简单重构453 21.5.3阶段 III：引入并行453 21.5.4阶段IV：简单重构454 21.5.5阶段关系455 21.5.6阶段 V：命令式重构455 21.5.7一些评论456 21.6并行和并发：讨论456 21.6.1\texttt CSP 和 \texttt RSL/CSP456 21.6.2建模技巧456 21.7文献评注457 21.8练习457 其他463 其他463 22其他465 22.1我们讨论了什么465 22.2下一个讨论什么465 22.3下一个的下一个讨论什么465 22.4提示466 22.5 \CJKfamily kai“轻量级”形式方法467 22.6文献评注467 \contentsline part\ VII\hskip \betweenumberspace 附录469 附录469 A共同练习题目471 A.1运输网络471 A.2集装箱物流471 A.3金融服务行业472 A.4练习参考总结473 B术语表474 B.1参考列表的种类475 B.1.1术语475 B.1.2词典475 B.1.3百科全书475 B.1.4本体论475 B.1.5分类学475 B.1.6术语学476 B.1.7类属词典476 B.2印刷格式和拼写476 B.3术语表476 \contentsline chapter参考文献545 样章： 023236-01.pdf 课件： 网络资源： 配套教学用书（配套教参、主课本等）： ·软件工程卷2：系统与语言规约 ·软件工程卷3：领域、需求与软件设计 可替代教学用书： 丛书名称：世界著名计算机教材精选 图书书评：

【欢迎来稿】 总编办：c-service@tup.tsinghua.edu.cn  【选题意向登记表】

客户服务：（010）62776969 c-service@tup.tsinghua.edu.cn

教师服务电话：010-62770175-3506

反盗版举报电话：(010) 62782989 bairsh@tup.tsinghua.edu.cn

质量反馈：(010) 62772015 zhiliang@tup.tsinghua.edu.cn

邮购电话：(010) 62786544 e-sale@tup.tsinghua.edu.cn

邮购地址：北京市海淀区清华大学出版社邮购组收 邮编:100084

读者服务部（购书）：(010) 62781733

通讯地址：清华大学学研大厦 A 座 邮编：100084

网管信箱：netadmin@tup.tsinghua.edu.cn

版权所有(C)2005 清华大学出版社有限公司

Copyrights @ 2005 by Tsinghua University Press. All Rights Reserved 京ICP备 05029640 号