Ada Engineering

Module 4 – Make assumptions visible and defend your result

Page 1 of 3 · About 15 minutes per lesson, including practice.

Write the condition a caller must respect

A precondition describes a requirement before a call; a postcondition describes a requirement after a successful return. Here a level may be 0 through 10, but incrementing is permitted only below 10. The result must be exactly one larger. These are useful statements for a human reviewer even before execution.

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;

The example explicitly enables assertion checking with Assertion_Policy (Check). Build it in Ada 2012 or later mode. The two assertions exercise the lowest valid input and the highest input permitted by the precondition. They print a success message only if both checks complete.

Reference: AdaCore: design by contracts.

Reference: GNAT: assertion policy.

Example code on Agila Forge ↗