A reviewed progress component

The challenge

Extend the level component with a clearly specified operation of your own. Submit both successful and expected-failure evidence plus a reviewable explanation.

Evidence to include

• Record the allowed inputs and promised result.
• Keep assertion checking enabled and record compiler settings.
• Test low and high valid inputs and one precondition violation separately.
• Demonstrate that a deliberately wrong body is caught, then restore it.
• Explain a remaining limitation and identify one next learning step.

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;

Save your practice

Sign in to save a project submission.