Software abstractions. : logic, language, and analysis (rev. ed.). By Daniel Jackson
The MIT Press Cambridge, MA, 2012, 376 pp., ISBN 0262017156.
CR Rev. No. 140359
In a Scientific American article [1] from around the time of this seminal book’s original edition [2], the author stated:
Managers involved in high-profile software blowouts could claim in their defense that they followed standard industry practices, and unfortunately they would be right. Developers rarely articulate their designs precisely and analyze them to check that they embody the desired properties.
The present, revised edition of this latter-day classic is as outstanding and definitive in its approach to the design problem as was the original, only more so (to use a Rick Blaine formula from the timeless film Casablanca). The book and its central subject, the Alloy 4 language, are the foundation and virtually unique occupants of a formal methods niche that I had originally thought impossible: lightweight formal methods that compete on equal terms in many contexts with the elaborate, heavy variety. There now exist a plethora, if not a virtual Tower of Babel, of effective heavyweight formal methods of both the theorem proving [3] and model checking [4] variety. In light of this, Alloy’s promise extends, unlike that of the heavy machinery, to greater pervasiveness of formal modeling and verification among designers and developers.
The book consists of six chapters—“Introduction,” “A Whirlwind Tour,” “Logic,” “Language,” “Analysis” (that is, what the Alloy analyzer does given an Alloy text or model), and “Examples”—and five appendices—“Exercises,” “Alloy Language Reference,” “[Alloy 4] Kernel Semantics,” “Diagrammatic Notation,” and “Alternative Approaches” (that is, heavyweight methods such as B, object constraint language (OCL), Vienna development method (VDM), and Z).
The author identifies his intended audience as “software designers, whether they call themselves requirements analysts, specifiers, designers, architects, or programmers.” This characterization displays the author’s great clarity of expression, in this instance born of avoiding verbal clutter by nonessentials. (Compare this with conventional job descriptions in these purportedly separate callings.) It is quite instructive for the author to state (or admit) that “model,” that most overused word of our profession, was chosen for its vagueness. Theorem proving (syntactic) and model checking (semantic)—what may be termed the two antipodes of formal methods—assign different meanings to the term. However, model checking was the “original inspiration” of the Alloy analyzer, which later was complemented by Boolean constraint satisfaction (SAT) solvers.
Alloy’s logic is that of relations—a relation being the conventional mathematical set of tuples. As one learns and confronts the syntax of Alloy models, it is useful to remember the author’s explanation that Alloy comprises one logic that is expressible in three styles: predicate calculus style, navigation style, and relational calculus style. One model can contain instances of all three. This gives the correct impression that Alloy is very rich, though everything is constructed from atoms and (their) relations. In getting the hang of Alloy, users must master notations and notions such as {(a)} standing for any of a, {a}, (a), and itself.
I hasten to add that it is, to say the least, worth it. The book, though relatively short, imparts some deep insights: “Predicate calculus lacks transitive closure, so reachability properties can’t be expressed [in it].” “Is equality structural equality or reference equality?” The book has the answer: “A relation has no identity distinct from its value[.] ... If two relations have the same set of tuples ... they’re just one and the same relation.” The author points out that equality cannot be represented as a first-order relation. Also, the keyword “in,” which contextually stands for either “is an element of” or “is a subset of” was “carefully chosen for its ambiguity.” This last comment is very helpful regarding motivation. The exposition is honest; there is no salesmanship. The Alloy road to writing what one means to express using, for example, quantifiers versus multiplicities is not a royal one: one x : Line | cache’ = cache - x versus some x : Line | cache’ = cache - x.
Sections 4.5, on Alloy facts, predicates, functions, and assertions, and 5.1.3, on Alloy’s fundamental small-scope hypothesis (which justifies exhaustive search for (counter) examples within a finite scope), effectively summarize the essentials. They can be peeked at with profit before one gets to them through a sequential reading of the whole book. The examples are up to par with the rest of the book. The Alloy model of leader election in a ring topology communication network can, as it happens, be compared with that of Event-B [3], an excellent heavyweight theorem-proving tool.
Ensuring that “what you write down means what you think it means” is the abiding challenge to designers. The book and its associated Web site of tutorials, examples, models, and downloads (including Alloy 4 itself, of course) will furnish designers with a rigorous and expressive but agile way of effecting that most important of features: correctness. It has my highest recommendation.
Reviewer: George Hacken (Wayne, NJ)
REFERENCES
[1] Jackson, D. Dependable software by design. Scientific American 294 (June 2006), 68-75. http://dx.doi.org/10.1038/scientificamerican0606-68.
[2] Jackson, D. Software abstractions: logic, language and analysis. MIT Press, Cambridge, MA, 2006.
[3] Abrial, J.-R. Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge, MA, 2010.
[4] Ben-Ari, M. Principles of the Spin model checker. Springer, London, UK, 2008.
Comments