Using a cloned object as if it were newly instantiated - verifier complaining about 'modifies' clause

Apr 27, 2013 at 9:21 PM

I have a question, if anybody has a minute.

The Spec# tutorial introduces at some point a Rectangle class. This class has a Clone() method.
  public Rectangle Clone()
    Rectangle res = new Rectangle();
    res.X = X;
    res.Y = Y;
    res.Dx = Dx;
    res.Dy = Dy;
    return res;
Now, I am trying to do this:
// Somewhere in the code
    static void foo() {
        Rectangle rect = new Rectangle();
        rect.MoveToOrigin(); // no problems here
        Rectangle rect2 = rect.Clone();
        rect2.MoveToOrigin(); // the verifier complains here!
The verifier's warning is this: method invocation may violate the modifies clause of the enclosing method

Now, I think this happens because the verifier doesn't know that the rectangle returned by clone is a new, fresh clone created on the spot and to which the previous rectangle doesn't hold any reference.

My intuition is that there must be some tag/attribute/whatever that I should add to the Clone() method which basically promises this, but I don't know how and I can't find any documentation about this. The Spec# tutorial doesn't seem to mention that. I tried [Fresh], ensures Owner.None(result) and other stuff with no luck.

Any hints?

Thank you
Apr 30, 2013 at 4:25 AM

Your reasoning is correct. All you need to add to your Clone method is
ensures result.IsNew;
May 1, 2013 at 9:05 PM

As expected, it worked. Thank you very much!