Tokeneer Discovery - A SPARK Tutorial

What is Special About SPARK Contracts?

The following simple example shows why contracts are so special to the SPARK language. Let’s examine the following Ada subprogram declaration for the procedure Inc.


        procedure Inc (X : in out Integer);
    

The declaration says very little. It only tells us that the procedure has a single in and out parameter X of type Integer - that is, the value may be read and may be updated. There is no way to determine what effect, if any, the subprogram has on parameter X or any other global variables (variables that are in-scope). Nothing can be inferred from the name of the procedure. The procedure could add or subtract one, a hundred or any other integer value to the variable X, do nothing at all, or update any global variable without contradicting the procedure’s declaration.

SPARK contracts provide the mechanism to specify properties about subprograms (procedures and functions).

Let’s first specify that the procedure reads and updates the global variable CallCount to record the number of times this procedure is called, and that no other global variables are read or updated. In SPARK, contracts are expressed with the prefix ––#.


        procedure Inc (X : in out Integer);
        ––# global in out CallCount;
    

The contract above specifies that the formal parameter X and global variable CallCount must be read by at least one path and must be updated by at least one path through the procedure.

SPARK static analysis will report an error if the implementation of the procedure:

SPARK contracts can specify, using postconditions, even more about the effects on the parameter X and global variable CallCount - see code below.


        procedure Inc (X : in out Integer);
        ––# global in out CallCount;
        ––# post X = X~ + 1 and 
        ––#      CallCount = CallCount~+ 1;
    

The postconditions specify that both variables are incremented by one. In SPARK, X~ refers to the initial value of X - similarly for CallCount. This is a far more precise statement about the procedure than what we initially started with. The SPARK Toolset will raise an error if the implementation contradicts the procedure’s contract.

Contracts can also specify preconditions to express properties that must hold when the subprogram is called. The code below specifies the condition that both variables must be less than Integer’Last. The purpose of adding this precondition is to prevent integer overflow errors. The SPARK Toolset, during source code analysis, will attempt to verify that all calls to this procedure satisfy this precondition.


        procedure Inc (X : in out Integer);
        ––# global in out CallCount;
        ––# pre  X < Integer’Last and
        ––#      CallCount < Integer’Last;
        ––# post X = X~ + 1 and 
        ––#      CallCount = CallCount~ + 1;
    

This brief introduction gives an insight into the precision at which we can specify program behaviours through contracts. This ability distinguishes SPARK from other standard programming languages.

The remainder of this tutorial contains a series of lessons using the Tokeneer source code to demonstrate key capabilities of the SPARK Toolset and why SPARK is ideally suited for high-assurance software. The lessons show why the SPARK Toolset can verify that a SPARK program is free from certain classes of common and potentially dangerous errors.