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 比較各種記號。