The Philosophy of SPARK

Correctness by Construction

Critical software is different. The need to show, before there is any service experience, that a system will be trustworthy requires a qualitatively different approach. Simply being more careful is not sufficient. In today's competitive environment the challenge is even greater: it is not enough just to produce trusted systems, we need to produce them in a timely and effective manner with risk and cost always under control.

The twin demands of high integrity and rapid development are often seen as being in opposition. In fact, we can align these goals by adopting a development approach leading to correctness by construction.

The key factors of the approach are:

• A "right first time" approach-doing the job once rather than trying to speed up an iterative code-test-debug process;
• the avoidance of surprise;
• an emphasis on fault prevention rather than fault detection; and
• maintaining manageable "semantic gaps" between process stages.

The key to reaching these desirable goals is the ability to reason about the meaning and behaviour of software at an early stage in its development. Program source code is available relatively early in the development process. Source code analysis therefore offers us a way of achieving the correctness by construction goals. Unfortunately, all standard programming languages allow construction of programs of uncertain meaning; these difficulties mean that we have become used to the idea that software behaviour is defined by test results rather than predicted by its source code. Therefore developers can often be misled by the apparent need to get to test as quickly as possible rather than to try the cheaper "right first time" approach.


The SPARK Solution

To reap the considerable benefits of correctness by construction the first requirement is a programming language providing precision of expression: source code must have a unique and precise meaning. SPARK is a secure, formally-defined sub-language of Ada with precisely the required properties. SPARK source code is unambiguous and amenable to rigorous analysis. The language itself eliminates whole classes of common error and facilitates the very early detection of any that remain. A system of annotations embeds specification information in the code reducing the semantic gap between them.

The use of SPARK and its support tool (the Examiner) allows the behaviour of designs and programs to be explored throughout the development process. Most errors can be eliminated before testing even begins; often before the code is even ready to be compiled. Testing changes from an endless bug hunt to a demonstration of correctness. Costly re-work is reduced and the often-experienced bottlenecks of integration testing and independent verification are eliminated. SPARK offers the win-win-win of faster development, reduced risk and higher-quality code.