# 5.4. Type Contracts¶

SPARK contains various features to constrain the values of a given type:

- A
*scalar range*may be specified on a scalar type or subtype to bound its values. - A
*record discriminant*may be specified on a record type to distinguish between variants of the same record. - A
*predicate*introduced by aspect`Static_Predicate`

,`Dynamic_Predicate`

or`Predicate`

may be specified on a type or subtype to express a property verified by objects of the type. - A
*type invariant*introduced by aspect`Type_Invariant`

or`Invariant`

may be specified on the completion of a private type to express a property that is only guaranteed outside of the type scope. - A
*default initial condition*introduced by aspect`Default_Initial_Condition`

on a private type specifies the initialization status and possibly properties of the default initialization for a type.

Note that SPARK does not yet support aspect `Type_Invariant`

from Ada 2012.

## 5.4.1. Scalar Ranges¶

[Ada 83]

Scalar types (signed integer types, modulo types, fixed-point types,
floating-point types) can be given a low bound and a high bound to specify that
values of the type must remain within these bounds. For example, the global
counter `Total`

can never be negative, which can be expressed in its type:

```
Total : Integer range 0 .. Integer'Last;
```

Any attempt to assign a negative value to variable `Total`

results in raising
an exception at run time. During analysis, GNATprove checks that all values
assigned to `Total`

are positive or null. The anonymous subtype above can
also be given an explicit name:

```
subtype Nat is Integer range 0 .. Integer'Last;
Total : Nat;
```

or we can use the equivalent standard subtype `Natural`

:

```
Total : Natural;
```

or `Nat`

can be defined as a derived type instead of a subtype:

```
type Nat is new Integer range 0 .. Integer'Last;
Total : Nat;
```

or as a new signed integer type:

```
type Nat is range 0 .. Integer'Last;
Total : Nat;
```

All the variants above result in the same range checks both at run-time and in GNATprove. GNATprove also uses the range information for proving properties about the program (for example, the absence of overflows in computations).

## 5.4.2. Record Discriminants¶

[Ada 83]

Record types can use discriminants to:

- define multiple variants and associate each component to a specific variant
- bound the size of array components

For example, the log introduced in State Abstraction could be
implemented as a discriminated record with a discriminant `Kind`

selecting
between two variants of the record for logging either only the minimum and
maximum entries or the last entries, and a discriminant `Capacity`

specifying
the maximum number of entries logged:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 | ```
package Logging_Discr with
SPARK_Mode
is
type Log_Kind is (Min_Max_Values, Last_Values);
type Integer_Array is array (Positive range <>) of Integer;
type Log_Type (Kind : Log_Kind; Capacity : Natural) is record
case Kind is
when Min_Max_Values =>
Min_Entry : Integer;
Max_Entry : Integer;
when Last_Values =>
Log_Data : Integer_Array (1 .. Capacity);
Log_Size : Natural;
end case;
end record;
subtype Min_Max_Log is Log_Type (Min_Max_Values, 0);
subtype Ten_Values_Log is Log_Type (Last_Values, 10);
function Log_Size (Log : Log_Type) return Natural;
function Last_Entry (Log : Log_Type) return Integer with
Pre => Log.Kind = Last_Values and then Log.Log_Size in 1 .. Log.Capacity;
end Logging_Discr;
``` |

Subtypes of `Log_Type`

can specify fixed values for `Kind`

and
`Capacity`

, like in `Min_Max_Log`

and `Ten_Values_Log`

. The discriminants
`Kind`

and `Capacity`

are accessed like regular components, for example:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | ```
package body Logging_Discr with
SPARK_Mode
is
function Log_Size (Log : Log_Type) return Natural is
begin
case Log.Kind is
when Min_Max_Values =>
return 2;
when Last_Values =>
return Log.Log_Size;
end case;
end Log_Size;
function Last_Entry (Log : Log_Type) return Integer is
begin
return Log.Log_Data (Log.Log_Size);
end Last_Entry;
end Logging_Discr;
``` |

Any attempt to access a component not present in a variable (because it is of a different variant), or to access an array component outside its bounds, results in raising an exception at run time. During analysis, GNATprove checks that components accessed are present, and that array components are accessed within bounds:

```
logging_discr.adb:4:13: info: range check proved
logging_discr.adb:10:23: info: discriminant check proved
logging_discr.adb:14:13: info: range check proved
logging_discr.adb:16:17: info: discriminant check proved
logging_discr.adb:16:31: info: discriminant check proved
logging_discr.adb:16:31: info: index check proved
logging_discr.ads:13:13: info: range check proved
logging_discr.ads:18:37: info: range check proved
logging_discr.ads:18:53: info: range check proved
logging_discr.ads:19:40: info: range check proved
logging_discr.ads:19:53: info: range check proved
logging_discr.ads:24:48: info: discriminant check proved
```

## 5.4.3. Predicates¶

[Ada 2012]

Predicates can be used on any type to express a property verified by objects of
the type at all times. Aspects `Static_Predicate`

and `Dynamic_Predicate`

are defined in Ada 2012 to associate a predicate to a type. Aspect
`Dynamic_Predicate`

allows to express more general predicates than aspect
`Static_Predicate`

, at the cost of restricting the use of variables of the
type. The following table summarizes the main similarities and differences
between both aspects:

Feature | `Static_Predicate` |
`Dynamic_Predicate` |
---|---|---|

Applicable to scalar type | Yes | Yes |

Applicable to array/record type | No | Yes |

Allows simple comparisons with static values | Yes | Yes |

Allows conjunctions/disjunctions | Yes | Yes |

Allows function calls | No | Yes |

Allows general Boolean properties | No | Yes |

Can be used in membership test | Yes | Yes |

Can be used as range in for-loop | Yes | No |

Can be used as choice in case-statement | Yes | No |

Can be used as prefix with attributes First, Last or Range | No | No |

Can be used as index type in array | No | No |

Aspect `Predicate`

is specific to GNAT and can be used instead of
`Static_Predicate`

or `Dynamic_Predicate`

. GNAT treats it as a
`Static_Predicate`

whenever possible and as a `Dynamic_Predicate`

in the
remaining cases, thus not restricting uses of variables of the type more than
necessary.

Predicates are inherited by subtypes and derived types. If a subtype or a derived type inherits a predicate and defines its own predicate, both predicates are checked on values of the new type. Predicates are restricted in SPARK so that they cannot depend on variable input. In particular, a predicate cannot mention a global variable in SPARK, although it can mention a global constant.

GNATprove checks that all values assigned to a type with a predicate are
allowed by its predicate (for all three forms of predicate: `Predicate`

,
`Static_Predicate`

and `Dynamic_Predicate`

). GNATprove generates a
predicate check even in cases where there is no corresponding run-time check,
for example when assigning to a component of a record with a
predicate. GNATprove also uses the predicate information for proving
properties about the program.

### 5.4.3.1. Static Predicates¶

A static predicate allows specifying which values are allowed or forbidden in a
scalar type, when this specification cannot be expressed with Scalar Ranges (because it has *holes*). For example, we can express that the global
counter `Total`

cannot be equal to `10`

or `100`

with the following
static predicate:

```
subtype Count is Integer with
Static_Predicate => Count /= 10 and Count /= 100;
Total : Count;
```

or equivalently:

```
subtype Count is Integer with
Static_Predicate => Count in Integer'First .. 9 | 11 .. 99 | 101 .. Integer'Last;
Total : Count;
```

Uses of the name of the subtype `Count`

in the predicate refer to variables
of this type. Scalar ranges and static predicates can also be combined, and
static predicates can be specified on subtypes, derived types and new signed
integer types. For example, we may define `Count`

as follows:

```
type Count is new Natural with
Static_Predicate => Count /= 10 and Count /= 100;
```

Any attempt to assign a forbidden value to variable `Total`

results in
raising an exception at run time. During analysis, GNATprove checks that all
values assigned to `Total`

are allowed.

Similarly, we can express that values of type `Normal_Float`

are the *normal*
32-bits floating-point values (thus excluding *subnormal* values), assuming
here that `Float`

is the 32-bits floating-point type on the target:

```
subtype Normal_Float is Float with
Static_Predicate => Normal_Float <= -2.0**(-126) or Normal_Float = 0.0 or Normal_Float >= 2.0**(-126);
```

Any attempt to assign a subnormal value to a variable of type `Normal_Value`

results in raising an exception at run time. During analysis, GNATprove
checks that only normal values are assigned to such variables.

### 5.4.3.2. Dynamic Predicates¶

A dynamic predicate allows specifying properties of scalar types that cannot be
expressed as static predicates. For example, we can express that values of type
`Odd`

and `Even`

are distributed according to their name as follows:

```
subtype Odd is Natural with
Dynamic_Predicate => Odd mod 2 = 1;
subtype Even is Natural with
Dynamic_Predicate => Even mod 2 = 0;
```

or that values of type `Prime`

are prime numbers as follows:

```
type Prime is new Positive with
Dynamic_Predicate => (for all Divisor in 2 .. Prime / 2 => Prime mod Divisor /= 0);
```

A dynamic predicate also allows specifying relations between components of a record. For example, we can express that the values paired together in a record are always distinct as follows:

```
type Distinct_Pair is record
Val1, Val2 : Integer;
end record
with Dynamic_Predicate => Distinct_Pair.Val1 /= Distinct_Pair.Val2;
```

or that a record stores pairs of values with their greatest common divisor as follows:

```
type Bundle_Values is record
X, Y : Integer;
GCD : Natural;
end record
with Dynamic_Predicate => Bundle_Values.GCD = Get_GCD (Bundle_Values.X, Bundle_Values.Y);
```

or that the number of elements `Count`

in a resizable table is always less
than or equal to its maximal number of elements `Max`

as follows:

```
type Resizable_Table (Max : Natural) is record
Count : Natural;
Data : Data_Array(1 .. Max);
end record
with Dynamic_Predicate => Resizable_Table.Count <= Resizable_Table.Max;
```

A dynamic predicate also allows specifying global properties over the content of an array. For example, we can express that elements of an array are stored in increasing order as follows:

```
type Ordered_Array is array (Index) of Integer
with Dynamic_Predicate =>
(for all I in Index => (if I < Index'Last then Ordered_Array(I) < Ordered_Array(I+1)));
```

or that a special end marker is always present in the array as follows:

```
type Ended_Array is array (Index) of Integer
with Dynamic_Predicate =>
(for some I in Index => Ended_Array(I) = End_Marker);
```

Dynamic predicates are checked only at specific places at run time, as mandated by the Ada Reference Manual:

- when converting a value to the type with the predicate
- when returning from a call, for each in-out and out parameter passed by reference
- when declaring an object, except when there is no initialization expression and no subcomponent has a default expression

Thus, not all violations of the dynamic predicate are caught at run time. On the contrary, during analysis, GNATprove checks that initialized variables whose type has a predicate always contain a value allowed by the predicate.

## 5.4.4. Type Invariants¶

[Ada 2012]

In SPARK, type invariants can only be specified on completions of private
types (and not directly on private types declarations). They express a property
that is only quaranteed outside of the immediate scope of the type bearing the
invariant. Aspect `Type_Invariant`

is defined in Ada 2012 to associate an
invariant to a type. Aspect `Invariant`

is specific to GNAT and can be
used instead of `Type_Invariant`

.

GNATprove checks that, outside of the immediate scope of a type with an invariant, all values of this type are allowed by its invariant. In order to provide such a strong guarantee, GNATprove generates an invariant check even in cases where there is no corresponding run-time check, for example on global variables that are modified by a subprogram. GNATprove also uses the invariant information for proving properties about the program.

As an example, let us consider a stack, which can be queried for the maximum of the elements stored in it:

```
package P is
type Stack is private;
function Max (S : Stack) return Element;
private
```

In the implementation, an additional component is allocated for the maximum,
which is kept up to date by the implementation of the stack. This information is
a type invariant, which can be specified using a `Type_Invariant`

aspect:

```
private
type Stack is record
Content : Element_Array := (others => 0);
Size : My_Length := 0;
Max : Element := 0;
end record with
Type_Invariant => Is_Valid (Stack);
function Is_Valid (S : Stack) return Boolean is
((for all I in 1 .. S.Size => S.Content (I) <= S.Max)
and (if S.Max > 0 then
(for some I in 1 .. S.Size => S.Content (I) = S.Max)));
function Max (S : Stack) return Element is (S.Max);
end P;
```

Like for type predicates, the name of the type can be used inside the invariant
expression to refer to the current instance of the type. Here the type predicate
of `Stack`

expresses that the `Max`

field of a valid stack is the maximum of
the elements stored in the stack.

To make sure that the invariant holds for every value of type `Stack`

outside
of the package `P`

, GNATprove introduces invariant checks in several
places. First, at the type declaration, it will make sure that the invariant
holds every time an object of type `Stack`

is default initialized. Here, as
the stack is empty by default and the default value of `Max`

is 0, the check
will succeed. It is also possible to forbid default initialization of objects of
type `Stack`

altogether by using a Default Initial Condition of
`False`

:

```
type Stack is private with Default_Initial_Condition => False;
type Stack is record
Content : Element_Array;
Size : My_Length;
Max : Element;
end record with Type_Invariant => Is_Valid (Stack);
```

A check is also introduced to make sure the invariant holds for every global
object declared in the scope of `Stack`

after it has been initialized:

```
package body P is
The_Stack : Stack := (Content => (others => 1),
Size => 5,
Max => 0);
begin
The_Stack.Max := 1;
end P;
```

Here the global variable `The_Stack`

is allowed to break its invariant during
the elaboration of `P`

. The invariant check will only be done at the end of
the elaboration of `P`

, and will succeed.

In the same way, variables and parameters of a subprogram are allowed to break
their invariants in the subprogram body. Verification
conditions are generated to ensure that no invariant breaking value can leak
outside of `P`

. More precisely, invariant checks on subprogram parameters are
performed:

- when calling a subprogram visible outside of
`P`

from inside of`P`

. Such a subprogram can be either declared in the visible part of`P`

or in another unit, - when returning from a subprogram declared in the visible part of
`P`

.

For example, let us consider the implementation of a procedure `Push`

that
pushes an element of top of a stack. It is declared in the visible part of the
specification of `P`

:

```
function Size (S : Stack) return My_Length;
procedure Push (S : in out Stack; E : Element) with
Pre => Size (S) < My_Length'Last;
procedure Push_Zero (S : in out Stack) with
Pre => Size (S) < My_Length'Last;
```

It is then implemented using an internal procedure `Push_Internal`

declared
in the body of `P`

:

```
procedure Push_Internal (S : in out Stack; E : Element) with
Pre => S.Size < My_Length'Last,
Post => S.Size = S.Size'Old + 1 and S.Content (S.Size) = E
and S.Content (1 .. S.Size)'Old = S.Content (1 .. S.Size - 1)
and S.Max = S.Max'Old
is
begin
S.Size := S.Size + 1;
S.Content (S.Size) := E;
end Push_Internal;
procedure Push (S : in out Stack; E : Element) is
begin
Push_Internal (S, E);
if S.Max < E then
S.Max := E;
end if;
end Push;
procedure Push_Zero (S : in out Stack) is
begin
Push (S, 0);
end Push_Zero;
```

On exit of `Push_Internal`

, the invariant of `Stack`

is broken. It is OK
since `Push_Internal`

is not visible from outside of `P`

. Invariant checks
are performed when exiting `Push`

and when calling it from inside
`Push_Zero`

. They both succeed.
Note that, because of invariant checks on parameters, it is not allowed in
SPARK to call a function that is visible from outside `P`

in the invariant
of `Stack`

otherwise this would lead to a recursive proof. In particular, it
is not allowed to make `Is_Valid`

visible in
the public declarations of `P`

. In the same way, the function `Size`

cannot
be used in the invariant of `Stack`

. We also avoid using `Size`

in the
contract of `Push_Internal`

as it would have enforced additional invariant
checks on its parameter.

Checks are also performed for global variables accessed by subprograms inside
`P`

. Even if it is allowed to break the invariant of a global variable when
inside the body of a subprogram declared in `P`

, invariant checks are
performed when calling and returning from every subprogram inside `P`

. For
example, if `Push`

and `Push_Internal`

are accessing directly the global
stack `The_Stack`

instead of taking it as a parameter, there will be a failed
invariant check on exit of `Push_Internal`

:

```
procedure Push_Internal (E : Element) with
Pre => The_Stack.Size < My_Length'Last
is
begin
The_Stack.Size := The_Stack.Size + 1;
The_Stack.Content (The_Stack.Size) := E;
end Push_Internal;
procedure Push (E : Element) is
begin
Push_Internal (E);
if The_Stack.Max < E then
The_Stack.Max := E;
end if;
end Push;
```

In this way, users will never have to use contracts to ensure that the invariant
holds on global variable `The_Stack`

through local subprogram calls.

## 5.4.5. Default Initial Condition¶

[SPARK]

Private types in a package define an encapsulation mechanism that prevents
client units from accessing the implementation of the type. That boundary may
also be used to specify properties that hold for default initialized values of
that type in client units. For example, the log introduced in State Abstraction could be implemented as a private type with a default initial
condition specifying that the size of the log is initially zero, where uses of
the name of the private type `Log_Type`

in the argument refer to variables of
this type:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | ```
package Logging_Priv with
SPARK_Mode
is
Max_Count : constant := 100;
type Log_Type is private with
Default_Initial_Condition => Log_Size (Log_Type) = 0;
function Log_Size (Log : Log_Type) return Natural;
procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
Pre => Log_Size (Log) < Max_Count;
private
type Integer_Array is array (1 .. Max_Count) of Integer;
type Log_Type is record
Log_Data : Integer_Array;
Log_Size : Natural := 0;
end record;
function Log_Size (Log : Log_Type) return Natural is (Log.Log_Size);
end Logging_Priv;
``` |

This may be useful to analyze with GNATprove client code that defines a
variable of type `Log_Type`

with default initialization, and then proceeds to
append values to this log, as procedure `Append_To_Log`

‘s precondition
requires that the log size is not maximal:

```
The_Log : Log_Type;
...
Append_To_Log (The_Log, X);
```

GNATprove‘s flow analysis also uses the presence of a default initial
condition as an indication that default initialized variables of that type are
considered as fully initialized. So the code snippet above would pass flow
analysis without messages being issued on the read of `The_Log`

. If the full
definition of the private type is in SPARK, GNATprove also checks that the
type is indeed fully default initialized, and if not issues a message like
here:

```
logging_priv.ads:18:04: medium: type "Log_Type" is not fully initialized
```

If partial default initialization of the type is intended, in general for
efficiency like here, then the corresponding message can be justified with
pragma `Annotate`

, see section Justifying Check Messages.

Aspect `Default_Initial_Condition`

can also be specified without argument to
only indicate that default initialized variables of that type are considered as
fully initialized. This is equivalent to `Default_Initial_Condition => True`

:

```
type Log_Type is private with
Default_Initial_Condition;
```

The argument can also be `null`

to specify that default initialized variables
of that type are *not* considered as fully initialized:

```
type Log_Type is private with
Default_Initial_Condition => null;
```

This is different from an argument of `False`

which can be used to indicate
that variables of that type should always be explicitly initialized (otherwise
GNATprove will not be able to prove the condition `False`

on the default
initialization and will issue a message during proof).