Syntax:
pragma Subprogram_Variant (SUBPROGRAM_VARIANT_LIST); SUBPROGRAM_VARIANT_LIST ::= STRUCTURAL_SUBPROGRAM_VARIANT_ITEM | NUMERIC_SUBPROGRAM_VARIANT_ITEMS NUMERIC_SUBPROGRAM_VARIANT_ITEMS ::= NUMERIC_SUBPROGRAM_VARIANT_ITEM {, NUMERIC_SUBPROGRAM_VARIANT_ITEM} NUMERIC_SUBPROGRAM_VARIANT_ITEM ::= CHANGE_DIRECTION => EXPRESSION STRUCTURAL_SUBPROGRAM_VARIANT_ITEM ::= STRUCTURAL => EXPRESSION CHANGE_DIRECTION ::= Increases | Decreases
The Subprogram_Variant
pragma is intended to be an exact replacement for
the implementation-defined Subprogram_Variant
aspect, and shares its
restrictions and semantics.
This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section 11.4.2.