Next: , Previous: , Up: Implementation Defined Pragmas   [Contents][Index]

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    [=> boolean_EXPRESSION]
  | Async_Writers    [=> boolean_EXPRESSION]
  | Effective_Reads  [=> boolean_EXPRESSION]
  | Effective_Writes [=> boolean_EXPRESSION]
    others            => 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.