Gem #148 : Su(per)btypes in Ada 2012 - Part 3

by Yannick Moy —AdaCore

In the previous two Gems, we saw how aspects Static_Predicate and Dynamic_Predicate can be used to state properties of objects that should be respected at all times. This third and final Gem in the series is concerned with an aspect called Type_Invariant.

The Type_Invariant aspect can be used with private types, to define a property that all objects of the types should respect outside of the package where the types are declared. Take for example a type Communication storing the messages between various parties, based on the Message type used in the previous Gem:

package Communications is
   type Message_Arr is array (Integer range <>) of Message;
   type Communication (Num : Positive) is private;
private
   type Communication (Num : Positive) is record
      Msgs : Message_Arr (1 .. Num);
   end record;
end Communications;

To state that messages should be ordered by date of reception, we can add the aspect to the full type:

type Communication (Num : Positive) is record
   Msgs : Message_Arr (1 .. Num);
end record with
  Type_Invariant =>
    (for all Idx in 1 .. Communication.Num-1 =>
      Communication.Msgs(Idx).Received <= Communication.Msgs(Idx+1).Received);

The compiler will insert run-time checks to ensure that this property holds at prescribed locations in the code:

• at object initialization (including by default!)
• on conversions to the type
• when returning an object from a public function defined in the type's package
• on out and in out parameters, when returning from a public procedure of the type's package

For example, consider the following incorrect code that fails to initialize Com to a correct value satisfying the invariant:

Com : Communication (2);  -- incorrect

Compiling it with assertions and running it leads to the following error:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed invariant from communications.ads:16

But if we give the object an explicit value, through a creation function Create defined in unit Communications, then the object declaration is elaborated without errors:

Coms : Communication (2) := Create (A);

Inside the Create function, the initialization of Coms must respect the invariant, but after that, the invariant could be violated between the time Coms is declared, and the time it is returned.

function Create (A : Message_Arr) return Communication is
   Coms : Communication := (Num => A'Length, Msgs => A);
begin
   -- statements before the return might violate the invariant
   return Coms;
end Create;

Ada requires that the type invariant be checked on every part of a parameter that has type Communication, where a part can be a component of a record, or an element of an array, or any such combination. For example, it is checked on every element of the array returned by Create_N or potentially modified by Update_N:

type Communication_Arr is array (Integer range <>) of Communication;
function Create_N return Communication;
procedure Update_N (A : in out Communication_Arr);

Importantly, the invariant is not checked on subprograms declared in the private part or in the package body. These subprograms are internal operations, and should be callable on objects whose invariant does not hold. Likewise, the invariant is not checked on parameters of mode in, for example on query functions used in the definition of the type invariant itself. This is fortunate, since otherwise this would easily cause infinite loops!

As a side note, it's worth mentioning that GNAT also provides an aspect with the name Invariant, which is a synonym for the Type_Invariant aspect (and implemented before Type_Invariant appeared in Ada 2012).

This Gem ends the series of three Gems on su(per)btypes in Ada. Together with Static_Predicate and Dynamic_Predicate, Type_Invariant provides new ways to state properties of your data, both in new and existing programs, so try them out!

About the Author