Pragma Initializes (GNAT Reference Manual)

### 2.88 Pragma Initializes ¶

Syntax:

    pragma Initializes (INITIALIZATION_LIST);

    INITIALIZATION_LIST ::=
         null
      | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})

    INITIALIZATION_ITEM ::= name [=> INPUT_LIST]

    INPUT_LIST ::=
         null
      |  INPUT
      | (INPUT {, INPUT})

    INPUT ::= name

For the semantics of this pragma, see the entry for aspect `Initializes` in the SPARK 2014 Reference Manual, section 7.1.5.