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