This is a revised version of a previous book "High Integrity Ada", by John Barnes. In the present book, Barnes describes how to use "Spark" (a programming language based on Ada) to write software for applications where predictable system performance is a key requirement.

The use of Spark - with appropriate tools - allows a high degree of static analysis to be carried out during program development, with the aim of obtaining what Barnes calls "correctness by construction". For example, the programmer can specify pre- and post-conditions for functions, in a (comparatively) simpleway.

There are many interesting ideas here. However, around a third of the book is a cut-down "user guide" for a set of tools produced by Praxis Critical Systems. In addition, the examples presented throughout the text are very small, and even the (so called) case studies are rather too brief to be very convincing. I was also struck by the very limited coverage of issues relating to I/O (crucial in most safety-critical systems), and the fact that interrupt handling (another important issue) is not even listed in the index.

Overall, this book may be of greatest value to users of those who have purchased Spark tools and want an introduction to the language and its use.Internet