Syntax:
pragma 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 Depends
in the
SPARK 2014 Reference Manual, section 6.1.5.