Software Abstractions: Logic, Language, and Analysis [Hardcover]

Daniel Jackson (Author)

Book Description

Publication Date: March 24, 2006 | ISBN-10: 0262101149 | ISBN-13: 978-0262101141

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 approach: 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.

Editorial Reviews

Review

"Abstraction is the essence of simple and effective software design, and logic is the essential tool for exploring and validating abstractions. These basic insights, which have been laboriously rediscovered by many practicing programmers, are now accessible to students and professionals at all levels of experience. Daniel Jackson supports his clear and elegant text with a powerful logical analysis tool that brings his witty examples to life."--Tony Hoare, Senior Researcher, Microsoft

"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." George Hacken Computing Reviews

About the Author

Daniel Jackson is Professor in the Department of Electrical Engineering and Computer Science and leads the Software Design Group at the Computer Science and Artificial Intelligence Lab at MIT.

Product Details

• Hardcover: 366 pages
• Publisher: The MIT Press (March 24, 2006)
• Language: English
• ISBN-10: 0262101149
• ISBN-13: 978-0262101141
• Product Dimensions: 9.3 x 6.1 x 0.9 inches
• Shipping Weight: 12 ounces (View shipping rates and policies)
• Average Customer Review: 2.5 out of 5 stars  See all reviews (2 customer reviews)
• Amazon Best Sellers Rank: #1,028,384 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

14 of 14 people found the following review helpful:

4.0 out of 5 stars Good guide for those looking for formal methods that are actually useful, June 5, 2007

By 

Joseph Carnahan (Boston, MA) - See all my reviews
(REAL NAME)   

This review is from: Software Abstractions: Logic, Language, and Analysis (Hardcover)

This book describes Alloy, a tool for specifying and analyzing data structures and other relationships within your programs. The book walks you through a tutorial, showing you how you can find the bugs in your specifications before you actually write any code, and then goes into the details of the language and its semantics.

I think I was exactly the target audience for this book (and the Alloy language), as I write a lot of Java software and have been looking for a practical specification tool. I've heard of other people who were less happy with this book, as they were trying to learn _about_ Alloy rather than learning Alloy itself. There is some material at the beginning and end that compares and contrasts Alloy with other specification languages, but the real value of this book comes in the middle where it teaches you how to use Alloy effectively.

6 of 10 people found the following review helpful:

1.0 out of 5 stars Horrid Book, Out-Of-Date, Many Corrections Needed, February 22, 2011

By 

Seemann - See all my reviews

Amazon Verified Purchase

This review is from: Software Abstractions: Logic, Language, and Analysis (Hardcover)

Some may say that it is pompous to promote oneself and one's computer language by writing a book about it, rather than simply doing a formal grammar summary, API, tutorials, or other such media... some may say that it is even worse to do as such and get it wrong (e.g., examples that don't work, syntax that was out-of-date with your latest language revisions when you wrote the book, and just plain errors)... some may even say it's even worse to write a book explaining your language and then changing the language afterward so that more than 2/3rds of the book are completely worthless, incorrect, and useless... but I say that the worst part about this book is that I feel it purports to be something that it's not. The title should be 'Alloy: Language Specifications', not 'Software Abstractions: Logic, Language, and Analysis'.

All things aside, the book is not worth $10.00, or even $5.00. I'm not even sure I would take it if you offered it to me for free. Why? Simply because it is not very well written, does little to actually help you write hardcore Alloy models, and is about as out-of-date as the few tutorials on Alloy's website. Mr. Jackson made certain to publish a book on the language and its syntax (not covering everything or anything complex, as well as providing a lot of awful examples that left the reader lacking and simply thinking the language underpowered compared to the numerous other DSMLs available) and then change the syntax so that most of the examples, if not every one of them, will not run in Alloy interpreters without various modifications... oh... and I forgot to mention, that in many cases, the changes are a bit involved and the interpreter does little to help you figure out what it is that you need to do to resolve the issue.

Seriously... save your money (no matter what the price is) and your time... don't buy this book... and don't read this book.