string - 使用规则约束或子类型 Ada 中的 Unbounded_String？

Question

Ada 的新手，但到目前为止喜欢它。我可能是在以菜鸟的方式问这个问题，因为我在尝试写一些有用的东西时有点糊涂，但这里是:
我有一个使用 Unbounded_String 的系统s 和我想对它们应用一些规则，即长度是否可以被 n 整除。或者它们可以包含哪些字符。有没有一种巧妙的方法来解决这个问题，以便我可以依靠类型系统进行验证？

Answer 1

您可以使用 Dynamic_Predicate 方面要求类型系统检查分配给变量的值:

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;

用法示例:如果您在启用断言检查的情况下进行编译(GNAT 为 -gnata)，这些声明将引发 Assert_Failure，因为分配的值未通过子类型的谓词:

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

第一个有三个字符，所以 Length mod 2/= 0，而第二个有一个大写字符。
通常，断言检查的启用/禁用由编译指示 Assertion_Policy 控制。 GNAT 的默认设置是忽略断言，但 -gnata 会启用它们。
(当然，如果您使用 7 位 ASCII 以外的任何字符集，您应该使用 Ada.Characters.Handling 来测试小写/大写，而不是上面示例使用的简单范围。)