6.A. Type contracts: Predicates - JulTob/Ada GitHub Wiki

Range checks are a special form of type contracts; a more general method is provided by Ada subtype predicates.

Introduced in Ada 2012.

A subtype predicate is a boolean expression defining conditions that are required for a given type or subtype.

For example:

subtype Dice_Throw is Integer
   with Dynamic_Predicate => Dice_Throw in 1 .. 6;

The clause beginning with with introduces an Ada ‘aspect’, which is additional information provided for declared entities such as types and subtypes.

The Dynamic_Predicate aspect is the most general form.

Within the predicate expression, the name of the (sub)type refers to the current value of the (sub)type.

The predicate is checked on assignment, parameter passing, and in several other contexts.

There is a “Static_Predicate” form which introduce some optimization and constrains on the form of these predicates.

Of course, predicates are useful beyond just expressing ranges.

They can be used to represent types with arbitrary constraints, in particular types with discontinuities, for example:

type Not_Null is new Integer
   with Dynamic_Predicate => Not_Null /= 0;

type Even is new Integer
   with Dynamic_Predicate => Even mod 2 = 0;