Finally, in the upcoming release of Whiley, I have added support for both `while`

and `for`

loops — which is about time. Here’s an example:

define nat as int where $ >= 0 nat sum([nat] list): r=0 i=0 while i < |list| where r >= 0: r = r + list[i] i = i + 1 return r

This code sums a list of [[natural number|natural numbers]] which, of course, produces a natural number. It illustrates a few points: firstly, the syntax for `while`

loops is as expected; secondly, `while`

loops may be given [[loop invariant|loop invariants]] (i.e. the `where`

clause).

We can rewrite this example using a `for`

loop as follows:

define nat as int where $ >= 0 nat sum([nat] list): r=0 for l in list where r >= 0: r = r + l return r

This does what you’d expect and serves to illustrate that loop invariants can be given to `for`

loops as well.

[…] Whiley has regained the while loop and also a for loop. You can read more about that here. […]