I am trying to solve a resize of array using Dafny

Question

I am traying to solve an issue with DAFNY with resizing array. below is the code which is giving me an error and cannot figure out what the problem is. Any help is appreciated.

This is the full code I have, it is always giving me an error when checking.

Code:

// class CircularMemory
// This class implements a cicular buffer with with 2 int typed pointers
class CircularMemory
{
  var cells : array<int>
  var read_position : int
  var write_position : int

  constructor Init(cap : int)
    requires cap > 0
    ensures  Valid()
    ensures  fresh(cells)
  {
    cells := new int[cap];
    read_position, write_position := 0, 0;
  }

  // Valid is the class invariant we would like to maintain
  // for any CircularMemory at any moment of its lifetime
  predicate Valid()
    reads this, cells
  {
    cells != null && // cells is valid data

    // write and read pointers are within valid bounds
    0 <= write_position < cells.Length &&
    0 <= read_position < cells.Length
  }

  // A predicate indicating no more Read available
  predicate isEmpty()
    reads this
  {
    // If both the read and write pointers are at the same element it means that the buffer is empty
    read_position == write_position
  }

  // A predicate indicating no more Write should be allowed
  predicate isFull()
    reads this
    requires cells.Length > 0
  {
    // If when we attempt to increment the write pointer by 1, we get a pointer to the same element the
    // read pointer points to then we can consider the buffer full
    (write_position + 1) % cells.Length == read_position
  }

  method Read() returns (isSuccess : bool, content : int)
    modifies this, cells
    requires Valid()
    requires 0 <= read_position < cells.Length
    ensures  Valid()
    // on success, make sure the buffer is not full (we popped an element after reading successfully)
    //    and that the old content did not change
    //    and that the read pointer has been advanced by one cell
    ensures  isSuccess ==> !isFull() && content == old(cells[read_position]) &&
                            read_position != old(read_position)
    // on failure, make sure the buffer is empty (only failure case) and that we return the dummy value
    ensures !isSuccess ==> isEmpty() && content == 0
  {
    
    // Fail if the circular buffer is empty
    if (isEmpty() == true) {
      content:= 0;
      isSuccess := false;
    } else {
      // Read from buffer using the current read position
      content := cells[read_position];
      // Advance read pointer by 1 cell, and wrap around
      read_position := (read_position + 1) % cells.Length;
      isSuccess := true;
    }
  }

  method Write(input : int) returns (isSuccess : bool)
    modifies this, cells
    requires Valid()
    ensures  Valid()
    // Ensure we aren't empty and that the write pointer has advanced by one cell
    ensures  isSuccess ==> !isEmpty() && write_position != old(write_position)
  {

    if (isFull() == false) {
      // Write to the cell
      cells[write_position] := input;
      // Advance the write pointer by 1, and wrap around
      write_position := (write_position + 1) % cells.Length;
      isSuccess := true;
    } else {
      isSuccess := false;
    }
  }

    // Question 3 for Lab 4
  method DoubleCapacity()
    modifies this`cells
    requires Valid()
    ensures Valid()
    ensures cells.Length == 2 * old(cells.Length)
    ensures read_position == old(read_position)
    ensures write_position == old(write_position)
    ensures forall j : int :: 0 <= j < old(cells.Length) ==> cells[j] == old(cells[j]) // doesnt work
    ensures forall j : int :: old(cells.Length) <= j < cells.Length ==> cells[j] == 0
  {
    // one or more loops to double the capacity of cells
    // the most important part is the loop invariants!
    var oldCap := cells.Length;
    var newCap := 2 * oldCap;
    var newCells := new int[newCap];
    var i := 0;
    
    // Copy existing elements to the new array
    while (i < oldCap)
        invariant 0 <= i <= oldCap <= cells.Length < newCells.Length
        invariant forall j :: 0 <= j < i ==> newCells[j] == cells[j]
        decreases oldCap - i

        
        invariant 0 <= i <= oldCap <= cells.Length < newCells.Length
    {
        newCells[i] := cells[i];
        i := i + 1;
    }
    // fails already ???
    assert forall j : int :: 0 <= j < cells.Length < newCells.Length ==> newCells[j] == cells[j];

    // Initialize the remaining elements to 0
    while (i < newCap)
        invariant 0 <= oldCap <= i <= newCap
        invariant forall j :: 0 <= j < oldCap < cells.Length ==> newCells[j] == cells[j]
        invariant forall j :: oldCap <= j < i ==> newCells[j] == 0
        decreases newCap - i
    {
        newCells[i] := 0;
        i := i + 1;
    }
    // fails again ???
    assert forall j : int :: 0 <= j < cells.Length < newCells.Length ==> newCells[j] == cells[j];

    cells := newCells;
  }
}

I tried to find the error but cannot find how to solve it

Answer 1

The main problem is that, while your loop invariants talk about some elements of newCells, they are silent about the elements of cells and the elements assigned to newCells in the first loop. In general, when a loop body makes any update in the heap, then your loop invariant needs to talk about all parts of the heap that you care about. More precisely, if the loop body can modify the heap, then the verifier treats the whole loop as if it could modify whatever the enclosing modifies clause says. (An example that discusses this point is found in section 14.1.2 of my book, Program Proofs. If you have the book, I recommend reading that section.)

To remedy the situation, you need to say that the array referenced by this.cells and the elements of that array are invariant under both loops. For example, you might say

invariant cells == old(cells)
invariant forall j :: 0 <= j < cells.Length ==> cells[j] == old(cells[j])

In other situations, you may need to know that additional fields of this are unchanged, in which case you can use the unchanged predicate in Dafny (see also this Dafny Power User note). In fact, for your example, you can write my two loop invariants above with just

invariant unchanged(this) && unchanged(cells)

And yet one other way to accomplish this is to declare directly what each loop modifies. That's the most straightforward way to do it (but may or may not be allowed by your assignment, which apparently is to write loop invariants). You do this by adding a modifies clause to each loop:

modifies newCells

It rare that loops have modifies clauses, but this is one situation where it makes for a good description of the loop does.

Okay, from what I have said so far, your loops need to say more about what is not changed. However, this is not the only problem in your attempted program. Another problem is your invariant

invariant forall j :: 0 <= j < oldCap < cells.Length ==> newCells[j] == cells[j]

Since oldCap == cells.Length, the antecedent oldCap < cells.Length is false, so this loop invariant is useless. It is usually not a good idea to constrain variables other than the bound variable (here, j) in the antecedent of a quantified expression (forall). If you fix this, then your program verifies.

Others readers (who are not constrained by the instructions of your assignment) may also be interested in the following. First, you can omit these decreases clauses from the program text, because Dafny will correctly guess them from the while condition. Second, instead of using while loops, you can use Dafny's for loops. Then, you don't need decreases clauses at all, and the range condition on the loop-index variable is also taken care of automatically by Dafny. Third, the easiest way to implement method DoubleCapacity is to not use any loops at all! Dafny provides some loop-less constructs for accomplishing things like copying and initialization (see, for example, section 14.1.4 of Program Proofs).