Feeds

High integrity software

Writing correct programs with little testing

Choosing a cloud hosting partner with confidence

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.

Top 5 reasons to deploy VMware with Tegile

More from The Register

next story
Download alert: Nearly ALL top 100 Android, iOS paid apps hacked
Attack of the Clones? Yeah, but much, much scarier – report
You stupid BRICK! PCs running Avast AV can't handle Windows fixes
Fix issued, fingers pointed, forums in flames
Microsoft: Your Linux Docker containers are now OURS to command
New tool lets admins wrangle Linux apps from Windows
Facebook, working on Facebook at Work, works on Facebook. At Work
You don't want your cat or drunk pics at the office
Soz, web devs: Google snatches its Wallet off the table
Killing off web service in 3 months... but app-happy bonkers are fine
First in line to order a Nexus 6? AT&T has a BRICK for you
Black Screen of Death plagues early Google-mobe batch
prev story

Whitepapers

Why and how to choose the right cloud vendor
The benefits of cloud-based storage in your processes. Eliminate onsite, disk-based backup and archiving in favor of cloud-based data protection.
Forging a new future with identity relationship management
Learn about ForgeRock's next generation IRM platform and how it is designed to empower CEOS's and enterprises to engage with consumers.
10 ways wire data helps conquer IT complexity
IT teams can automatically detect problems across the IT environment, spot data theft, select unique pieces of transaction payloads to send to a data source, and more.
5 critical considerations for enterprise cloud backup
Key considerations when evaluating cloud backup solutions to ensure adequate protection security and availability of enterprise data.
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?