New RFC for variants on subprograms

[clairedross]

https://github.com/AdaCore/ada-spark-rfcs/blob/11dbbc563665edbe3bbcacbe02f63202a4fdecf4/considered/rfc-subprogram-variant.rst

[clairedross]

https://github.com/AdaCore/ada-spark-rfcs/blob/11dbbc563665edbe3bbcacbe02f63202a4fdecf4/considered/rfc-subprogram-variant.rst

[yannickmoy]

typo: multiple examples contain the typo "Descreases" instead of "Decreases"

[yannickmoy]

The recursive call to F in F's precondition, in the last example, is not checked dynamically for variant decrease. I assume GNATprove would still check that the variant decreases here?

[clairedross]

The recursive call to F in F's precondition, in the last example, is not checked dynamically for variant decrease. I assume GNATprove would still check that the variant decreases here?

Yes. We coudl also check it dynamically I suppose, but it seemed complicated to me as precondition is supposed to be checked at call site.

[raph-amiard]

The feature seems fine, I do however have a problem with the name of the aspect, Variant, since Variant is already a term used in the RM for variant parts, and, as a shortcut, variant records.

What about Progresses, or Function_Variant?

[clairedross]

Le 05/11/2019 à 17:27, Raphaël AMIARD a écrit :

The feature seems fine, I do however have a problem with the name of the aspect, |Variant|, since Variant is already a term used in the RM for variant parts, and, as a shortcut, variant records.

What about |Progresses|, or |Function_Variant|?

Function_Variant would be fine with me, but Progresses is too far from the current Loop_Variant pagma IMO.

-- Claire

[yannickmoy]

Function_Variant will not work for procedures. Why not the proposal of Bob Duff: Call_Variant?

[clairedross]

Function_Variant will not work for procedures. Why not the proposal of Bob Duff: Call_Variant?

Or Subprogram_Variant?