This book is very different to Software Requirements by Karl E. Wiegers I have just reviewed. That was a conventional software requirements book. This one is a little different. This one is closer to formal methods... Well there goes 80% of the audience! I picked up this book hoping for a conventional book on software specifications so I was a bit unhappy. Perhaps it should have something about formal methods in the title? Fortunately for those who by online the contents page does give some indication of the direction of this book.
Upon flicking through the book I was pleasantly surprised to see the examples of code were in C. This led me to hope that I might be able to apply formal methods to my C code specifications. As I work in embedded systems I come across a lot of safety and mission critical systems. Most books on formal methods are in Z, VDM etc or target things like Ada. So a book with formal methods and C would be welcome.
However when I looked at the first code example I found the include file "specdef.i" , apparently" .i" for include, contained a function with executable code in it and other include files! The short program contained a for loop where the statement following the control statement did not have braces around it... the excuse of saving page space is not acceptable in a book that is intending to teach rigour and formal methods.
On further examination I found the standard of the C throughout the book to be well below that which I would expect for any book looking to raise the quality of software engineering. In fact it is down right poor. I suspect that a mathematician rather than an engineer wrote this book. Single letter variables may make it look more like algebra but are not a good idea in software engineering.
Many of the things in the source code of this book are the some of the first things outlawed in coding standards. One of the "more efficient" code fragments uses multiple gotos! I then looked at the introduction to discover why this book had been written. Basically it is the notes for a module on formal methods for a university course. In some universities lecturers may recommend their own books as course books.
You may wonder why I have looked so long at the source code rather than the actual subject of the book... simply because it is no use having a good grasp of theoretical specification if you translate that into such poor quality code you make it difficult to debug and maintain. Not to mention test. You have to be able to test the code against the specification. Also there is some attempt to explain (teach?) the C as the book goes along. Actually it is C/C++, classes with printf statements in them! Strangely the references for C and C++ are the K&R and Stroustrup books, not a mention of the ISO standards in sight. So much for formal specifications!
The other problem is that there are exercises in the book, which one is expected to implement in C/C++ but only "selected hints" at the end of the book and no solutions.
There is a heavy reliance on assert. The problem is that formal methods tend to be used in safety critical areas. These are often embedded systems where there is often no assert function for obvious reasons. The other problem is that code must be shipped as tested and it is not usual to ship with assert code in it.
Having found so much I did not like about this book I must admit I did not work too hard to look at the more formal mathematical parts of the book.
This book may be usable for the students of the class where it is taught but I cannot find any reason to recommend it for anyone else. There are better books on formal methods, C, C++ and specifying software. This is a pity as a good book on more rigorous specification of C programs would useful. Not Recommended.
