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.

Comments

Popular posts from this blog

Comparing Ada and High Integrity C++

An Ada Publish-Subscribe Producer-Consumer Exercise

Ada vs C++ Bit-fields