cpp-forrange.tex

\subsection{for with range statement [C++]}

\lang introduced a new kind of iteration statement: the range-based for statement, illustrated in the code below:
\lstinputlisting{range.cpp}

In each case the value of \lstinline|i| or \lstinline|value| is progressively the respective array or list elements. The  
index for the array or iterator for the list that would be used in other forms of \lstinline|for| statements is implicit here, simplifying and
clarifying the code.

However this form poses a difficulty for reasoning about the
loop. Typically an iteration over the array would be specified as
follows.

\lstinputlisting{loop.cpp}

Note that the loop index, here \lstinline|j|, is needed in the loop invariant to help state the inductive loop invariant. However, there is no explicit loop index in the
for-range syntax. So we define one, named \lstinline|\count|, for specification purposes.
\lstinline|\count| is the number of completed loop iterations so far; 
at the beginning of the initial iteration its value is 0; it 
increments by 1 each time the loop body is started again (including by a
\lstinline|continue| statement).
We also define \lstinline|\data| to refer to the value of the array or list over which the for-loop ranges.

With these constructs, we can specify our two example uses of
for-range as follows.

\lstinputlisting{loop_range.cpp}

In \lang, a for-range loop is just another kind of loop statement, as in Fig. \ref{sec:loop_annot}. Thus the grammar for loop annotations needs no enhancement other than
allowing \lstinline|\count| and \lstinline|\data| as terms, as shown in Fig. \ref{fig:gram:this}.