Feeds

High integrity software

Writing correct programs with little testing

High performance access to file storage

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.

High Integrity Software

High Integrity SoftwareVerdict: Surprisingly, given its title, this book is readable, even fun in places, without being trivial. It should be essential reading for any programmers who value correctness in their programs - not because they should all use SPARK, but because it will help them understand the consequences of their language choices. Of course, it is also an excellent guide to SPARK for high-integrity programming specialists, dealing with safety-critical and high-security systems and the like.

Author: John Barnes

Publisher: Addison Wesley

ISBN: 0321136160

Media: Book

Buy this book at Cash 'n' Carrion

David Norfolk is the author of IT Governance, published by Thorogood. More details here.

High performance access to file storage

More from The Register

next story
Android engineer: We DIDN'T copy Apple OR follow Samsung's orders
Veep testifies for Samsung during Apple patent trial
Windows 8.1, which you probably haven't upgraded to yet, ALREADY OBSOLETE
Pre-Update versions of new Windows version will no longer support patches
Microsoft lobs pre-release Windows Phone 8.1 at devs who dare
App makers can load it before anyone else, but if they do they're stuck with it
This time it's 'Personal': new Office 365 sub covers just two devices
Redmond also brings Office into Google's back yard
Half of Twitter's 'active users' are SILENT STALKERS
Nearly 50% have NEVER tweeted a word
Windows XP still has 27 per cent market share on its deathbed
Windows 7 making some gains on XP Death Day
Internet-of-stuff startup dumps NoSQL for ... SQL?
NoSQL taste great at first but lacks proper nutrients, says startup cloud whiz
US taxman blows Win XP deadline, must now spend millions on custom support
Gov't IT likened to 'a Model T with a lot of things on top of it'
Batten down the hatches, Ubuntu 14.04 LTS due in TWO DAYS
Admins dab straining server brows in advance of Trusty Tahr's long-term support landing
prev story

Whitepapers

Securing web applications made simple and scalable
In this whitepaper learn how automated security testing can provide a simple and scalable way to protect your web applications.
Five 3D headsets to be won!
We were so impressed by the Durovis Dive headset we’ve asked the company to give some away to Reg readers.
HP ArcSight ESM solution helps Finansbank
Based on their experience using HP ArcSight Enterprise Security Manager for IT security operations, Finansbank moved to HP ArcSight ESM for fraud management.
The benefits of software based PBX
Why you should break free from your proprietary PBX and how to leverage your existing server hardware.
Mobile application security study
Download this report to see the alarming realities regarding the sheer number of applications vulnerable to attack, as well as the most common and easily addressable vulnerability errors.