Gem #147 : Su(per)btypes in Ada 2012 - Part 2

by Yannick Moy —AdaCore

Let's get started...

The previous Gem in this series showed how the aspect Static_Predicate can be used to state properties of scalar objects that should be respected at all times. This Gem is concerned with the Dynamic_Predicate aspect, which can be used on all type and subtype declarations (not just scalar ones).

Consider for example a type Message encoding the dates when a message was sent and received, where dates are represented by strings, such as "1789-07-14" for the fourteenth of July 1789:

type Day is new String (1 .. 10);

type Message is record
   Sent     : Day;
   Received : Day;
end record;

To state that a message reception date should always be greater than the date it was sent, we can write:

type Message is record
   Sent     : Day;
   Received : Day;
end record with
  Dynamic_Predicate => Message.Sent <= Message.Received;

Note that the type name itself is used as a prefix of the components named in the predicate. In this context the name of the type denotes what Ada calls the current instance of the type, which at run time will denote the actual object the predicate is applied to.

In contrast to Static_Predicate, the compiler cannot determine in general if a Dynamic_Predicate will fail, so it inserts run-time checks at certain required locations in the code:

• when assigning to a variable of the subtype
• when passing an input parameter of the subtype
• when returning an output parameter to an object of the subtype
• when converting a value to the subtype

For example, on the following incorrect code:

M : Message := (Received => "1776-07-04", Sent => "1783-09-03");  --  incorrect

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

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Dynamic_Predicate failed at main.adb:3

If the values of the Sent and Received components are corrected to reflect the actual event ordering of the proclamation of the Independence of the United States and the date of the treaty of Paris ending the American Revolutionary War, then the generated code executes without errors.

Beware that no run-time checks are inserted when assigning to individual components, so the predicate can be silently violated between assignments and calls. For example, if the definition above separately assigns each component of M, even if the value for Received and Sent are appropriately ordered:

   M : Message;  --  incorrect
begin
   M.Received := "1783-09-03";  --  incorrect
   M.Sent := "1776-07-04";      --  predicate is correct here

This code does not lead to a run-time failure, but if we pass the message before it is completely initialized to some procedure Process taking it as input parameter:

procedure Process (M : Message);

Compiling the resulting code with assertions and running it again leads to an error:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Dynamic_Predicate failed at main.adb:7

Note that Dynamic_Predicate is more flexible than Static_Predicate: it can be applied to more forms of types and more general predicate expressions. For example, the mod operator is not allowed outside a static expression in a Static_Predicate, so the type of odd numbers must be defined with a Dynamic_Predicate:

subtype Odd is Integer with Dynamic_Predicate => Odd mod 2 = 1;

Likewise, a user function can be called in a Dynamic_Predicate, but not in a Static_Predicate.

GNAT conveniently provides an aspect Predicate that can be used anywhere a Dynamic_Predicate is allowed, and analyzes it as a Static_Predicate when possible.

In the next and final Gem in this series on type and subtype contracts we'll look at a related aspect called Type_Invariant.

About the Author