2.14 Pragma Assume

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.