What is the proper annotation for ranges in function contracts

[feliperodri]

CBMC version: 5.26.0
Operating system: macOS Mojave
Exact command line resulting in the issue: N/A.
What behaviour did you expect: N/A.
What happened instead: N/A.

Currently, we support the specification of array ranges in code contracts using the syntax [lower .. upper]. However, this requires changes in the parser. @hannes-steffenhagen-diffblue suggested here a different approach:

I'm quite worried about the proliferation of nonstandard extensions. We're getting into a situation where we have to support gcc extensions, clang extensions, visual studio extensions on top of our own modifications to the language...
This could've been done without any parser changes at the relatively small cost of a less cute syntax, e.g. __CPROVER_array_range(array, lower, upper) or something like that. Looks bad, but less problematic syntactically.

Which one should we adopt?

[SaswatPadhi]

I'm just documenting the offline discussion we had.

Hannes' concerns regarding syntax are valid and it's unclear if we need such level of precision within the assigns clause right now. Many languages that do support assigns / modifies clause, e.g. Dafny, Spec# etc. just use the entire array, or a particular index of it in the modifies clause. To my knowledge, only JML supports the range syntax a[lower .. upper].

The consensus is to start with a first implementation of the assigns clause that doesn't introduce any special syntax -- you can only mention a or a[i] in the modifies clause. If need be, we could later bring in the other changes that are proposed in this PR for ranges.

[martin-cs]

If you have existential variables and can introduce them in contracts then that would give you another alternative. We have some support for ACSL which would be another alternative. IMHO trying to use the same syntax for dependencies as assignment LHS could be good.

[SaswatPadhi]

If you have existential variables and can introduce them in contracts then that would give you another alternative.

That's a good point! We do have plans to implement ghost variables, so we could probably leverage those.

[feliperodri]

I'll close this issue for now since none of our applications require such range notation so far. We can always re-open the issue if the discussion come up in the future.