我如何强制类型保持只能是一组固定的非连续值？

Question

当我将 3 作为有效的 Scale 值提供给它时​​，我期望这个程序会引发错误，但没有这样的运气：

with Ada.Text_IO; use Ada.Text_IO;

procedure predicate is
   type Scale is new Integer
      with Dynamic_Predicate => Scale in 1 | 2 | 4 | 8;
   GivesWarning : Scale := 3; -- gives warning
begin
   Put_Line ("Hello World");
   loop
      Put_Line ("Gimme a value");
      declare
         AnyValue : Integer := Integer'Value (Get_Line);
         S : Scale := Scale (AnyValue); -- no check done!
      begin
         Put_Line ("okay, that works" & S'Image);
      end;
   end loop;
end predicate;

我发现了这个相关的问题，但要求是使用枚举。解决方案是从枚举 -> 值定义一个数组。

我想要一些至少在编译时给我警告的东西，并允许我在运行时检查，如果我尝试输入无效值，则会引发错误。然后，如果我可以使用 SPARK 来证明没有可能会出现无效值，我可以关闭上述检查。我的印象是这就是 Static_/Dynamic_ 谓词的工作方式，所以上面的例子让我大吃一惊。

Answer 1

您需要启用断言。编译-gnata或设置适当的Assertion_Policy

pragma Assertion_Policy(Dynamic_Predicate => Check);