Ada 2012 Type Invariants and Predicates
Constrained Data Types and Subtypes The Ada language has always had a limited ability to specify type invariants through the definition of range constraints on scalar data types. Along with giving the programmer the ability to specify range constraints, the Ada language has always provided some pre-defined subtypes of the Integer data type. For instance, the subtype Natural is defined as subtype Natural is Integer range 0..Integer’Last; This definition specifies that Natural is an integer with a constrained range of values, in this case the smallest valid Natural value is 0 and the highest is the maximum valid Integer value. Similarly, Ada provides the pre-defined subtype Positive, defined as subtype Positive is Integer range 1..Integer’Last; Type Integer is a signed data type, allowing both positive and negative values, but subtype Positive is an integer that can only contain a positive value. While range specifications are very useful, they are also highly limite...