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.