ada - 我如何强制一个类型只包含一组固定的非连续值？

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;

我找到了 this related question ，但要求是使用枚举。解决方案是从枚举 -> 值定义一个数组。

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

Answer 1

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

pragma Assertion_Policy(Dynamic_Predicate => Check);