What do you think?
Rate this book
Software Abstractions: Logic, Language, and Analysis: Logic, Language, and Analysis
In Software Abstractions Daniel Jackson introduces a new approach to software design that draws on traditional formal methods but exploits automated tools to find flaws as early as possible. This approach--which Jackson calls "lightweight formal methods" or "agile modeling"--takes from formal specification the idea of a precise and expressive notation based on a tiny core of simple and robust concepts but replaces conventional analysis based on theorem proving with a fully automated analysis that gives designers immediate feedback. Jackson has developed Alloy, a language that captures the essence of software abstractions simply and succinctly, using a minimal toolkit of mathematical notions. The designer can use automated analysis not only to correct errors but also to make models that are more precise and elegant. This approach, Jackson says, can rescue designers from "the tarpit of implementation technologies" and return them to thinking deeply about underlying concepts.Software Abstractions introduces the key elements of the a logic, which provides the building blocks of the language; a language, which adds a small amount of syntax to the logic for structuring descriptions; and an analysis, a form of constraint solving that offers both simulation (generating sample states and executions) and checking (finding counterexamples to claimed properties). The book uses Alloy as a vehicle because of its simplicity and tool support, but the book's lessons are mostly language-independent, and could also be applied in the context of other modeling languages.
366 pages, Kindle Edition
First published March 24, 2006
25 people are currently reading
244 people want to read
About the author
Daniel Jackson
6 books14 followersDaniel Jackson is professor of computer science and associate director of CSAIL, MIT’s largest lab. His software research won an Impact Award and Outstanding Research Award from the Association for Computing Machinery, and he is an ACM Fellow. He is lead designer of the Alloy software modeling language. He led a National Academies study on software dependability, and has collaborated on software projects with NASA on air-traffic control, with Massachusetts General Hospital on proton therapy, and with Toyota on autonomous cars.
Jackson is also a photographer. His book Portraits of Resilience, which combines stories and images of people who've experienced mental health challenges, was featured on PBS's Newshour and NPR’s Here and Now.
Jackson is also a photographer. His book Portraits of Resilience, which combines stories and images of people who've experienced mental health challenges, was featured on PBS's Newshour and NPR’s Here and Now.
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 4 of 4 reviews
August 6, 2022
This is a very special, unique book that I liked a lot, but I don’t think I can easily recommend to all fellow software engineers and architects.
I first heard about this book when its first edition came out, that is, almost 16 years ago! Finally, six years after its second edition, I decided to dive into it, before tackling “Practical TLA+: Planning Driven Development.”
The author of the book is also the designer of Alloy declarative specification language and Alloy analyzer software that lets you execute/explore/test Alloy models, and luckily for us, not only is he the obvious authority on this topic, but he is also a good writer with a very good pedagogical style.
I’m thankful to the author and other software engineers that built and released Alloy as “a self-contained executable, which includes the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples.” Most of the technology-related books quickly go out of date, but in this case, six years after the book’s publication and new releases of the software tools, it was still straightforward to run the Alloy analyzer and use it to experiment with the models in the book.
Having said that, I should also warn you because even though the author has a very nice, gentle conversational tone, trying to relate the most abstract logical, mathematical and computer science concepts to concrete examples from various software application domains, some parts of the book is not light reading, including some of the exercises. Whether that will be worth your intellectual efforts depends very much upon you and your sub-field of software work.
All in all, I’m glad to finally see how such an interesting language and related tools can augment human intelligence in terms of logical software modeling. In author’s words, “software, unlike hardware, rarely fails because of a single tiny but debilitating flaw. In almost all cases, software fails because of poor abstractions that lead to a proliferation of bugs, one of which happens to cause the failure.” Another critical idea that I took away from the book is the “small scope hypothesis”, the idea that a high proportion of bugs can be found by testing a program for all test inputs within some small scope. Or, in other words, “systems that fail on large instances almost always fail on small ones with similar properties. Whether these small instances are common in the actual executing system doesn’t matter.”
Another nice touch of the book, something that deserves great praise is the comparison of Alloy with other similar languages and tools by encoding the same model (recodable hotel door lock design): solutions crafted by the experts to the same modeling problem are presented for Z, OCL, VDM, and B (see The B-Book: Assigning Programs to Meanings).
Before finishing the review, I'd like to add that if you are really new to this field, it will probably be more productive and effective if you can find at least another interested friend, and also someone more experienced in this kind of formal abstract software modeling, because such a "reading/study group" will probably be very helpful for the more challenging parts of the book.
Now go forth and model! :)
I first heard about this book when its first edition came out, that is, almost 16 years ago! Finally, six years after its second edition, I decided to dive into it, before tackling “Practical TLA+: Planning Driven Development.”
The author of the book is also the designer of Alloy declarative specification language and Alloy analyzer software that lets you execute/explore/test Alloy models, and luckily for us, not only is he the obvious authority on this topic, but he is also a good writer with a very good pedagogical style.
I’m thankful to the author and other software engineers that built and released Alloy as “a self-contained executable, which includes the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples.” Most of the technology-related books quickly go out of date, but in this case, six years after the book’s publication and new releases of the software tools, it was still straightforward to run the Alloy analyzer and use it to experiment with the models in the book.
Having said that, I should also warn you because even though the author has a very nice, gentle conversational tone, trying to relate the most abstract logical, mathematical and computer science concepts to concrete examples from various software application domains, some parts of the book is not light reading, including some of the exercises. Whether that will be worth your intellectual efforts depends very much upon you and your sub-field of software work.
All in all, I’m glad to finally see how such an interesting language and related tools can augment human intelligence in terms of logical software modeling. In author’s words, “software, unlike hardware, rarely fails because of a single tiny but debilitating flaw. In almost all cases, software fails because of poor abstractions that lead to a proliferation of bugs, one of which happens to cause the failure.” Another critical idea that I took away from the book is the “small scope hypothesis”, the idea that a high proportion of bugs can be found by testing a program for all test inputs within some small scope. Or, in other words, “systems that fail on large instances almost always fail on small ones with similar properties. Whether these small instances are common in the actual executing system doesn’t matter.”
Another nice touch of the book, something that deserves great praise is the comparison of Alloy with other similar languages and tools by encoding the same model (recodable hotel door lock design): solutions crafted by the experts to the same modeling problem are presented for Z, OCL, VDM, and B (see The B-Book: Assigning Programs to Meanings).
Before finishing the review, I'd like to add that if you are really new to this field, it will probably be more productive and effective if you can find at least another interested friend, and also someone more experienced in this kind of formal abstract software modeling, because such a "reading/study group" will probably be very helpful for the more challenging parts of the book.
Now go forth and model! :)
May 26, 2015
The book describes the features of Alloy language. The exposition style is unlike other books about programming languages or tools. Further, the simultaneous exposition about both relational and predicate style to specify constraints in Alloy makes understanding harder. While the interspersed discussions are interesting, a comparative presentation of the features of Alloy language with a running example with references to pertinent discussions might have made the book more accessible to beginners.
March 11, 2014
i want to read..
Displaying 1 - 4 of 4 reviews