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
,Ghost_Predicate
orPredicate
may be specified on a type or subtype to express a property verified by objects of the (sub)type.A type invariant introduced by aspect
Type_Invariant
orInvariant
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.
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 with 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:
1package Logging_Discr with
2 SPARK_Mode
3is
4 type Log_Kind is (Min_Max_Values, Last_Values);
5 type Integer_Array is array (Positive range <>) of Integer;
6
7 type Log_Type (Kind : Log_Kind; Capacity : Natural) is record
8 case Kind is
9 when Min_Max_Values =>
10 Min_Entry : Integer;
11 Max_Entry : Integer;
12 when Last_Values =>
13 Log_Data : Integer_Array (1 .. Capacity);
14 Log_Size : Natural;
15 end case;
16 end record;
17
18 subtype Min_Max_Log is Log_Type (Min_Max_Values, 0);
19 subtype Ten_Values_Log is Log_Type (Last_Values, 10);
20
21 function Log_Size (Log : Log_Type) return Natural;
22
23 function Last_Entry (Log : Log_Type) return Integer with
24 Pre => Log.Kind = Last_Values and then Log.Log_Size in 1 .. Log.Capacity;
25
26end 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:
1package body Logging_Discr with
2 SPARK_Mode
3is
4 function Log_Size (Log : Log_Type) return Natural is
5 begin
6 case Log.Kind is
7 when Min_Max_Values =>
8 return 2;
9 when Last_Values =>
10 return Log.Log_Size;
11 end case;
12 end Log_Size;
13
14 function Last_Entry (Log : Log_Type) return Integer is
15 begin
16 return Log.Log_Data (Log.Log_Size);
17 end Last_Entry;
18
19end 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:10:23: info: discriminant 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:21:13: info: implicit aspect Always_Terminates on "Log_Size" has been proved, subprogram will terminate
logging_discr.ads:23:13: info: implicit aspect Always_Terminates on "Last_Entry" has been proved, subprogram will terminate
logging_discr.ads:24:48: info: discriminant check proved
5.4.3. Predicates
[Ada 2012]
Predicates can be used on any subtype to express a property verified by objects of
the subtype at all times. Aspects Static_Predicate
and Dynamic_Predicate
are defined in Ada to associate a predicate with a subtype. Aspect
Dynamic_Predicate
allows to express more general predicates than aspect
Static_Predicate
, at the cost of restricting the use of variables of the
subtype. The following table summarizes the main similarities and differences
between both aspects:
Feature |
|
|
---|---|---|
Applicable to scalar subtype |
Yes |
Yes |
Applicable to array/record subtype |
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 subtype 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 subtype more than
necessary.
Aspect Ghost_Predicate
is also specific to GNAT and can be used
instead of Dynamic_Predicate
when the predicate expression needs to
reference ghost entities or ghost attributes like Initialized
. In that
case, the subtype cannot be used as subtype_mark in a membership test.
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 (sub)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 subtype with a predicate are
allowed by its predicate (for all forms of predicate: Predicate
,
Static_Predicate
, Dynamic_Predicate
and Ghost_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 subtype, 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 subtype. 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 subtype 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 subtype Normal_Float
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 subtypes that cannot be
expressed as static predicates. For example, we can express that values of subtype
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 subtype 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 subtype 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 type declarations). They express a property
that is only guaranteed outside of the immediate scope of the type bearing the
invariant. Aspect Type_Invariant
is defined in Ada to associate an
invariant with 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 subtype predicates, the name of the type can be used inside the invariant
expression to refer to the current instance of the type. Here the subtype 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 ofP
. Such a subprogram can be either declared in the visible part ofP
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:
1package Logging_Priv with
2 SPARK_Mode
3is
4 Max_Count : constant := 100;
5
6 type Log_Type is private with
7 Default_Initial_Condition => Log_Size (Log_Type) = 0;
8
9 function Log_Size (Log : Log_Type) return Natural;
10
11 procedure Append_To_Log (Log : in out Log_Type; Incr : in Integer) with
12 Pre => Log_Size (Log) < Max_Count;
13
14private
15
16 type Integer_Array is array (1 .. Max_Count) of Integer;
17
18 type Log_Type is record
19 Log_Data : Integer_Array;
20 Log_Size : Natural := 0;
21 end record;
22
23 function Log_Size (Log : Log_Type) return Natural is (Log.Log_Size);
24
25end 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
18>| type Log_Type is record
... | ...
21 | end record;
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).
In general, GNATprove generates checks for the default value of a type when a variable of this type is default initialized. This is not the case for private types, as the default value of a private type declared in a library unit is really the responsibility of the implementer of the library, not the user. If the private type has a known discriminant part, then default checks are done for any values of the discriminants.
If a private type has a Default_Initial_Condition
, then this
condition can act either as a precondition or as a postcondition of the default
value computation. If the Default_Initial_Condition
does not refer to the
current type instance, or if it only refers to its discriminants, then it is
considered to be a precondition: it is the user of the private type who is
responsible for ensuring its validity. As such, the condition is assumed when
checking the default value of the private type, and it is checked each time a
variable of the type is default initialized. For example, in the following
example, we must have First < Last
to be allowed to safely default
initialize our stack type:
type Stack (First, Last : Positive) is private with
Default_Initial_Condition => First < Last;
GNATprove will take advantage of this information when checking the default
value of Stack
for run-time exceptions. For example, it will be able to
ensure that the predicate will hold if Stack
is defined as follows:
type Stack (First, Last : Positive) is record
Content : Nat_Arr (First .. Last) := 0;
Top : Positive := First;
end record with
Predicate => Top in Content'Range;
Otherwise, the Default_Initial_Condition
is handled as a postcondition of
the default value computation. It is checked once and for all when the
definition of the type is analyzed.