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 predefined 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
predefined 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 runtime. 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 postcondition 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 postcondition 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 A105700 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
Post a Comment