Pragma Abstract_State (GNAT Reference Manual) (original) (raw)

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.