For loop specification needs total rewrite

Section `\ref{forLoop}` in the language specification needs to be completely rewritten: It specifies a highly incomplete set of static analysis rules, and it only specifies the dynamic semantics for one form of the statement (in particular, it does not cover the case where the iteration variable has a declared type).

Furthermore, it uses a very unusual approach to specify that there is a fresh iteration variable for each iteration of the loop, involving substitutions of variable names on the entire body of the loop, at run time.

It may work better to specify this kind of for loop in terms of a desugaring step where the fresh variable for each iteration is achieved by introducing regular local variable declaration in a nested block, and relying on the standard semantics of such declarations.