from i := 0 n := 10 invariant n until i >= 10 loop i := i + 1 variant n-i end
across list_of_customers as customer loop Io.put_string (customer.item.name) Io.new_line end across 1 |..| 5 as it loop Io.put_integer (it.item) Io.new_line end