Dafny: Updating an array of objects

[rsingha108]

class element {
    var x : int
    var y : int

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

    constructor from_elem(e: element)  // to deepcopy an element
    {
      x := e.x;
      y := e.y;
    }

    method update_x(val: int) modifies this
    {
      this.x := val;
    }

}

class A  {
    var arr : array<element>
    constructor() 
    {
      var empty := new element();
      arr := new element[5](i => empty); // initialised to empty array
    }
}

method update_arr(a: A) modifies a, a.arr
requires a.arr.Length > 0
{
  var i := 0;
  while (i <= a.arr.Length - 1) modifies a, a.arr
    invariant 0 <= i <= a.arr.Length
    invariant old(a.arr) == a.arr
  {
    // update in place
    a.arr[i].update_x(10);

    // create a copy of the element and update the x value
    var e := new element.from_elem(a.arr[i]);
    e.update_x(10);
    a.arr[i] := e;

    i := i + 1;
  }
}

The method update_arr tries to update the field x of an array of objects of class A. If I want to update the i-th element of the array in place by a.arr[i].update_x(10), the verifier gives error. But if I create a copy of the object and then update the value of x, then it is verified. What can I do to get it verified without creating any copies?

[MikaelMayer]

modifies a, a.arr means you can modify

1. modifies a: The fields of the object a and assign them different values (for example, replace arr with another array)
2. modifies a.arr: The elements of the initial array at a.arr by assigning a.arr[i] = ... for example.

It looks like what you are trying to modify are the elements of the array themselves, not the array itself.
In Dafny, to convert an array (which is considered as an object where fields are integers) to a sequence of its elements that it suitable in a modifies clause, you'd write

modifies a.arr[..].

And you can now omit modifies a.arr if you don't have the intention to reorder the elements.

Note that if you omit a.arr in the modifies clause, suddenly the assignment that was working a.arr[i] := e; does not work anymore! But now you should know why and re-add modifies a.arr if you want it. That would still not be sufficient as the first update_x might now fail.
Indeed, if Dafny determines that elements of the array were replaced, how to ensure that you still have permission to update them in the loop?

The final answer to that is to ensure that all the elements you added were not allocated at the beginning of the method, so it's perfectly valid to modify them. It has to be captured in an invariant, which looks like this:

    invariant fresh((set o <- a.arr[..]) - old((set o <- a.arr[..])))

Explanation: fresh(a) means allocated(a) && !old(allocated(a)) as said. But we only consider the set of elements that are in the array now and that were not part of the original array. Dafny can prove that invariant and that is sufficient to get your green gutter icons (if you are using VSCode)

[rsingha108]

Thanks a lot. That was really helpful. But I want to understand it in more depth. Here's a similar situation:

class elem{
    var x : int
    var y : int
    constructor()
    {
        x := 0;
        y := 0;
    }
}

class P {
    var list: seq<elem>
    constructor()
    ensures fresh(list)
    {
        list := [];
    }
}

method main()
{
    var p := new P();
    update1(p);
    update2(p); // gives error: call might violate context's modifies clause
}

method update1(p : P) modifies p
ensures fresh((set o <- p.list[..]) - old((set o <- p.list[..]))) // this mitigates the error
{
    var e := new elem();
    p.list := p.list + [e];
}

method update2(p : P) modifies p, p.list[..]
{}

If I omit the ensure condition, update2(p) gives verification error. I don't fully understand the ensure condition yet. But I gave it a try as you mentioned and it worked. Can you explain me what is happening here, why it is giving error without the ensures fresh((set o <- p.list[..]) - old((set o <- p.list[..]))) and why adding it solves the error?

[MikaelMayer]

That's again a good question to ask. Let's look at the error message first if you comment the ensures clause.

"Error: call might violate context's modifies clause"

This means the method does not have the permissions to modify the fields update2 states it declares.
Methods have the permission to modify either

1. Objects that appear in their own modifies clauses
2. Object that were created since the method started to execute. Since Dafny is a sequential language, objects created since the method started were not accessible at call site so no specification could be made about them, so that's why we can modify them even if they are not explicitly in the modifies clause.

Now let's look at update2's modifies clause. It contains p, but because p was not allocated at the beginning of the method (you can add assert !old(allocated(p)) before update2()), Dafny is not complaining about modifies p..
Let's look at the second modifies clause: p.list[..]. By the way, you don't need the [..] here as it's a no-op for sequences if no start or end boundary is given. It's only useful to convert an array to the sequence, so that we can talk about all the objects it contains rather than the object array itself.
So the second modifies clause is modifies p.list.
Again, since the enclosing method declares an empty modifies clause (1) cannot be satisfied, so it has to be (2). We need to prove that
assert !old(allocated(p.list)). If you add this assertion before update2(), you'll see that the error moves from the call update(2) to this assertion, which indicates that we have an assertion that implies what Dafny could not prove, which is a good sign usually.
Here, it's a bit more tricky, because p itself was not allocated, so the assertion is really:
assert (var list := p.list; !old(allocated(list))), but for some reason it does not work (@RustanLeino do you know why?)
so the assertion you want is
assert fresh(p.list);

Now, the value p.list could have been modified by update1, as update1 declares all the fields of p. Hence, without any ensures clause about p.list in update1, the list could be anything, including objects that were created before the call to main(), that one would not have the right to modify. If we only used pure Dafny code, we could theoretically run a whole-program analysis to detect that since main() started without argument, any object in p.list must have not been allocated at the beginning of main(). However, Dafny does not do such whole-program analysis, and it's perfectly possible to axiomatize methods that will return objects that could have been allocated outside of main, and before main() (think of a handler).

Since we now need to prove fresh(p.list) between update1() and update2(), the only thing we can do now is to add a postcondition to update1().
Adding ensures fresh(p.list) as a postcondition to method update1 is not what we want. Indeed, now fresh is local as it would mean that all the objects of p.list were not allocated at the beginning of update1, which is not the case, so that ensures would not be provable.
What we actually need to prove is that all the added objects to p.list are fresh in the method. If they are fresh in update1, then after update1 they are also fresh in main(), because they were not allocated.

Looking at update1, the only object that is fresh is the last one. Hence, stating that all objects remain the same except the last one and that the last one is fresh is sufficient for your needs:

method update1(p : P) modifies p
  ensures |p.list| > 0
  ensures p.list == old(p.list) + [p.list[|p.list|-1]]
  ensures fresh(p.list[|p.list|-1])

This is a very precise postcondition that is sufficient for our needs. You can even formulate the last one differently, with ensures var pList := p.list; !old(allocated(pList[|pList|-1])), which is sufficient because Dafny knows that all the objects of p.list are allocated at the end of update1.

Your postcondition states something more general that the postcondition above implies. Let me break it down:

ensures fresh((set o <- p.list) - old((set o <- p.list)))
              ^^^^^^^^^^^^^^^^ = All the objects in p.list after the call to update1
                                  ^^^^^^^^^^^^^^^^^^^^^^^All the objects in p.list before the call to udpate1
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ == {p.list[|p.list|-1]}

So I hope you see why this one is the most general one that Dafny requires to be happy.