pragma Postcondition ( [Check =>] Boolean_Expression [,[Message =>] String_Expression]);
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.
Furthermore, 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
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
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
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.