Next: , Previous: Pragma Abort_Defer, Up: Implementation Defined Pragmas


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.