《软件工程卷1～3》是冯诺依曼奖章获得者、世界著名的计算机科学家Dines Bjorner教授的最新著作。这套丛书为读者理解软件和软件开发过程提供了一个“全新的视角”。这三卷书首次系统地论述了如何用形式方法来指导领域工程、需求工程和软件设计，即软件工程的三个相互关联并重叠的组成部分，或称之为软件工程的“三部曲”。在软件开发的各个阶段，如果都能够采用这种形式化的开发模式，将能够在极大程度上保证软件开发的正确性和有效性。
　　这套丛书可以被视为软件工程史上里程碑式的著作。作者通过长达30年的程序设计方法论的研究与实践，加上长达25年不断完善的课程讲义汇编成这一套前后连贯、内容一致以及相对完整的软件工程著作。这套丛书的一个显著特点就是在这三卷书中，所有的原理、技术和工具都是通过大量的案例分析来进行阐述，并覆盖了所有主要的软件开发时期、阶段和步骤；同时，这些原理、技术和工具是能够应用在大型工业和商业软件的开发项目中去的。
　　这套丛书不但可以作为高校计算机专业学生、教师以及研究人员的教材和必备参考书，而且在工业和计算机产业界也具有极大的实用价值。
　　《软件工程卷1：抽象与建模》介绍了抽象与建模的基本原理和技术。首先，本卷给出了离散数学的基本介绍，包括数、集合、笛卡尔、类型、函数、入-演算、代数和数理逻辑，然后讲授基本的面向属性与面向模型的规约的基本原理和技术。一些其他的规约语言，比如B、VDM-SL和Z都具有面向模型的概念，本卷则通过RAISE规约语言RSL来讲解这个概念。本卷还介绍了有关应用式（函数式）、命令式和并发式（并行式）规约程序设计的基本原则。最后，本卷给出了一个全面的软件工程术语表以及大量的索引和参考文献。
　　《软件工程卷2：系统与语言规约》介绍了描述系统与语言的规约的基本原理和技术。首先，本卷讲授一些高级的原理和技术：分层与组合、指称与计算以及构型：环境与状态的抽象与建模，然后讲授符号学建模的基本原理和技术：语用、语义以及系统和语言的句法。其中重要的一部分介绍了对空间和简单时态现象进行建模的基本原理和技术。本卷的主要章节用于介绍一些专门的主题，比如模块（包括UML的类图）、Petri网、活动序列图、状态图和时态逻辑（包括时段演算）。最后，本卷介绍了开发函数式，命令式以及并行程序设计语言的可靠和有效的解释器和编译器的基本原理和技术。本卷适合于作为高年级本科生和研究生，以及研究程序设计方法学的学者的教材或参考书。
　　《软件工程卷3：领域、需求与软件设计》介绍了整体软件开发的基本原理和技巧：从领域描述，经过需求分析，直到软件设计。本卷倡导一种全新的软件工程开发模式：在需求被形式化之前，人们必须理解应用领域，因此本卷首先介绍领域描述的原理和技术，然后介绍从领域模型导出需求规则的原理和技术，最后介绍细化需求到软件设计的原理和技术：体系结构和组件设计。

　　1绪论
　　1.3.5分析文档特性描述：分析文档，通过其我们指其对象为描述文档的文档。分析文档的文本分析一个描述文档。
　　如该术语所示，分析文档是其内容为其他文档（这里是描述文档）的分析的文档。我们考虑四种分析文档：那些表示以下内容的文档（i）（在头脑风暴中）来自于粗略描述的概念的形成，（ii）形式和非形式描述文档的确认，（iii）描述性质验证，和（iv）开发变迁（即开发步骤）正确性验证。
　　可能有其他的分析文档。例如：其内容是分析所需计算系统行为方面的文档，比如基于排队理论研究所预期的接口反应时间；基于复杂度理论研究所预期的机器计算时间；基于引用模式的统计研究的字典或数据库散列算法的细节等等。也可能包括有内容为分析实际问题的文档，比如项目和生产规划、监测和控制计算系统的基于统计研究的生产线流程（拥塞）；金融服务或电子交易计算系统的基于类似研究的公司现金流等等。可以设想其他种类的分析文档。在这几卷中，我们将只考虑那些提及的文档。粗略描述分析和概念形成
　　在描述一个领域、规定某需求或规约某软件设计中，最为重要的任务就是识别论域发展所围绕的核心概念。一方面，领域中的这些现象是所想要的在软件或软件程序结构（数据结构、程序等等）中的工具。另一方面在现实世界中的这些现象，这些（将在所需软件中显现出来的）工具或程序代码结构将（对于该领域来说）被概念化，或者当它们作为需求获取出来或存在于软件代码中时，实际上它们就是概念（抽象观念）。
　　因此我们了解了从通常可触知现象的具体的、显然的、现实的世界到概念的抽象、可理性感知但通常无形的世界的变迁。从可感知的事物，通过可想象的事物，到达“做进”软件中的事物，我们需要记录的正是这一变迁。
　　对于领域，我们这样做是通过首先进行头脑风暴，也就是说，通过粗略地描述领域描述，并且由此通过分析来识别领域概念。然后，对于需求，通过构想来这样做。其中通过粗略地描述需求“规定”，并且由此通过分析来识别需求概念。最后对于软件我们通过“角色分配”，也就是说，通过粗略的描述软件“设计”，并且由此通过分析来识别适当的软件结构。
　　以形成概念为目标的分析是一门艺术。恐怕最难学习的事情就是正确地对其进行处理，或者至少通过某种方式来处理，其中会出现令人高兴、优雅和实用的概念。但是阅读许多分析示例可能会有所帮助。因此第3卷的第13、21章给出了分析和概念形成的例子、原则和技术，它们对于进行上述所示的分析来说非常有用。

原著作者为中文版所作的序
译者序
前言
丛书成因
丛书的不足
着手方法
软件新观
“轻量级”形式技术
“超级程序设计师
何为软件工程
作者的愿望
这几卷在软件工程教育课程中的作用
为什么这么多材料
课程中如何使用这套丛书
本书的简要介绍
本卷的简要介绍
致谢

开篇
绪论
1.1 准备
1.2 软件工程三部曲
1.2.1 软件和系统开发
1.2.2 三部曲引出
1.2.3 领域工程
1.2.4 需求工程
1.2.5 软件设计
1.2.6 讨论
1.3 文档
1.3.1 文档种类
1.3.2 时期、阶段和步骤文档
1.3.3 信息文档
1.3.4 描述文档
1.3.5 分析文档
1.4 形式技术和形式工具
1.4.1 关于形式技术和语言
1.4.2 软件工程教材中的形式技术
1.4.3 一些程序设计语言
1.4.4 一些形式规约语言
1.4.5 目前形式语言的不足
1.4.6 其他的形式工具
1.4.7 为什么要形式技术和形式工具
1.5 方法和方法学
1.5.1 方法
1.5.2 方法学
1.5.3 讨论
1.5.4 元方法学
1.6 软件基础
1.6.1 教学法和范式
1.6.2 语用、语义和句法
1.6.3 规约和程序设计范式
1.6.4 描述、规定和规约
1.6.5 元语言
1.6.6 总结
1.7 目标和效果
1.7.1 目标
1.7.2 效果
1.7.3 讨论
1.8 文献评注
1.9 练习

离散数学
数
2.1 引言
2.2 数符和数
2.3 数的子集
2.3.1 自然数：Nat
2.3.2 整数：Int
2.3.3 实数：Real
2.3.4 无理数
2.3.5 代数数
2.3.6 超越数
2.3.7 复数和虚数
2.4 类型定义：数
2.5 总结
2.6 文献评注
2.7 练习
集合
3.1 背景
3.2 数学的集合
3.3 特殊集合
3.3.1 外延公理
3.3.2 划分
3.3.3 幂集
3.4 分类和类型定义：集合
3.4.1 集合抽象
3.4.2 集合类型表达式和类型定义
3.4.3 分类
3.5 RSL中的集合
3.6 文献评注
3.7 练习
笛卡尔
4.1 要点
4.2 笛卡尔值表达式
4.3 笛卡尔类型
4.4 笛卡尔的目
4.5 笛卡尔的相等
4.6 一些构造的例子
4.7 分类和类型定义：笛卡尔
4.7.1 笛卡尔抽象
4.7.2 笛卡尔类型表达式和类型定义
4.8 RSI.中的笛卡尔
4.9 文献评注
4.10 练习
类型
5.1 值和类型
5.2 现象和概念类型
5.2.1 现象和概念
5.2.2 实体：原子和复合
5.2.3 属性和值
5.3 程序设计语言类型概念
5.4 分类或抽象类型
5.5 内建和具体类型
5.6 类型检查
5.6.1.类型确定的变量和表达式
5.6.2 类型错误
5.6.3 类型错误检测
5.7 类型作为集合，类型作为格
5.8 总结
5.9 练习
函数
6.1 概述
6.2 要点
6.2.1 背景
6.2.2 一些函数概念
6.3 数是如何产生的
6.4 关于求值概念的题外话
6.4.1 求值，解释和细化
6.4.2 两个求值的例子
6.4.3 函数调用
6.5 数代数
6.5.1 代数
6.5.2 数类型
6.5.3 高阶函数类型
6.5.4 非确定性函数
6.5.5 常量函数
6.5.6 严格函数
6.5.7 严格函数和严格函数调用
6.5.8 数上的操作
……
简单RSL
规约类型
规约程序设计
其他
附录
参考文献