Syntax:
pragma Assume ( boolean_EXPRESSION [, string_EXPRESSION]);
The effect of this pragma is identical to that of pragma Assert,
except that in an Assertion_Policy pragma, the identifier
Assume is used to control whether it is ignored or checked
(or disabled).
The intention is that this be used for assumptions about the
external environment. So you cannot expect to verify formally
or informally that the condition is met, this must be
established by examining things outside the program itself.
For example, we may have code that depends on the size of
Long_Long_Integer being at least 64. So we could write:
pragma Assume (Long_Long_Integer'Size >= 64);
This assumption cannot be proved from the program itself, but it acts as a useful run-time check that the assumption is met, and documents the need to ensure that it is met by reference to information outside the program.