2.137 Pragma Precondition

Syntax:

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

The Precondition pragma is similar to Postcondition except that the corresponding checks take place immediately upon entry to the subprogram, and if a precondition fails, the exception is raised in the context of the caller, and the attribute ’Result cannot be used within the precondition expression.

Otherwise, the placement and visibility rules are identical to those described for postconditions. The following is an example of use within a package spec:

package Math_Functions is
   ...
   function Sqrt (Arg : Float) return Float;
   pragma Precondition (Arg >= 0.0)
   ...
end Math_Functions;

Precondition pragmas may appear either immediately 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).

Note: precondition 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 precondition checking is enabled.

Note that pragma Precondition differs from the language-defined Pre aspect (and corresponding Pre pragma) in allowing multiple occurrences, allowing occurences in the body even if there is a separate spec, and allowing a second string parameter, and the use of the pragma identifier Check. Historically, pragma Precondition was implemented prior to the development of Ada 2012, and has been retained in its original form for compatibility purposes.