Feeds

High integrity software

Writing correct programs with little testing

Top 5 reasons to deploy VMware with Tegile

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.

Providing a secure and efficient Helpdesk

More from The Register

next story
Preview redux: Microsoft ships new Windows 10 build with 7,000 changes
Latest bleeding-edge bits borrow Action Center from Windows Phone
Google opens Inbox – email for people too thick to handle email
Print this article out and give it to someone tech-y if you get stuck
Microsoft promises Windows 10 will mean two-factor auth for all
Sneak peek at security features Redmond's baking into new OS
UNIX greybeards threaten Debian fork over systemd plan
'Veteran Unix Admins' fear desktop emphasis is betraying open source
Google+ goes TITSUP. But WHO knew? How long? Anyone ... Hello ...
Wobbly Gmail, Contacts, Calendar on the other hand ...
DEATH by PowerPoint: Microsoft warns of 0-day attack hidden in slides
Might put out patch in update, might chuck it out sooner
Redmond top man Satya Nadella: 'Microsoft LOVES Linux'
Open-source 'love' fairly runneth over at cloud event
prev story

Whitepapers

Cloud and hybrid-cloud data protection for VMware
Learn how quick and easy it is to configure backups and perform restores for VMware environments.
A strategic approach to identity relationship management
ForgeRock commissioned Forrester to evaluate companies’ IAM practices and requirements when it comes to customer-facing scenarios versus employee-facing ones.
High Performance for All
While HPC is not new, it has traditionally been seen as a specialist area – is it now geared up to meet more mainstream requirements?
Three 1TB solid state scorchers up for grabs
Big SSDs can be expensive but think big and think free because you could be the lucky winner of one of three 1TB Samsung SSD 840 EVO drives that we’re giving away worth over £300 apiece.
Security for virtualized datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.