Pragma Abstract_State (GNAT Reference Manual)

### 2.2 Pragma Abstract_State ¶

Syntax:

    pragma Abstract_State (ABSTRACT_STATE_LIST);

    ABSTRACT_STATE_LIST ::=
         null
      |  STATE_NAME_WITH_OPTIONS
      | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} )

    STATE_NAME_WITH_OPTIONS ::=
         STATE_NAME
      | (STATE_NAME with OPTION_LIST)

    OPTION_LIST ::= OPTION {, OPTION}

    OPTION ::=
        SIMPLE_OPTION
      | NAME_VALUE_OPTION

    SIMPLE_OPTION ::= Ghost | Synchronous

    NAME_VALUE_OPTION ::=
        Part_Of => ABSTRACT_STATE
      | External [=> EXTERNAL_PROPERTY_LIST]

    EXTERNAL_PROPERTY_LIST ::=
         EXTERNAL_PROPERTY
      | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )

    EXTERNAL_PROPERTY ::=
        Async_Readers    [=> static_boolean_EXPRESSION]
      | Async_Writers    [=> static_boolean_EXPRESSION]
      | Effective_Reads  [=> static_boolean_EXPRESSION]
      | Effective_Writes [=> static_boolean_EXPRESSION]
        others            => static_boolean_EXPRESSION

    STATE_NAME ::= defining_identifier

    ABSTRACT_STATE ::= name

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