Syntax:
pragma Post (Boolean_Expression);
The Post pragma is intended to be an exact replacement for
the language-defined
Post aspect, and shares its restrictions and semantics.
It must appear either immediately following the corresponding
subprogram declaration (only other pragmas may intervene), or
if there is no separate subprogram declaration, then it can
appear at the start of the declarations in a subprogram body
(preceded only by other pragmas).
This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section 11.4.2.