In CAST, the an example of a loop statement in the meta-language might look like:
<i:N:
inv z[i];
x[i] = y[i];
>
The equivalent in HAC would look like:
(;i:N:
inv z[i..i];
x[i] = y[i];
)
The main difference is the use of parentheses instead of angle brackets and an extra semicolon operator. Notice that the declaration of z in the loop uses an explicit range to declare each sparse instance in the collection (Arrays). (It is highly recommended to keep declarations outside of loops where possible, leaving only connection statements inside loops.)
Like in CAST, loops may be nested arbitrarily deep and may be nested with conditional bodies.