Ada 2012 Type Invariants and Predicates

Constrained Data Types and Subtypes

The Ada language has always had a limited ability to specify type invariants through the definition of range constraints on scalar data types. Along with giving the programmer the ability to specify range constraints, the Ada language has always provided some pre-defined subtypes of the Integer data type. For instance, the subtype Natural is defined as

subtype Natural is Integer range 0..Integer’Last;

This definition specifies that Natural is an integer with a constrained range of values, in this case the smallest valid Natural value is 0 and the highest is the maximum valid Integer value. Similarly, Ada provides the pre-defined subtype Positive, defined as

subtype Positive is Integer range 1..Integer’Last;

Type Integer is a signed data type, allowing both positive and negative values, but subtype Positive is an integer that can only contain a positive value.

While range specifications are very useful, they are also highly limited in their usefulness. Ada ranges must always be contiguous. This means that you cannot specify an integer data type of only even numbers, for instance. Even numbers are not contiguous.

More general type invariants are made available in the Ada 2012 language. There are two kinds of type invariants: static invariants and dynamic invariants. A static invariant is one that can be determined at compile time, such as a discrete list of valid values. Type invariants are contractual within a program.

Subtype predicates, on the other hand are more like value constraints, similar to a range constraint on a subtype. A dynamic predicate can be used, for instance, to define a subtype containing only even numbers.

subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;

A  dynamic predicate allows the definition of a type that must be evaluated at run-time. In the case above every value in the subtype Even must satisfy the Dynamic_Predicate.

A Prime Number subtype

I decided to explore the possibility of creating a constrained subtype that only contains prime numbers. I wanted to understand how complex it would be to define such a type, and how inefficient such a subtype might be to use.

Table 1 Primes package specification

------------------------------------------------------------------ -- This package defines a subtype of integer                    -- -- All valid values in this subtype are prime numbers           -- ------------------------------------------------------------------ package Primes is    subtype Prime_Num is Integer with    Dynamic_Predicate => Is_Prime(Prime_Num);       -- Primality Test    function Is_Prime(Item : Positive) return Boolean;       -- Return the smallest prime number greater than the parameter    function Next(Item : Positive) return Prime_Num      with Pre => Item < Integer'Last;       -- Return the greatest prime number less than the parameter    function Previous(Item : Positive) return Prime_Num      with Pre => Item > 2; end Primes;

This was encouraging. Defining a prime number integer data type is very simple. The Dynamic_Predicate expression must evaluate to True or False, so I created a primality test returning a Boolean value. I added functions Next and Previous to allow iteration through the set of values in my Prime_Num type. Note that I called this a set of values and not a range of values. The set of prime numbers is very much discontinuous.

The package body for the Primes package reveals how simple the three functions actually are.

Table 2 Primes package body

with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions; package body Primes is    --------------    -- Is_Prime --    --------------    function Is_Prime (Item : Positive) return Boolean is       T : Positive := 2;       Limit : Integer := Integer(Sqrt(Float(Item)));    begin       if Item = 2 then          return True;       end if;       while T <= Limit loop          if Item rem T = 0 then             return False;          end if;          T := T + (if T = 2 then 1 else 2);       end loop;       return True;    end Is_Prime;    ----------    -- Next --    ----------    function Next (Item : Positive) return Prime_Num is       Value : Integer := Item + 1;    begin       while Value <= Integer'Last loop          if Value in Prime_Num then             return Value;          end if;          Value := Value + 1;       end loop;       return Item;    end Next;    --------------    -- Previous --    --------------    function Previous (Item : Positive) return Prime_Num is       Value : Integer := Item - 1;    begin       while Item >= 2 loop          if Value in Prime_Num then             return Value;          end if;          Value := Value - 1;       end loop;       return Item;    end Previous; end Primes;

The Is_Prime function is a slight modification of a naïve primality test. The function Next tests the values greater than the parameter passed to it and returns the first prime number it encounters. Notice that the test within the Next function is a simple type membership test. That membership test is based upon the Dynamic_Predicate specified for the subtype Prime_Num. In other words, it returns the result of the Is_Prime function. Similarly, the Previous function searches the integers less than the parameter for the first value that is in the Prime_Num subtype, and returns that value. If there is no prime number within the range of Integer that is greater than the parameter passed to Next, the function simply returns the parameter. A dynamic predicate is checked as a post-condition for every function returning a value of the type with that dynamic predicate. If the Next function returns a value that is not a prime number the function will raise an Assertion Error exception.

What then is the inefficiency associated with using a Dynamic_Predicate? As you can see, the function called within the Dynamic_Predicate is called twice in both the Next and Previous functions. One time within the body of the function and another time as a post-condition check of the function.

The following is a test program I created to measure the time required to execute the Next and Previous functions for the Prime_Num subtype.

Table 3 Primes test program

------------------------------------------------------------------ -- Primes Test                                                  -- ------------------------------------------------------------------ with Ada.Text_Io; use Ada.Text_IO; with Primes; use Primes; with Ada.Calendar; use Ada.Calendar; procedure Primes_Test is    package Int_Io is new Ada.Text_IO.Integer_IO(Integer);    use Int_IO;    T_Start : Time;    T_End   : Time;    P       : Prime_Num; begin    Put_Line("Test the Next function to generate the next prime number");    for Num in 1..20 loop       Put(Item => Num, Width => 12);       Put(" =>");       T_Start := Clock;       P := Next(Num);       T_End := Clock;       Put(Item => P, Width => 12);       Put("   duration:" & Duration'Image(T_End - T_Start) &          " seconds");       New_Line;    end loop;    New_Line;    Put_Line("Test the Previous function");    for num in reverse Integer'Last - 20 .. Integer'Last loop       Put(Item => Num, Width => 12);       Put(" =>");       T_Start := Clock;       P := Previous(Num);       T_End := Clock;       Put(Item => P, Width => 12);       Put("   duration:" & Duration'Image(T_End - T_Start) &          " seconds");       New_Line;    end loop; end Primes_Test;

As you can see, I instrumented the calls to Next and Previous so that I could capture the elapsed time spent in those calls.

For reference purposes, the results below were obtained using a system with an AMD A10-5700 APU operating at 3.40 GHz, using the Windows 10 operating system.

Test the Next function to generate the next prime number            1 =>           2   duration: 0.000001414 seconds            2 =>           3   duration: 0.000000283 seconds            3 =>           5   duration: 0.000000566 seconds            4 =>           5   duration: 0.000000283 seconds            5 =>           7   duration: 0.000000283 seconds            6 =>           7   duration: 0.000000283 seconds            7 =>          11   duration: 0.000000566 seconds            8 =>          11   duration: 0.000000566 seconds            9 =>          11   duration: 0.000000283 seconds           10 =>          11   duration: 0.000000282 seconds           11 =>          13   duration: 0.000000283 seconds           12 =>          13   duration: 0.000000283 seconds           13 =>          17   duration: 0.000000282 seconds           14 =>          17   duration: 0.000000566 seconds           15 =>          17   duration: 0.000000283 seconds           16 =>          17   duration: 0.000000566 seconds           17 =>          19   duration: 0.000000282 seconds           18 =>          19   duration: 0.000000283 seconds           19 =>          23   duration: 0.000000849 seconds           20 =>          23   duration: 0.000000566 seconds Test the Previous function   2147483647 =>  2147483629   duration: 0.000217217 seconds   2147483646 =>  2147483629   duration: 0.000217217 seconds   2147483645 =>  2147483629   duration: 0.000218913 seconds   2147483644 =>  2147483629   duration: 0.000216934 seconds   2147483643 =>  2147483629   duration: 0.000216652 seconds   2147483642 =>  2147483629   duration: 0.000216652 seconds   2147483641 =>  2147483629   duration: 0.000204772 seconds   2147483640 =>  2147483629   duration: 0.000204489 seconds   2147483639 =>  2147483629   duration: 0.000204490 seconds   2147483638 =>  2147483629   duration: 0.000204772 seconds   2147483637 =>  2147483629   duration: 0.000204206 seconds   2147483636 =>  2147483629   duration: 0.000204207 seconds   2147483635 =>  2147483629   duration: 0.000204206 seconds   2147483634 =>  2147483629   duration: 0.000204490 seconds   2147483633 =>  2147483629   duration: 0.000179317 seconds   2147483632 =>  2147483629   duration: 0.000179317 seconds   2147483631 =>  2147483629   duration: 0.000179317 seconds   2147483630 =>  2147483629   duration: 0.000179034 seconds   2147483629 =>  2147483587   duration: 0.000283683 seconds   2147483628 =>  2147483587   duration: 0.000283965 seconds   2147483627 =>  2147483587   duration: 0.000283683 seconds

As expected, it takes a lot longer to calculate the next or previous prime number for a very large number than it does for a small number.