Help me to understand the concept of "freshness" in Dafny

[rsingha108]

class X {
    var a: int
    var b: int

    constructor() 
    {
        a := 0;
        b := 0;
    }

    method copy() returns (x: X)
        ensures fresh(x)
    {
        x := new X();
        x.a := this.a;
        x.b := this.b;
    }
}

class Element {
    var x: X
    var y: int

    constructor() 
    {
        x := new X();
        y := 0;
    }

    method copy() returns (e: Element)
        ensures fresh(e)    
        ensures fresh(e.x)
    {
        e := new Element();
        e.x := this.x.copy();
        e.y := this.y;
    }
}

class Data {
    var src_seq: seq<Element>
    var dst_seq: seq<Element>
}

method m1(d : Data) modifies d, d.dst_seq[..]

method m2(d: Data) modifies d, d.dst_seq[..]
{
  var i := 0;
  while (i < |d.src_seq|)
    invariant 0 <= i <= |d.src_seq|
    invariant fresh((set o <- d.dst_seq[..]) - old((set o <- d.dst_seq[..])))
    modifies d, d.dst_seq[..]
  { 
    var e := d.src_seq[i].copy();
    d.dst_seq := d.dst_seq + [e];
    i := i + 1;
  }
  d.src_seq:= [];
  m1(d);
}

In the above dafny code, I have a class Data with two sequences, src_seq and dst_seq and the method m2 adds elements from src_seq to dst_seq. When I try to call method m1 within m2 it gives an error call might violate context's modifies clause.

I understand that m1 needs a guarantee that the elements added to dst_seq are fresh. For that I added copy() methods in the classes Element and X. Also added a loop invariant fresh((set o <- d.dst_seq[..]) - old((set o <- d.dst_seq[..]))) to method m2 which mitigates the error.

Is there a better way to mitigate the verification error, without duplicating using copy() methods?

[rsingha108]

Is it possible to not have the call might violate context's modifies clause error without the freshness invariant fresh((set o <- d.dst_seq[..]) - old((set o <- d.dst_seq[..])))? Or is there a different way to ensure the freshness of the new elements added to d.dst_seq from d.sec_seq?