\count and \index

[davidcok]

At the Shohan JML Workshop, \count was added to JML in preference to \index as a builtin expression for the (inner-most) loop counter. This variable is necessary for the foreach style loop and is handy for others (although a ghost variable could be used). The name change (\index was quite recent) reflects that the variable is actually the number of times the loop body has been executed, not the value of the loop index, though sometimes those are the same.

This issue asks a) that we want to keep \count b) whether we keep \index as well or deprecate it

I advocate Yes on (a) and am mostly neutral on (b). I'd rather deprecate \index to keep the language smaller, but I recognize there are existing uses, so the deprecation can be slow -- or we can keep both names.

[dmzimmerman]

I'd think it makes sense to keep \count, and as \index is potentially confusing because it isn't really the value of the loop index, deprecating that seems like a good idea - though I don't have any sense for how widely \index is actually used in practice.

[mattulbrich]

KeY has implemented \index. Yet, it seems to be rarely (if at all) used in our example and case studies. I do not have a preference regarding the keyword. But I would refrain from having 2 keywords. So, (a) it is for me.

(We would probably keep \index for a while with a deprecation warning and remove it eventually.)

[mattulbrich]

Consensus Candidate: Rename \index to \count and deprecate \index, to be removed eventually.

[leavens]

I agree with that change: use \count instead of \index.

[davidcok]

All agreed.