SPARK is a subset and extension of the Ada programming language, designed for developing and verifying highly reliable software. This book is a tutorial on SPARK 2005, the current but soon to be displaced version of the language.
SPARK restricts Ada to a subset of its features, and then extends it using specially formatted Ada comments to embed assertions and additional information about program data flow. SPARK tools use these annotations to analyze programs, to establish aspects of their correctness and to help generate program proofs. Nevertheless, every SPARK program is also a legitimate Ada program, so any Ada compiler can compile a verified SPARK program. This strategy has proven quite successful, and SPARK has been used to develop many high-reliability products for more than 30 years.
SPARK was created in the late 1980s based on Ada 83; as Ada evolved, it was revised into SPARK 95 (based on Ada 95) and then SPARK 2005 (based on Ada 2005). Along the way, SPARK incorporated more features and greater capabilities as well. John Barnes also wrote a book on SPARK 95 in 1997, and a revision incorporating changes to SPARK 95 in 2003. The current book documents SPARK 2005.
This book is a typical member of the programming language text genre. Part 1, comprising three chapters, introduces the language, its use, and its advantages, with several examples. Part 2, consisting of six chapters, presents the SPARK language in detail, contrasting it with full Ada. Part 3, another six chapters, covers SPARK program analysis tools, how they work, and how to use them effectively; the final chapter presents two case studies. There are three appendices specifying the language syntax, listing lexical items unique to SPARK, and discussing upgrades to SPARK currently in progress. Finally, there are answers to the exercises that appear occasionally throughout the book, a bibliography, and an index.
Some programming language texts also make good references, but the rather short index and pedagogical presentation make this book less than ideal as a reference. The value of the text is increased by the discussions in the last part of the book, which cover program design practices, tips for using SPARK effectively, and case studies illustrating SPARK. On the other hand, its dearth of exercises and lack of other pedagogical features (such as review questions, outlines, and so forth) detract from its value as a textbook. Overall, this is a solid tutorial on SPARK and the tools that go with it as of 2012. It is also the only SPARK textbook available.
As I’m writing this review in July 2013, work is already well under way on SPARK 2014, due to be released in only a few months. SPARK 2014 is based on Ada 2012, which includes a new feature called aspects. Aspects provide an elegant and powerful means of stating assertions and program properties in the Ada code itself, and consequently SPARK 2014 abandons the comment-annotation strategy of all previous versions of SPARK in favor of aspects. SPARK 2014 also admits a much larger subset of Ada into SPARK. Consequently, the version of SPARK presented in this (quite new) book is already becoming obsolete (although legacy SPARK 2005 systems will undoubtedly persist for some time). In fact, while I was unable to obtain a free version of SPARK 2005 to use in helping me review this book, I could download an early version of SPARK 2014. The website for the book also seems to have vanished.
The small community of SPARK 2005 developers may welcome this book as a resource to help master the language and its toolset. Teachers interested in a SPARK textbook, and other people interested in high-reliability computing, may want to wait for a text documenting SPARK 2014. Barnes may not be eager to write that one, however, after all the work he put into a book whose shelf life has proven to be so short.
