Why Can't My Loop Modify Objects Allocated in the Same Method?

[nwad123]

Hello!

I'm running into an issue with correctly specifying a modifies clause for a program that create a sequence of objects and then modifies those object. To preface this, I have found a work-around by refactoring my code, but I'm curious if there is a way to fix the issue without refactoring my code and instead providing Dafny more information.

Related Posts

Discussion 2164: relates to modifies clauses for loops and methods, but does not cover my specific warning.
Zulip discussion: ✔ Modifies on loop that mutates object through a method @ 💬: relates to the specific warning I get, but covers an array of objects instead of a sequence of objects. Covers the specific warning that I get and provides a solution (see below for implementation).

Detailed Problem Description

I created the following program that represents a small example of what I'm trying to accomplish. I have a object type, Counter, that contains a increment-able natural number. I want to create a sequence of Counter objects then increment each counter in another loop.

class Counter {
  var x: nat
  constructor() { x := 0; }

  method inc()
    modifies this`x
    ensures old(x) + 1 == x
  {
    x := x + 1;
  }
}

// Impl0 does not verify
method Impl0()
{
  var counters: seq<Counter> := [];

  for i := 0 to 10
  {
    var c := new Counter();
    counters := counters + [c];
  }

  var n := 0;
  while n < 10
    modifies counters[..]
  {
    for i := 0 to |counters|
    {
      counters[i].inc();
    }
    n := n + 1;
  }
}

// Impl1 verifies just fine
// In this method I have refactored out the creation of the
// sequence of counters.
method Impl1(counters: seq<Counter>)
  modifies counters[..]
{
  var n := 0;
  while n < 10
    modifies counters[..]
  {
    for i := 0 to |counters|
    {
      counters[i].inc();
    }
    n := n + 1;
  }
}

The method Impl0 represents my original implementation and fails to verify. In Impl0 I first create the sequence of counter objects, then in a separate loop I increment the counters. I use modifies b[..] in the second loop to indicate to Dafny that each counter will be modified. My understanding (from 2164) is that because each Counter was created in Impl0 it can be modified in Impl0. However, that does not appear to be the case.

This is the specific error message:

$ dafny verify tmp.dfy
tmp.dfy(25,2): Error: loop modifies clause might violate context's modifies clause
   |
25 |   while n < 10
   |

The method Impl1 represents my refactoring of the problem. In this case I've imagined that another method is in charge of producing the sequence of counters, and Impl1 is only responsible for incrementing them. This method verifies without any issues.

I'd like to understand why Impl1 verifies and Impl0 does not, and (if possible) what can be done to provide Dafny enough information such that Impl0 verifies.

Thank you! Have a great day.

• Nick

---

Disclaimer

The presented program is a silly program that doesn't appear to accomplish anything useful, but my actual program is full of large objects and lots of additional logic so I tried to create a pared down version that contains the same behavior.

Dafny Information

I ran my example on MacOS Tahoe 26.1 with Dafny version 4.11.0 and Z3 4.15.4 (64-bit)

[nwad123]

Well, apparently I should have read this Zulip thread that I linked in my related posts section more carefully, because it actually contained the solution.

Solution

When allocating each object in counters I need to remind Dafny that it's a freshly allocated object--i.e., each Counter was freshly allocated inside of the Impl method. Here is version of my problem that verifies correctly:

method Impl2()
{
  var counters: seq<Counter> := [];

  for i := 0 to 10
    invariant |counters| == i
    // Inform Dafny that each Counter is freshly allocated
    invariant forall j | 0 <= j < i :: fresh(counters[j])
  {
    var c := new Counter();
    counters := counters + [c];
  }

  // This assertion is just there for demonstration, and is not necessary for verification
  assert forall j | j in counters :: fresh(j);

  var n := 0;
  while n < 10
    modifies counters[..]
  {
    for i := 0 to |counters|
    {
      counters[i].inc();
    }
    n := n + 1;
  }
}

---

Bonus Content

In my original example I was just modifying a natural number in each Counter instance, but for my use case I actually needed to modify a reference member of a class. This turned out to be a bit more work, so I thought I'd include my solution here to provide a possible solution for those who were confused like me.

In the example below I've created an additional class, Counters, with two Counter object references in it. These Counter objects are allocated in the Counters constructor, and there is a method (unimplemented) that modifies c0. I want to be able to modify the c0 object of each Counters object in the same way that I have done with the natural number of Counter in my previous solution. My previous solution is not strong enough to inform Dafny that I can modify c0 in the second loop, and I would get a similar verification failure where calling seqOfCounters[j].mod(). To resolve this issue I had to

1. Introduce a postcondition to the Counters constructor that indicated that c0 and c1 are both freshly allocated objects,
2. Add an invariant to my first loop that indicates that c0 (the variable of interest in the mod method) is also freshly allocated, and
3. Let Dafny know that the second loop would modify field c0 of each Counters object in the seqOfCounters sequence.

To accomplish step 3. I used a set comprehension (I think that's the name), which I'm not sure if that is the best way but it was the way that worked for me.

class Counter {
  var x: nat
  constructor() { x := 0; }

  method inc()
    modifies this`x
    ensures old(x) + 1 == x
  {
    x := x + 1;
  }
}

class Counters {
  // Marking these as const indicates that they are allocated once
  // once in the constructor, but then are not allocated again. The
  // const modifier only applies to the reference (in my understanding)
  // and not the variables inside each Counter object
  const c0: Counter
  const c1: Counter

  constructor()
    // Provide information that each Counters object freshly
    // constructs c0 and c1
    ensures fresh(c0) && fresh(c1)
  { 
    c0 := new Counter();
    c1 := new Counter();
  }

  method mod()
    modifies this.c0
}

method Impl()
{
  var seqOfCounters: seq<Counters> := [];

  for i := 0 to 10
    invariant |seqOfCounters| == i 
    // Update invariant to also include fresh(c0)
    invariant forall j | 0 <= j < i :: fresh(seqOfCounters[j]) && fresh(seqOfCounters[j].c0)
  {
    var c := new Counters();
    seqOfCounters := seqOfCounters + [c];
  }

  for i := 0 to 10
    modifies seqOfCounters[..]
    // Indicate that the set of `c0` objects in each `Counters` object are modified
    modifies (set x | x in seqOfCounters :: x.c0)
  {
    for j := 0 to |seqOfCounters|
    {
      seqOfCounters[j].mod();
    }
  }
}