Описание типа String в Ada

Question

У меня есть тип, похожий на:

type ID is new String (1 .. 7);
-- Example: 123-456

Как я могу указать этот формат в коде, либо с Ada или SPARK?

Я думал о Static_Predicate, но условие, что строка должна начинаться с 3 положительных целых чисел, за которыми следует тире, за которым следует другой набор из 3 положительных целых чисел, не может быть описано с помощью Static_Predicate выражение.

Answer 1

Вы должны использовать Dynamic_Predicate за это:

type ID is new String (1 .. 7)
  with Dynamic_Predicate => (for all I in ID'Range =>
                               (case I is
                                   when 1 .. 3 | 5 .. 7 => ID (I) in '0' .. '9',
                                   when 4               => ID (I) in '-'));

Я использую это совсем немного, но я в основном делаю подтипы типов String вместо актуальных новых типов.