Pragma Postcondition

Syntax:

     pragma Postcondition (
        [Check   =>] Boolean_Expression
      [,[Message =>] String_Expression]);

The Postcondition pragma allows specification of automatic postcondition checks for subprograms. These checks are similar to assertions, but are automatically inserted just prior to the return statements of the subprogram with which they are associated (including implicit returns at the end of procedure bodies and associated exception handlers).

In addition, the boolean expression which is the condition which must be true may contain references to function'Result in the case of a function to refer to the returned value.

Postcondition pragmas may appear either immediate following the (separate) declaration of a subprogram, or at the start of the declarations of a subprogram body. Only other pragmas may intervene (that is appear between the subprogram declaration and its postconditions, or appear before the postcondition in the declaration sequence in a subprogram body). In the case of a postcondition appearing after a subprogram declaration, the formal arguments of the subprogram are visible, and can be referenced in the postcondition expressions.

The postconditions are collected and automatically tested just before any return (implicit or explicit) in the subprogram body. A postcondition is only recognized if postconditions are active at the time the pragma is encountered. The compiler switch gnata turns on all postconditions by default, and pragma Check_Policy with an identifier of Postcondition can also be used to control whether postconditions are active.

The general approach is that postconditions are placed in the spec if they represent functional aspects which make sense to the client. For example we might have:

        function Direction return Integer;
        pragma Postcondition
         (Direction'Result = +1
            or else
          Direction'Result = -1);

which serves to document that the result must be +1 or -1, and will test that this is the case at run time if postcondition checking is active.

Postconditions within the subprogram body can be used to check that some internal aspect of the implementation, not visible to the client, is operating as expected. For instance if a square root routine keeps an internal counter of the number of times it is called, then we might have the following postcondition:

        Sqrt_Calls : Natural := 0;
     
        function Sqrt (Arg : Float) return Float is
          pragma Postcondition
            (Sqrt_Calls = Sqrt_Calls'Old + 1);
          ...
        end Sqrt

As this example, shows, the use of the Old attribute is often useful in postconditions to refer to the state on entry to the subprogram.

Note that postconditions are only checked on normal returns from the subprogram. If an abnormal return results from raising an exception, then the postconditions are not checked.

If a postcondition fails, then the exception System.Assertions.Assert_Failure is raised. If a message argument was supplied, then the given string will be used as the exception message. If no message argument was supplied, then the default message has the form "Postcondition failed at file:line". The exception is raised in the context of the subprogram body, so it is possible to catch postcondition failures within the subprogram body itself.

Within a package spec, normal visibility rules in Ada would prevent forward references within a postcondition pragma to functions defined later in the same package. This would introduce undesirable ordering constraints. To avoid this problem, all postcondition pragmas are analyzed at the end of the package spec, allowing forward references.

The following example shows that this even allows mutually recursive postconditions as in:

     package Parity_Functions is
        function Odd  (X : Natural) return Boolean;
        pragma Postcondition
          (Odd'Result =
             (x = 1
               or else
             (x /= 0 and then Even (X - 1))));
     
        function Even (X : Natural) return Boolean;
        pragma Postcondition
          (Even'Result =
             (x = 0
               or else
             (x /= 1 and then Odd (X - 1))));
     
     end Parity_Functions;

There are no restrictions on the complexity or form of conditions used within Postcondition pragmas. The following example shows that it is even possible to verify performance behavior.

     package Sort is
     
        Performance : constant Float;
        --  Performance constant set by implementation
        --  to match target architecture behavior.
     
        procedure Treesort (Arg : String);
        --  Sorts characters of argument using N*logN sort
        pragma Postcondition
          (Float (Clock - Clock'Old) <=
             Float (Arg'Length) *
             log (Float (Arg'Length)) *
             Performance);
     end Sort;

Note: postcondition pragmas associated with subprograms that are marked as Inline_Always, or those marked as Inline with front-end inlining (-gnatN option set) are accepted and legality-checked by the compiler, but are ignored at run-time even if postcondition checking is enabled.