01 / 导读
导读
引用
Jackson, D. (2012). Software Abstractions: Logic, Language, and Analysis (revised ed.). MIT Press.
章节概要
本书（约 375 页）介绍 Alloy，一种基于关系逻辑的建模语言，以及能自动检查模型的 Alloy Analyzer。书中的论点是：软件开发的核心是抽象的设计，而代码并不适合用来探索抽象——可执行性带来无关的细节，设计时看不到的缺陷到编码时就变得显而易见。Alloy 提供了一种便于表达的记号和一种能立即给出反馈的分析。作者把这种方法称为“轻量级形式化方法”：像传统形式化规约那样使用小而简单的记号，但以完全自动的分析取代定理证明。修订版针对 Alloy 4 更新了正文、示例和附录。第1章是简短的引言，第2至5章讲授语言，第6章给出较大的示例，之后是五个附录。
第1章：引言
本章论证软件建立在抽象之上，对未经检验的抽象抱有一厢情愿的想法是常见的失败原因，而补救办法是借助可分析的记号，直接着手抽象的设计。它与那些把设计作为独立阶段取消的方法作了对照。
第2章：快速浏览
以一个扩展示例——通讯录——分阶段构建。本章先探索状态（静态），再加入操作（动态）、分类层次和执行轨迹，使读者在了解细节之前先看到模拟—检查—改进的整个工作流程。
第3章：逻辑
本章展开语言所依据的逻辑。它介绍“三种逻辑合一”、原子与关系、快照、运算符、约束、声明与重数约束，以及基数与整数。
第4章：语言
本章从“自己的祖父”（self-grandpas）示例出发，讲述签名（signature）与字段、模型图、类型与类型检查、事实、谓词、函数与断言、命令与范围、模块与多态，以及整数与算术。
第5章：分析
本章从用户的角度说明 Analyzer 如何工作：范围完备的分析、实例、样例与反例、无界全称量词问题，以及范围的选择与单调性。前言说明，Analyzer 把约束翻译成布尔约束，交给现成的 SAT 求解器。
第6章：示例
四个较大的模型：环上的领导者选举、酒店房间门锁、媒体资产管理和内存抽象。
附录 A–E
附录 A 是习题：逻辑习题、扩展简单模型、经典谜题、元模型、小型案例研究和开放式案例研究。附录 B 是语言参考（词法问题、语法、优先级、语义、类型与重载、语言特性、关系表达式、整数表达式和布尔表达式）。附录 C 给出 Alloy 内核的语义，附录 D 讲图示记号，附录 E 以酒店门锁问题比较其他方法（B、OCL、VDM 和 Z）。
核心概念
第1–2章：抽象与工作流程
- 软件抽象：化简到本质形式的结构，本书视之为设计的核心。
- 轻量级形式化方法：精确的记号加完全自动的分析，逐步构建。
第3–4章：逻辑与语言
- 关系逻辑：以集合与关系作为模型唯一的构造材料。
- 签名与字段：模型声明对象种类及其之间关系的方式。
- 事实、谓词、函数、断言：书写模型和命题所用的约束形式。
- 命令与范围：要求 Analyzer 运行或检查什么，以及在什么界限内。
第5章：分析
- 范围完备的分析：对直到给定规模的所有情形做穷尽检查。
- 实例与反例：模型的一个例子，或对断言的违反，以可视化方式展示。
- 无界全称量词：对无界集合的量词，受范围限制的分析无法完全覆盖；第 5.3 节讨论这一问题。
评析
优点
- 关于设计的清晰主张。 前言和第1章论证了为什么要尽早、明确地关注抽象，书名点明了这一主题。
- 在反馈中学习。 前言描述了借助 Analyzer 逐步构建模型的过程：边模拟边检查，得到即时的可视化反馈，并体验到发现自己模型中错误的感觉。
- 循序渐进的路径。 先有快速浏览，再讲逻辑和语言各章，读者先看到工作流程。附录给出六类习题，从逻辑习题到开放式案例研究。
- 完整的案例与模型。 第6章为四个系统建模，书的网站可下载全部模型。
- 评论。 George Hacken（《Computing Reviews》）因其示例和习题而对本书给予最高推荐；Anthony Sloane（《Journal of Functional Programming》）写道，像 Alloy 这样的系统应当出现在所有软件设计者和开发者的工具箱中。
局限
- 工具版本。 修订版与 Alloy 4 兼容；Alloy 网站现在列出一本较新的在线书《Practical Alloy》，涵盖时序建模等 Alloy 6 的特性。
- 有界分析。 该方法检查直到给定范围的每种情形，因此通过检查的模型并不能证明在任意规模下都正确；第5章用专门的小节讨论无界全称量词和范围的选择。
- 需要逻辑基础。 内容建立在集合、关系和一阶逻辑之上，适合熟悉离散数学的读者。
- 针对设计模型而非程序。 模型描述的是设计而不是代码；与其他规约方法的比较仅限于附录 E，它在酒店门锁问题上把 Alloy 与 B、OCL、VDM 和 Z 并列比较。
在课程中的定位
这是软件工程书单中的形式化方法之书。《A Philosophy of Software Design》是一本关于通过深模块和信息隐藏管理复杂性的短书；它与 Jackson 一样关注抽象，但表达为实用建议。《Software Architecture in Practice》讲真实项目中的架构与质量属性；Sommerville 的《Software Engineering》是跟随系统整个生命周期的综合入门；《The Pragmatic Programmer》是实用习惯的汇编；《Software Engineering at Google》解释一个大型组织如何长期维持软件。
当你对软件工程有了整体认识，并希望以严格的方式在构建之前检查一个设计时，读《Software Abstractions》。它是对那些实用书籍的补充，而不是替代。
如何使用本书
本书适合熟悉集合、关系和一阶逻辑并有一些软件设计经验的读者。本书网站上的推荐语描述的读者范围从实际从业者到研究人员。
实用安排：
- 第一遍： 第1章、第2章的快速浏览和讲语言的第4章；安装 Alloy Analyzer，并运行网站上的书中模型。
- 核心： 第3章（逻辑）与第4章并读，然后读第5章，了解如何解读分析结果和选择范围。
- 应用： 至少把第6章中的一个模型做完并加以修改（酒店房间门锁正是附录 E 用来比较各种记号的问题）。
- 练习： 做附录 A 的习题，从逻辑习题推进到小型案例研究；把附录 B 当作语言参考，用附录 E 比较各种记号。