在 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 的子类型，而不是实际的新类型。