Pragma Refined_State - GNAT Reference Manual

Next: Pragma Relative_Deadline, Previous: Pragma Refined_Post, Up: Implementation Defined Pragmas

2.146 Pragma Refined_State

Syntax:

    pragma Refined_State (REFINEMENT_LIST);
    
    REFINEMENT_LIST ::=
      (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
    
    REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST
    
    CONSTITUENT_LIST ::=
         null
      |  CONSTITUENT
      | (CONSTITUENT {, CONSTITUENT})
    
    CONSTITUENT ::= object_NAME | state_NAME

For the semantics of this pragma, see the entry for aspect Refined_State in the SPARK 2014 Reference Manual, section 7.2.2.