SPARK (programming Language) - Annotation Examples

Annotation Examples

Consider the Ada subprogram specification below:

procedure Increment (X : in out Counter_Type);

What does this subprogram actually do? In pure Ada, it could do virtually anything — it might increment the X by one or one thousand; or it might set some global counter to X and return the original value of the counter in X; or it might do absolutely nothing with X at all.

With SPARK, annotations are added to the code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say:

procedure Increment (X : in out Counter_Type); --# derives X from X;

or

procedure Increment (X : in out Counter_Type); --# global Count; --# derives --# Count from Count, X & --# X from ;

The first of these specifications tells us that the Increment procedure does not update or read from any global variables and that the only data item used in calculating the new value of X is X itself. The second set of annotations tells us that Increment will use some global variable called "Count" in the same package as Increment and that the exported value of Count is dependent on the imported values of Count and X, but that exported value of X does not depend on any variables at all — it will be derived simply from constant data.

If the Examiner is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against that which has been specified by the annotations and any discrepancies reported to the user.

We can further extend these specifications by asserting various properties that either need to hold when a subprogram is called (preconditions) or that will hold once execution of the subprogram has completed (postconditions). For example, we could say the following:

procedure Increment (X : in out Counter_Type); --# derives X from X; --# pre X < Counter_Type'Last; --# post X = X~ + 1;

This specification now says that not only is X only derived from itself, but that before Increment is called X must be strictly less than the last possible value of its type and that afterwards X will be equal to the initial value of X plus one — no more and no less.