Pragma Refined_Depends (GNAT Reference Manual)

### 2.152 Pragma Refined_Depends ¶

Syntax:

    pragma Refined_Depends (DEPENDENCY_RELATION);

    DEPENDENCY_RELATION ::=
         null
      | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE})

    DEPENDENCY_CLAUSE ::=
        OUTPUT_LIST =>[+] INPUT_LIST
      | NULL_DEPENDENCY_CLAUSE

    NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST

    OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT})

    INPUT_LIST ::= null | INPUT | (INPUT {, INPUT})

    OUTPUT ::= NAME | FUNCTION_RESULT
    INPUT  ::= NAME

    where FUNCTION_RESULT is a function Result attribute_reference

For the semantics of this pragma, see the entry for aspect `Refined_Depends` in the SPARK 2014 Reference Manual, section 6.1.5.