I am working on a Dafny project where instances of a class can modify the fields of other objects stored in lists within that class.

In many cases, methods only change a specific attribute of these objects. I would like to know how to specify which attribute is changed in the modifies clause. Is there a way to do this in Dafny?

Here is a simple example

`  class A {
    var x : int 
    var y : int

  }

  class B 
  {
    const l : seq<A>

    method m()
        modifies l
        // I would like to write e.g. modifies (set x`a | a in l)
        ensures forall a :: a in l ==> a.x == 10
        // the following postcondition should be subsumed by the modifies clause
        ensures forall a :: a in l ==>  unchanged(a`y)
    {
       var it := 0;
       while it < |l|
        // here, I would like to write l[it]`x for example
            invariant 0 <= it <= |l|
            invariant forall a :: a in l[..it] ==> a.x == 10
            invariant forall a :: a in l ==> unchanged(a`y)
        {
            l[it].x := 10;
            it := it + 1;
        }
    }
  }`