Pragma Assume (GNAT Reference Manual)

### 2.18 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.

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.