Pragma Refined_State (GNAT Reference Manual)

Next: Pragma Relative_Deadline, Previous: Pragma Refined_Post, Up: Implementation Defined Pragmas [Contents][Index]

2.151 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.