Constrain or subtype an Unbounded_String in Ada with rules?

Question

new to Ada but loving it so far. I'm probably asking this question in a noob way since I'm sort of just muddling through writing something useful as my foray, but here goes:

I've got a system which uses Unbounded_Strings and I wanted to apply some rules to them, namely things like whether the length was divisible by n or which characters they could contain. Is there a neat way of going about this so that I can lean on the type system for the validation?

Answer 1

You can ask the type system to check values as they are assigned to variables, with Dynamic_Predicate aspects:

with Ada.Strings.Unbounded;
package UB_Preds
is
   use Ada.Strings.Unbounded;

   subtype Even_Length_String is Unbounded_String
   with Dynamic_Predicate => Length(Even_Length_String) mod 2 = 0;

   subtype Lower_Case_String is Unbounded_String
   with Dynamic_Predicate =>
      (for all C of To_String(Lower_Case_String) => C in 'a' .. 'z');

end UB_Preds;

Example of usage: if you compile with assertion checks enabled (-gnata for GNAT), these declarations will raise Assert_Failure because the assigned value fails the predicate of the subtype:

Odd : UB_Preds.Even_Length_String := To_Unbounded_String ("ABC");
UC : UB_Preds.Lower_Case_String := To_Unbounded_String ("aBc");

The first one has three characters, so Length mod 2 /= 0, while the second has an upper-case character.

In general, the enabling/disabling of assertion checks is controlled with pragma Assertion_Policy. The default for GNAT is to ignore assertions, but -gnata enables them.

(Of course, if you use any character set other than 7-bit ASCII, you should use Ada.Characters.Handling to test for lower/upper case, not the simple range that the example above uses.)