pragma Assertion_Policy (Check);
with Ada.Text_IO;

procedure Main is
   subtype Level is Integer range 0 .. 10;
   function Next_Level (Current : Level) return Level
     with Pre => Current < Level'Last,
          Post => Next_Level'Result = Current + 1;

   function Next_Level (Current : Level) return Level is
   begin
      return Current + 1;
   end Next_Level;
begin
   pragma Assert (Next_Level (0) = 1);
   pragma Assert (Next_Level (9) = 10);
   Ada.Text_IO.Put_Line ("Two boundary checks passed");
end Main;