This book may not be every programmer's cup of tea, but if you are interested in the Alloy programming language, agile modeling or a new way to look at software abstraction then this is the book for you.
Alloy is related to the Z language. Alloy is a combination of predicate logic and relational algebra that maps well to graphical modeling tools like UML (Universal Modeling Language). A sizable chunk of the book is dedicated to Alloy making it a good reference manual but Jackson does a good job of presenting his design principles while introducing aspects of Alloy.
Alloy will probably not push C out of its top programming language slot but it offers a number of benefits in terms of analysis and design. Alloy Analyzer is a tool that is discussed and that can be downloaded from MIT's website. It is applied to models written in Alloy. Formally meeting design constraints is becoming critical as designs become more complex, employ hundreds of designers and address safety critical and reliable applications.
Alloy is an interesting language, and you will need to read this book to understand it and its application. Alloy can be used to build and verify models even if the application is written in something like C. This is similar to UML, but Alloy is significantly simpler, though no less powerful. It might be more suitable for many developers.
This book does a good job of putting modeling and model analysis tools and methodologies into the hands of the reader.
