Subtype Predicates, Type Invariants & Default_Initial_Condition

Constrain subtypes with Static_Predicate (non-contiguous sets usable in case statements and loops) and Dynamic_Predicate (arbitrary conditions), protect private types with Type_Invariant, specify Default_Initial_Condition, and know when each is checked.

Ranges express simple constraints like 1 .. 100, but real rules are often richer: weekend days, even numbers, sorted arrays, an interval whose low bound never exceeds its high bound. Predicates attach such rules to subtypes; invariants attach them to private types. The rules are then checked automatically wherever values enter the subtype or leave the package.

Static and Dynamic Predicates

'subtype Weekend is Day with Static_Predicate => Weekend in Sat | Sun;' defines a non-contiguous subtype. Static predicates are restricted to membership tests and simple comparisons against static values, but in return they can be used as case choices and in for loops (for D in Weekend loops over Sat and Sun only). 'subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;' allows any Boolean expression — even quantified ones for arrays (Sorted_Array) — but cannot be looped over. The current instance is named by the subtype name inside the predicate.

Predicates are checked on assignment, initialization, parameter passing (in and out) and conversion to the subtype; a failure raises Assertion_Error with 'Dynamic_Predicate failed at ...' (or Static_Predicate). Membership tests (X in Even) evaluate the predicate without raising. Predicates are not rechecked when you modify a component of a composite object in place, so prefer them for scalars and immutable values.

• Static_Predicate: static membership sets; usable in case and for loops. • Dynamic_Predicate: any condition; not loopable. • Checked on assignment, parameters, conversions → Assertion_Error. • Component-level updates do not recheck.

Type Invariants and Default_Initial_Condition

'type Interval is private with Type_Invariant => Low (Interval) <= High (Interval);' states a property that must hold for every Interval visible outside the package. It is checked after default initialization, conversions, and on return from every public subprogram that produces or updates an Interval (and for in out/out parameters). Inside the package the invariant may be temporarily broken. Default_Initial_Condition (DIC) states what is true of a default-initialized object, e.g. 'type Stack is private with Default_Initial_Condition => Is_Empty (Stack);' — a useful contract for SPARK.

• Type_Invariant on private types; checked at the package boundary. • May be broken temporarily inside the package body. • Default_Initial_Condition specifies default-initialized state. • Type_Invariant'Class for tagged hierarchies.

Code Examples

Loops over static-predicate subtypes visit only the members. 4 + 3 = 7 violates Even; [3, 1, 2] violates Sorted_Array; Set_Low (50) on 5.. 10 violates the Interval invariant when Set_Low returns. Output: Weekend days: SAT SUN Odd digits: 1 3 5 7 9 Sun in Weekend? TRUE, Wed in Weekend? FALSE Sorted_Array accepted, length 4 Even:= 7 -> Dynamic_Predicate failed at l44_predicates.adb:68 Unsorted array -> Dynamic_Predicate failed at l44_predicates.adb:76 Interval now 5.. 10 Set_Low (50) -> failed invariant from l44_predicates.adb:24 subtype Weekend is Day range Sat.. Sun; -- then needing Mon | Sat | Sun subtype Off_Day is Day with Static_Predicate => Off_Day in Mon | Sat | Sun;

Ranges are contiguous; predicates express arbitrary sets.

for N in Even loop for N in 0.. 100 loop if N in Even then...

You cannot iterate over a subtype with a dynamic predicate.

type Interval is record... end record with Type_Invariant =>...; -- visible record type Interval is private with Type_Invariant =>...;

Type invariants apply to private types, where the package controls all updates.

Which predicate can be used in a for loop? A. Dynamic_Predicate B. Static_Predicate C. Both D. Neither

When is a Type_Invariant checked? A. After every statement B. When values cross the package boundary (e.g. on return from public subprograms) C. Only at program start D. Never at run time

What does 'X in Even' do if X = 7? A. Raises Assertion_Error B. Returns False C. Compile error D. Returns True

B. Membership tests evaluate predicates without raising.

Which aspect specifies the state of a default-initialized private object? A. Default_Value B. Default_Initial_Condition C. Initial_Invariant D. Pre Trace the predicate example.

Real output: Weekend days: SAT SUN Odd digits: 1 3 5 7 9 Sun in Weekend? TRUE, Wed in Weekend? FALSE Sorted_Array accepted, length 4 Even := 7 -> Dynamic_Predicate failed at l44_predicates.adb:68 Unsorted array -> Dynamic_Predicate failed at l44_predicates.adb:76 Interval now 5 .. 10 Set_Low (50) -> failed invariant from l44_predicates.adb:24

with Ada.Text_IO;    use Ada.Text_IO;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Assertions;

procedure L44_Predicates is
   type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

   --  Static predicate: a non-contiguous subset, usable in case statements and loops
   subtype Weekend is Day with Static_Predicate => Weekend in Sat | Sun;
   subtype Odd_Digit is Integer with Static_Predicate => Odd_Digit in 1 | 3 | 5 | 7 | 9;

   --  Dynamic predicate: any Boolean expression
   subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;

   type Int_Array is array (Positive range <>) of Integer;
   subtype Sorted_Array is Int_Array
     with Dynamic_Predicate =>
       (for all I in Sorted_Array'First .. Sorted_Array'Last - 1 =>
          Sorted_Array (I) <= Sorted_Array (I + 1));

   --  Type invariant: holds for a private type whenever clients can observe it
   package Ranges is
      type Interval is private
        with Type_Invariant => Low (Interval) <= High (Interval);
      function Make (L, H : Integer) return Interval;
      function Low (I : Interval) return Integer;
      function High (I : Interval) return Integer;
      procedure Set_Low (I : in out Interval; L 
…