Pragma Subprogram_Variant (GNAT Reference Manual) (original) (raw)

2.176 Pragma Subprogram_Variant ¶

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.