Whiley gets a While Loop!
Finally, in the upcoming release of Whiley, I have added support for both
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 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 invariants (i.e. the
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.