Array may be null or assignment may update...

Apr 19, 2015 at 3:28 AM
datatype ENTRY = PACK(key: int, val:int)
datatype RES = NONE | SOME(int)

class Dictionary
{
var table : array<ENTRY>;   //array to store entries
var elems : int;            // number of entries in dictionary
var tsize : int;            // maximum size of dictionary

function RepInv():bool
    reads this;
{
    table != null && 
    (tsize > 0) &&
    0 <= elems < tsize == table.Length
}


method init(size:int)
    requires size > 0;
    ensures RepInv();
    modifies this;
{
    table := new ENTRY[size];
    elems := 0;
    tsize := size;
}

//returns the index of the key k  on table
method indexOf(k:int) returns (index:int)
    requires RepInv();
    requires k > 0;
    ensures index == -1 ==> forall j :: (0<=j<elems) ==> table[j].key != k; // index é -1 se k nao existe no vetor
    ensures index != -1 ==> ((0<=index<elems) && table[index].key == k); // index entre 0 e n e valor do index igual a V se retorno diferente de -1
{
  var i:int := 0;
  index := -1;

  while(i < elems)
  invariant 0<=i<=elems;
  invariant index == -1 ==> forall j :: (0<=j<i) ==> table[j].key != k;
  invariant index != -1 ==> ((0<index<i) && table[index].key == k);
  {
    if (table[i].key == k) {
        index := i;
      break;
    }
    i := i + 1;
  }
}

//removes any existing association of key k in the dictionary
method delete(k:int)
requires RepInv();
requires k > 0;
modifies table;
{
    var index:int := indexOf(k);

    if(index != -1)
    {           
        while(index < (elems-1))
            invariant 0 <= index <= (elems);
        {
            var elemento:ENTRY := PACK(table[index+1].key, table[index+1].val);
            table[index] := elemento;
            index := index + 1;
        }           
        elems := elems - 1 ;
    }       
}       
}

I have this code and I'm getting the error "Assignment may update an object not in the enclosing..." on the line "elems := elems - 1; "

I understand the error because the modifies clause is only for the table. But if I replace the modifies clause to "modifies this" I get 3 errors:
  • "array may be null" on the line - var elemento:ENTRY := PACK(table[index+1].key, table[index+1].val);
  • "index out of range" on the same line
  • "assignment may update an array element not in the enclosing..." on the line: table[index] := elemento;
Why is dafny complaining?
Apr 20, 2015 at 8:21 AM
I think you need "modifies this, table;" as you are modifying both the table array and a field of the current object.