Pragma Refined_State (GNAT Reference Manual)

### 2.156 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.