Advertisement
Membership
Login
ACCU Buttons
Search in Book Reviews
Search is a simple string search in either book title or book author. The full text search is a search of the text of the review.
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