How do I enforce that a type hold only be a fixed set of non-contiguous values?

user_2144408 0
Viewed 62

I was expecting this program to raise an error when I feed it 3 as a valid Scale value, but no such luck:

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;

I found this related question, but there the requirement is to use an enum., and the solution is to define an array from enum -> value.

I want something that gives me at least a warning at compile time, and allows me to check at runtime as well, and that raises an error if I try to put an invalid value in. Then, if I can use SPARK to prove that no invalid values can occur, I could turn off said checks. I was under the impression that this was how Static_ / Dynamic_ predicates work, so the example above took me by surprise.

ada
1 Answers

You need to enable assertions. Either compile with -gnata or set an appropriate Assertion_Policy

pragma Assertion_Policy(Dynamic_Predicate => Check);
user_15680100
Related