A Review of ``Building High Integrity Applications with SPARK'' by McCormick and Chapin

Under review is (ISBN 978-1-107-65684-0).  Information concerning it may be found here:
http://www.cambridge.org/9781107656840

I read this work after ``Programming in Ada 2012'', and found it segued nicely.  I've not yet worked
in a proper Ada environment, impacting my ability to use this, but found it educational, regardless.
The book holds several amusing anecdotes concerning program failures which resulted in human deaths.

The first chapter introduces the concepts of software quality, formalizations thereof, and the basic
SPARK language.  Chapters two and three are of course worth reading, but contain naught that any Ada
programmer shouldn't already know.  Chapter four introduces data and flow dependency contracts which
are quite an interesting topic, showing their applicability to hardening a program's specifications.

Chapter five is basic mathematical background.  Chapter six is nearly one hundred pages long and, as
would be expected from this, introduces much of the most interesting material of the book, detailing
the proof system, loop invariants, Contract_Cases, assumptions, interaction with generics, and quite
a many other topics which I was entirely ignorant of beforehand.  Chapter seven details interfacing,
including some amusing detractions of C, and is the most useful chapter of the book after the sixth.

Chapter eight provides a reasonably-detailed overview of system design and evolution in SPARK, using
various starting conditions, and including some of the detail of a full program.  Lastly, the nineth
chapter covers ostensibly advance techniques, most importantly regarding debugging the proof system.

The book contains many working code fragments, and is typeset quite well.  While I dislike so-called
``variable packages'' on aesthetic grounds, I'm not in a position to argue against them; it would've
improved the book greatly were it to contain a working program that wasn't utterly trivial.  Chapter
eight would've been the proper place for such, but primarily defers to an online program repository.

I recommend this to those who read my previous Ada recommendation and are wanting to know more about
the development of provably-correct software in general and mainly to prospective SPARK programmers.
.