I’m pleased to see that the “all new” SPARK book was published this week. The book is by long-time SPARK users John McCormick and Peter Chapin. John has taught SPARK for many years as part of his real-time systems lab courses at UNI, while Peter is mainly known for his involvement in the remarkable Vermont CubeSat project, where the team used SPARK for the in-flight software.
The new book covers SPARK 2014, of course, in all its glory and the latest GPL release of the toolset. It’s aimed at an audience coming to SPARK (and Ada) for the first time, but it should also
be useful for those familiar with SPARK 2005.
The opening chapters covers the basics – SPARK’s type system, subprograms, packages and so on, before moving on to the more meaty stuff such as contracts, proof, and design issues.
The latter topic is particularly welcome – we always found that “design for verification” was a key driving force in the success (or otherwise…) of SPARK projects, but this topic was hardly touched on by other languages and design approaches.
I hope the book reaches a new audience of professors, students and engineers, raising awareness of SPARK and what it can do. A big thanks to John and Peter for their hard work in putting it together.
Here it is on amazon.co.uk.