Gem #146 : Su(per)btypes in Ada 2012 - Part 1

by Yannick Moy —AdaCore

Let's get started...

Ada 2012 is full of features for specifying a rich set of type properties. In this series of three Gems, we describe three aspects that can be used to state invariant properties of types and subtypes. This first Gem is concerned with the Static_Predicate aspect.

Static_Predicate can be specified on scalar types and subtype definitions to state a property that all objects of the subtype must respect at all times. Take for example a type Day representing the days of the week:

type Day is (Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday);

To state that T_Day is the (sub)type of days whose name starts with a 'T', we can write:

type T_Day is new Day with Static_Predicate => T_Day in Tuesday | Thursday;

or

subtype T_Day is Day with Static_Predicate => T_Day in Tuesday | Thursday;

Now the compiler will warn about a program that assigns a value statically known to be different from Tuesday or Thursday to a T_Day object.

We'll proceed with using the second definition above. For example, on this incorrect code:

D : T_Day := Day'First; -- Incorrect

GNAT generates the following warning at compile time:

>>> warning: static expression fails static predicate check on "T_Day"

The compiler also checks the completeness of case expressions and case statements involving T_Day arguments. For example, on this code:

   case D is
      when Tuesday => ...
      when Friday => ...  -- Incorrect
   end case;

GNAT generates the following errors at compile time:

>>> missing case value: "Thursday"
>>> static predicate on "T_Day" excludes value "Friday"

If Friday is replaced by the correct value Thursday, then the code compiles quietly.

Finally, the compiler generates run-time checks for any erroneous write of a day other than Tuesday or Thursday in an object of type T_Day, which makes it easy to detect violations of the predicate of a type as soon as it occurs! Note that to enable run-time checking of Static_Predicate (and other kinds of assertions specified by aspects) it's necessary to compile with the switch -gnata (or else enable assertion checking with the pragma Assertion_Policy).

For example, suppose we have a procedure Next that advances its argument to the next day, and we want to define a similar procedure, Next_T, that advances its argument of subtype T_Day. Here's the definition of procedure Day:

procedure Next (D : in out Day) is
begin
   if D = Sunday then
      D := Monday;
   else
      D := Day'Succ (D);
   end if;
end Next;

Following is a failed attempt at defining Next_T:

procedure Next_T (D : in out T_Day) is
begin
   Next (D); -- Incorrect
   while D not in T_Day loop
      Next (D);
   end loop;
end Next_T;

Let's add a test of this code:

with Days; use Days;
procedure Main is
   D : T_Day := Tuesday;
begin
   Next_T (D);
end Main;

When this code is compiled with assertions enabled (-gnata) and run, it issues a run-time error:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Static_Predicate failed at days.adb:3

This points to the first line where Next is called in Next_T. Indeed, on entry to Next_T, the value of D is Tuesday, so Next returns Wednesday, which does not satisfy the Static_Predicate of T_Day, but is assigned to a T_Day, hence triggering a run-time error. The correct version of Next_T uses a temporary variable of type T_Day'Base, which strips off all constraints from T_Day, including the predicate if present:

procedure Next_T (D : in out T_Day) is
   Tmp : T_Day'Base := D;
begin
   Next (Tmp);
   while Tmp not in T_Day loop
      Next (Tmp);
   end loop;
   D := Tmp;
end Next_T;

In the next Gem in this series we'll see how to use a related aspect called Dynamic_Predicate.

About the Author