Browse Books

Reviewer: George Hacken

Software abstractions (SAs), as implemented in the author's (and his colleagues') Alloy modeling language, are in my opinion a milestone in rendering verification more easily practicable. From the author's preface: "Simplicity of design means addressing the essence of design-the abstractions on which software is built-explicitly and up front." The Alloy language is used to write declarative models of a system that specify what a system is supposed to do (or in effect not to do), not how it should do it. Jackson mentions two traditional obstacles to formal specification's appeal: intimidating mathematical syntax, and the "lack of tool support beyond type checking and pretty printing." Alloy's greater practicability, as compared with the heavy investment of effort required even by today's theorem-prover-based formal methods, stems from its admittedly incomplete (because finite) automatic analysis, which nevertheless has a huge, prescribable coverage (scope) that test-case coverage cannot begin to approach, and which gives immediate feedback (the other half of enhanced practicability). Regarding test cases, "an assertion [which is an Alloy language construct] is rarely more trouble to write than a single test case, but has the coverage of an unimaginably huge test suite." Alloy's ASCII-based keywords and symbols (& for intersection, + for union), a seemingly small feature, prevent the last-minute annoyances of strange printouts and displays of Alloy model texts. Jackson's book delivers on a promise born of Sir C.A.R. Hoare's famous Turing Award quotation: "There are two ways of constructing a software design: One way is to make it so simple there are obviously no deficiencies and the other way is to make it so complicated that there are no obvious deficiencies." The book is a substantive, philosophical (in the good sense, that is, well-grounded) adjunct to the publicly available Alloy toolkit, documentation, and tutorial (http://alloy.mit.edu), and should be read as such-though it certainly passes muster as standalone reading. The book's audience comprises "analysts, specifiers, designers, architects, or programmers," and its level is that of advanced undergraduates and up, though the only explicit prerequisite is "familiarity with the basic notions of set theory." (Those who have assimilated more-than-naïve set theory will be asked to get used to the nuance that sets "are" unary relations-a small price to pay.) Though I dare say that all software practitioners who have ever been within earshot of Hoare's truth agree with it in principle, the road to realization of correctness has been found to be a winding one indeed, complete with rather steep grades through heavy formal methods territory. Jackson, very much in the thick of formal methods (FM) since the 1980s and knowledgeable in its various species (theorem proving, model checking, and constraint satisfaction), modestly refers to his approach as "lightweight formal methods." Although model checking was the Alloy Analyzer's "original inspiration," its analysis renders constraints to be solved as Boolean constraints and passes these to one of several satisfiability (SAT) solvers imported into the Alloy toolkit. Page 150 has an excellent explanation of the role of SAT solvers. Chapter 2, "A Whirlwind Tour," asks the reader not to "expect to follow all the details." The tour is one of an email client model, and covers (some) keywords, states, operations, and traces. The service that this well-characterized tour renders is to exhibit the look and feel of Alloy, and to impart a slightly-above-nodding acquaintance with such keywords as "sig"[nature], "lone" [zero or one], "pred"[icate], "some", and "check." Given that chapter 2 is, along with the rest of the book, a static presentation of Alloy's text and graphics, and assuming the reader can tolerate less-than-full comprehension, the tour achieves its goal. It is, of course, better to take the tour and interleave it with sessions at the Alloy Web site. My favorite detailed example (beginning on page 203) is titled "Media Asset Management," and involves the management of your photo albums and other digitized media and their ancillary files. The example resonated with my gradually developed impatience with many off-the-shelf, do-everything-for-you tools. A quotation is worth a thousand words: "Although I'd used (and been impressed by) [CommercialTool] for several years, when I constructed this [Alloy] model, [it became clear that] I hadn't understood the details of the basic functions." The discussion (question-and-answer) sections at the end of each chapter are very informative; they serve to enrich the reader's understanding by elaborating on design decisions, such as skolemization, that underlie the Alloy system. The same can be said of Appendix E, which is a clear, fair, and balanced comparison with B, the object constraint language, the Vienna development method, and Z. The examples and exercises, if given time, thought, and effort, can make better designers of all of us, as Alloy is a powerful force-multiplier in the war on bugs. Jackson's Software Abstractions has my highest recommendation. It is being put to immediate use in my group's venue of software-based safety-critical systems. Online Computing Reviews Service

Reviewer: Panagiotis Louridas

It is difficult to ignore a book that starts off by noting that The New Yorker is much more fun than The Economist , especially when this particular book is quite fun by itself. This work is, essentially, a book on formal methods in software engineering that happens to use a particular approach, Alloy, to present its views. The main idea is that formal methods can be engaging, if properly integrated into the development process. This can happen if they are lightweight enough that writing formal specifications does not take hours of abstract reasoning, and if they are endowed with adequate tool support so that writing abstract models and testing them can happen interactively during development. To illustrate this, the book starts with a whirlwind tour that presents the essentials of Alloy, both the modeling formalism and the environment that implements it. The tour chooses as an example an email address book, and that example is used repeatedly throughout the book. The tour is not always easy to follow, but the purpose is only to scratch the surface, leaving the details for later. Indeed, the details are given in their full glory in what follows. The next chapter presents the mathematical logic foundation of Alloy. This is a variation of relational logic. The presentation is leisurely, and adopts a style of presenting the basic facts first and then firing off a discussion section, where the author gives the rationale and more involved material. A minor carp may be that, in this way, the coverage becomes a bit lengthy; others may appreciate the conversational style, however. In the chapter that follows, the language constructs of Alloy build easily on the logic foundations. Alloy models consist of signatures, which may have fields and correspond to types, and also contain facts, predicates, functions, and assertions. In order to analyze a model, we write commands, and then instruct the Alloy tool to run them. We may instruct the tool to search for an instance of a predicate, or for a counterexample of an assertion. Analysis is the subject of the next chapter, which examines it in depth. A well-known dictum in program checking from Dijkstra—"program testing can be used to show the presence of bugs, but never to show their absence"—is quoted in the book. Even showing the presence of bugs, though, is no easy matter. Starting from an abstract software model, be it in the Alloy specification or in some other approach, and trying to find buggy instances of it, is an intractable problem, as the number of distinct states that must be considered grows exponentially. Here is the central premise of Alloy: "most bugs have small counterexamples." Hence, it is enough to run a model checker over a limited scope, namely, a restriction on the size of instances considered, in order to discover a significant number of bugs. Running abstract software models on a limited scope makes the whole process exploratory, and, in a sense, agile. Developers are expected to check their models on a scope, fix bugs, possibly increase the scope, extend the model by adding more elements to it, and so on. A chapter dedicated to examples gives insight on how one might proceed in real projects. The book ends with a series of appendices, containing, among other things, the Alloy language reference and a series of exercises. The bane of formal methods has been the reluctance of developers to dedicate serious brain power to nonprogramming tasks, especially when these involve dealing with intricate formalisms. The formalism described in this book is very close to a programming language, and it very much looks like one, so developers have a much narrower gap to cross. The Alloy tool makes a serious effort to move abstract model building much closer to programming. The book is well written, and may be the ideal introduction to the area of formal methods, combining theory and practice in a nice way. Will Alloy change the way programs are written__?__ There will always be code that will not be put in any kind of formal reasoning framework; it is likely that nobody knows whether formal methods will be applied in more areas than the relatively niche applications where they are currently used. Familiarity with formal methods, though, and the discipline they instill, would benefit all programmers. This book is a step in the right direction.

Reviewer: Fernando Berzal

Essentially, this is a handbook for the Alloy specification language. Alloy is a structural modeling language based on relational logic, which combines first-order logic quantifiers and relational calculus operations. Its associated tool, dubbed Alloy Analyzer, is technically a model finder. Given a specification written using the Alloy language, the Alloy Analyzer attempts to check that the described system has a given property by looking for counterexamples, or, in a different setting, it tries to find some possible states that make the specification true. Alloy has been developed during the last decade or so within the Software Design Group at the Massachusetts Institute of Technology, with the praiseworthy goal of making formal methods more approachable to a wider audience. It tries to obtain the benefits of traditional formal methods at a lower cost, and provides an interesting tool for designers to play with while they devise the solutions to their design problems. The rationale behind its development goes more or less like this: the core of software development is the design of abstractions, but programming languages, mired in details, are a poor medium for exploring abstractions. Therefore, a better notation should be chosen by following Whitehead's advice: "By relieving the brain from all unnecessary work, a good notation sets it free to concentrate on more advanced problems." Alloy is Daniel Jackson's proposal for such a notation. After a brief guided tour with an email client address book as a companion, Jackson delves right into the details of the Alloy language. First, he describes the basic blocks of the language. Even though it is remarkably flexible by admitting three styles of writing expressions (namely, predicate calculus, navigation expressions, and relational calculus), Alloy is still a relatively simple language, reminding us that simplicity is key to good software design. It should be noted, however, that this does not imply that Alloy is easy to use, since complexity is at the heart of software and its inherent complexity does not disappear just by changing notations. Alloy, whose notation was chosen for ease of expression, is heavily influenced by the Z notation from Oxford and the symbolic model verifier from Carnegie Mellon. Like Z, it does not distinguish functions from relations. Unlike Z, Alloy does not distinguish scalars, sets, and tuples from each other. This is probably the most interesting feature of Alloy syntax. Apart from its logic foundations, Alloy, as a language, also provides a type system and a module system. They provide ways to organize a model and build larger models from smaller ones. In the book, you will find a dedicated chapter that informally describes its syntax by example, and separate appendices that provide a formal language reference, a description of the language kernel semantics, and a quick guide to the diagrammatic notation used to illustrate Alloy textual models. The book also includes four complete examples that show how to use Alloy in different situations, from a textbook problem justifying the correctness of a memory implementation to a more realistic example analyzing the interactions of user interface features in a typical photo organizer. More than 30 graded exercises are also stated in an appendix for interested readers to get acquainted with the quirks of Alloy and achieve proficiency in its use. A key chapter in the book is devoted to the analysis techniques underlying Alloy, their strengths, and their limitations. Alloy is based on the "small scope hypothesis," which states that most design flaws in models can be illustrated by small instances. These instances represent the test cases that make bug reports reproducible. If we were able to perform a complete analysis of all small problem instances, way beyond what the best test suites can do, then most design flaws would be revealed. This is exactly what the Alloy Analyzer does. By setting a predefined scope, the analyzer performs an exhaustive search that finds all instances satisfying a predicate (the possible states obtained by simulation) or those violating an assertion (the counterexamples in checking). Since users limit the search space when using the Alloy Analyzer interactively, false positives might still be possible but true negatives will never be overlooked. Provided that the scope is sufficiently high, the small scope hypothesis will give us some confidence that our designs are correct, according to our Alloy specification. Researchers and graduate students will find the book valuable, especially the question-and-answer sections at the end of each topic discussion. For them, the final appendix is particularly relevant, since it describes five solutions to the same problem using different techniques (Alloy and four alternative approaches: B, OCL, VDM, and Z). This direct comparison of approaches lets the reader acquaint himself with the peculiarities each notation introduces as it provides a wider perspective on specification languages. However, a more tutorial-like gradual exposition of ideas would be desirable to target software practitioners as a potential audience for this book. I would even dare to suggest that a different notation, integrated within the metadata annotation capabilities of modern programming languages, would probably let lightweight formal methods achieve more momentum and have a more profound impact in practice. Online Computing Reviews Service