Software

This article is more than 1 year old

High integrity software

Writing correct programs with little testing

Wed 20 Sep 2006 // 11:09 UTC

Book review This book is the 2006 revision of the key guide to SPARK, a programming language founded on formal proof and static code analysis.

This language happens to be implemented as an Ada dialect that makes use of formal comments to specify what the associated code is supposed to do, but it is not really Ada.

Put simply, it is a development system in which tools are provided to check a formally validated design contract represented in the comments against the behaviour of the actual code – written using restricted coding constructs which facilitate this sort of formal analysis. SPARK programmers expect to get code right first time and generally see no need to fire up a debugger.

The goal of SPARK is to produce correct programs that satisfy some contract between the user and the automated system as to its behaviour – somewhat similar to Eiffel's "design by contract" concept.

SPARK promises to do this not only more effectively than other approaches to producing defect-free software (where defects are considered to be departures from a formal specification), but also more cheaply - if you consider whole-lifecycle cost.

Of course, if correctness doesn't matter because the cost of production failures or code rewrites "doesn't count", and you don't test your code, you can always produce code more cheaply still - but if correctness doesn't matter, one wonders why you're bothering to code at all.

But, it's all about "fitness for purpose", which permits interpretation, and 95 per cent correct may be good enough (as long as we distinguish mindless optimism from reasoned risk management). So, not everyone will be immediately enthusiastic about SPARK and its approach and it is good that John Barnes (the author of this book) professes himself sceptical of "formal theorists who like to define everything in some turgid specification language before contemplating the process known as programming".

Barnes even recognises that formal specifications could make programs less reliable, overall, by placing obstacles between the end-user, stakeholders in the system, and the developers. However, he is well-qualified to write about SPARK, having (with his daughter Janet) undertaken an early review of SPARK and its development, informally known as "Janet and John go a-Sparking". And, nevertheless, he does produce a convincing rationale for SPARK, which perhaps extends beyond the realms of just "safety critical computing".

SPARK is more than just a language (it is a fundamental part of a development process) and this book is more than just a language cookbook.

Part one of the book is an introduction to the "correctness by construction" process used with SPARK and the SPARK tools: Examiner, Simplifier and Proof Checker. The Examiner seems to be central to the use of SPARK – it checks conformance of the code to the rules of the kernel language; and the consistency between the code and the embedded comment annotations (using control, data and information flow analysis). The Examiner is written in SPARK and has been applied to itself, which (Barnes claims) means you can have confidence in its being correct.

Part two is a detailed description of the SPARK language, of the sort needed by an intending SPARK programmer.

Part three describes the SPARK tools and their use in more detail than that provided in the introduction. As well as verification, it covers design issues and provides a useful set of practical case studies.

A set of Appendices includes the core language syntax, a list of reserved words etc, documentation of the supplied CDROM, and a description of "work in progress" (the 2006 revision of this book takes account of, for example, the Ada Ravenscar profile for tasking in high integrity systems). Answers to exercises and a three page bibliography are also supplied.

The CD supplied with the book contains more documentation (including examples and exersises) as well as demo versions of the Examiner and Simplifier (but not the Proof Checker).

All-in-all, this book seems to be a pretty complete practical guide not only to an interesting programming language, one well worth looking at as concern with IT governance and software quality increases, but also to the philosophy and process behind its use. As a bonus, it is readable and not a bit offputting, at least for professional developers.