2.86 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.