How do I iterate over the elements of a finite set object in Dafny?

Question

What is the best way to iterate over the elements of a finite set object in Dafny? An example of working code would be delightful.

Answer 1

This answer explains how to do it using a while loop, rather than by defining an iterator. The trick is to use the "assign such that" operator, :|, to obtain a value y such that that y is in the set, and then repeat on that set with the y removing, continuing until there are not more elements. The decreases clause is necessary here. With it, Dafny proves termination of the while loop, but without it, not.

method Main()
{
    var x: set<int> := {1, 2, 3};
    var c := x;
    while ( c != {} )
        decreases c;
    {
        var y :| y in c;
        print y, ", ";
        c := c - { y };
    }
}