Once upon a time, a group set out to build a language which would allow you to write programs that could be formally verified. Formal analysis and proof can be used to determine that a program will work the way you want it to, and not do something very weird (usually at an inopportune time). First came the attempt to build the Southampton Program Analysis Development Environment (or SPADE) using a subset of the Pascal programming language. When it was determined that Pascal wasn't really suitable, research was directed to Ada, and the SPADE Ada Kernel, or (with a little poetic licence) SPARK, was the result.

SPARK can be considered both a subset and extension to Ada, but is best seen as a separate language in its own right. SPARK forbids language structures such as the infamous GOTO statement of Fortran and BASIC (which cannot be formally verified). Support for some object- oriented features has been included in SPARK, but not for aspects like polymorphism which would make formal proof problematic. A great deal of the security of SPARK lies in the idea of contracts and the use of data specifications (usually referred to as interfaces) that prevent problems such as the unfortunately all-too-ubiquitous buffer overflow.

Part one is an overview of the background and features of SPARK. Chapter one reviews some of the problems of unproven software, and the major components of SPARK. Support for the formal proof functions, such as abstraction (the elimination of details not essential to the fundamental operation of the concept or function) are dicussed in chapter two. The various analysis tools are listed in chapter three.

Part two outlines the SPARK language itself. Chapter four describes the structure of SPARK and the lexical items it contains. Language elements are covered in chapters five, six, and seven, successively dealing with the type model and operators, control and data flow, and packages and visibility (local, global, etc.) which also reviews the object-oriented aspects of SPARK. Interfacing of the various parts of SPARK, and also of SPARK and other languages, is in chapter eight.

Part three looks at the various analytical utilities in SPARK and the proof process. Chapter nine concentrates on the main Examiner tool. A mathematical discussion of data flow analysis, in chapter ten, is not necessary to the operation of SPARK, but provides background and explanation. Verification, and the instruments that support it, are reviewed in chapter eleven. Chapter twelve examines the rather vague practice of design, and proposes the INFORMED (INformation Flow Oriented MEthod of Design) process, although it seems to be limited to some admittedly useful principles. A list of similar precepts makes up the eponymous programming "Techniques" of chapter thirteen.

Chapter fourteen retails a number of case studies of the possible use of SPARK for various applications: the simpler ones also contain source code.

Both the writing in the book, and the explanations of SPARK, are clear. Formal methods of architecture and programming are not well understood, and this text does provide some justification for the exercise, although more evidence and support would be welcome. I recommend this work not only to those interested in more secure applications development, but also to those needing more information about formal methods in composition and system architecture.

copyright Robert M. Slade, 2003 BKHISTSA.RVW 20030913