Iterating over sequences and sets in Dafny

iteration.dfy

method sum_seq(xs: seq<int>) returns (z:int) {
    var sum := 0;
    var i := 0;
    while i < |xs|
        invariant i <= |xs|
    {
        sum := sum + xs[i];
        i := i + 1;
    }
    return sum;
}

// inspired by https://stackoverflow.com/q/48739486
method sum_set(xs: set<int>) returns (z:int) {
    var sum := 0;
    var c := xs;
    while c != {}
    decreases c
    invariant c <= xs;
    {
        var x :| x in c;
        sum := sum + x;
        c := c - {x};
    }
    return sum;
}