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. […]