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
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.
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 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:
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: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: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 2012 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 | Static_Predicate |
Dynamic_Predicate |
---|---|---|
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.
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 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 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 2012 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:
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).