Syntax:
pragma Assertion_Level (LEVEL_IDENTIFIER [, depends => DEPENDENCY_DESCRIPTOR]); DEPENDENCY_DESCRIPTOR ::= LEVEL_IDENTIFIER | LEVEL_IDENTIFIER_LIST LEVEL_IDENTIFIER_LIST ::= '[' LEVEL_IDENTIFIER {, LEVEL_IDENTIFIER} ']'
For the semantics of this pragma, see the SPARK 2014 Reference Manual, section 11.4.3.