`modifies` clauses in Dafny

recursiveRepr.dfy

class A {
    var n: nat
    ghost var Repr: set<object>
    predicate Valid()
        reads this, Repr
    {
        this in Repr &&
        n % 2 == 0
    }
    constructor()
        ensures Valid()
        ensures fresh(Repr - {this})
    {
        this.n := 0;
        this.Repr := {this};
    }
    method update()
        requires Valid()
        modifies this
        ensures Valid()
        ensures Repr == old(Repr)
        // more general: ensures fresh(Repr - old(Repr))
    {
        this.n := this.n + 2;
    }
}

class B {
    var a1: A
    var a2: A
    ghost var Repr: set<object>
    predicate Valid()
        reads this, Repr
    {
        this in Repr && a1 in Repr && a2 in Repr && a1.Repr <= Repr && a2.Repr <= Repr &&
        this !in a1.Repr && this !in a2.Repr &&
        //a1.Repr !! a2.Repr && // <-- needed?
        a1.Valid() && a2.Valid()
    }
    constructor(a1: A, a2: A) 
        requires a1.Valid() && a2.Valid()
        ensures Valid()
        ensures fresh(Repr - {this} - a1.Repr - a2.Repr)
    {
        this.a1 := a1;
        this.a2 := a2;
        this.Repr := {this} + a1.Repr + a2.Repr;
    }
    method update() 
        requires Valid()
        modifies Repr
        ensures Valid() 
        ensures Repr == old(Repr)
        // more general: ensures fresh(Repr - old(Repr))
    {
        this.a1.update();
        this.a2.update();
    }
}

class C {
    var bs: seq<B>
    ghost var Repr: set<object>
    predicate Valid()
        reads this, Repr
    {
        this in Repr && 
        (forall i :: 0 <= i < |bs| ==> 
            bs[i] in Repr && bs[i].Repr <= Repr && this !in bs[i].Repr && bs[i].Valid()) &&
        (forall i, j :: 0 <= i < j < |bs| ==>
            bs[i] in Repr && bs[j] in Repr &&
            bs[i].Repr !! bs[j].Repr)
    }
    method update()
        requires Valid()
        modifies Repr
        ensures Valid()
        ensures Repr == old(Repr)
        // more general: ensures fresh(Repr - old(Repr))
    {
        var i := 0;
        while (i < |bs|) 
            invariant Valid()
            invariant 0 <= i <= |bs|
            invariant Repr == old(Repr) // <-- without this, bs[i].update() might violate context's modifes clause
            decreases |bs| - i
        {
            bs[i].update();
            i := i + 1;
        }
    }
}