Feeds

High integrity software

Writing correct programs with little testing

The Power of One eBook: Top reasons to choose HP BladeSystem

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.

HP ProLiant Gen8: Integrated lifecycle automation

More from The Register

next story
Whoah! How many Google Play apps want to read your texts?
Google's app permissions far too lax – security firm survey
Chrome browser has been DRAINING PC batteries for YEARS
Google is only now fixing ancient, energy-sapping bug
Do YOU work at Microsoft? Um. Are you SURE about that?
Nokia and marketing types first to get the bullet, says report
Microsoft takes on Chromebook with low-cost Windows laptops
Redmond's chief salesman: We're taking 'hard' decisions
EU dons gloves, pokes Google's deals with Android mobe makers
El Reg cops a squint at investigatory letters
Big Blue Apple: IBM to sell iPads, iPhones to enterprises
iOS/2 gear loaded with apps for big biz ... uh oh BlackBerry
OpenWRT gets native IPv6 slurping in major refresh
Also faster init and a new packages system
prev story

Whitepapers

Reducing security risks from open source software
Follow a few strategies and your organization can gain the full benefits of open source and the cloud without compromising the security of your applications.
Consolidation: The Foundation for IT Business Transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.
Application security programs and practises
Follow a few strategies and your organization can gain the full benefits of open source and the cloud without compromising the security of your applications.
Boost IT visibility and business value
How building a great service catalog relieves pressure points and demonstrates the value of IT service management.
Consolidation: the foundation for IT and business transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.