ada

Subtype of string containing only hex characters in Ada

How can I define a subtype of String that allows only hex characters to be used? Here is my attempt, but I fail at the subtype definition:

subtype Hex_Character is Character
  with Static_Predicate => Hex_Character in 
     'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
subtype Hex_String is String ...;
Solution

  • You could add a dynamic predicate and leverage the dynamic semantics of the membership test. From RM 4.5.2 (29/4):

    An individual membership test yields the result True if:

    • [...]
    • The membership_choice is a subtype_mark, the tested type is scalar, the value of the tested_simple_expression belongs to the range of the named subtype, and the value satisfies the predicates of the named subtype.

    For example:

    main.adb

    procedure Main with SPARK_Mode is

   subtype Hex_Character is Character
     with Static_Predicate => Hex_Character in 
       'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
      
   subtype Hex_String is String
     with Dynamic_Predicate =>
       (for all Char of Hex_String => Char in Hex_Character);
   
   S1 : Hex_String := "ABCDEF1234567890";       -- Line 11
   S2 : Hex_String := "Foo";                    -- Line 12
   
begin
   null;
end Main;

    output (GNATprove)

    $ gnatprove -Pdefault.gpr -u main.adb --level=1 --report=all
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
main.adb:11:23: info: predicate check proved

main.adb:12:23: medium: predicate check might fail, cannot prove Char in Hex_Character
   12 |   S2 : Hex_String := "Foo";
      |                      ^~~~~
  in inlined predicate at main.adb:9
Summary logged in ./obj/gnatprove/gnatprove.out