3.10 Default_Initial_Condition for types

Default_Initial_Condition for types (AI12-0265) introduces a new contract aspect, Default_Initial_Condition (see RM 7.3.3), which may be specified for a private type (or private extension). As with other contracts, it tells the reader and analysis tools what to expect, in this case what the properties of a default initialised object of a type should be.

After the successful default initialisation of an object of the type, a default initial condition check is performed. Since the behaviour of this check does not depend on how the private type is used, the check can only fail if the implementation (or the contract) is incorrect. In the case of a controlled type, the check is performed after the call to the type's Initialize procedure. For example:

package Sets is
   type Set is private
      with Default_Initial_Condition => Is_Empty (Set);
   function Is_Empty (S : Set) return Boolean;
   ...
end Sets;