Dafny: modifies clause

Oct 8, 2012 at 4:12 PM

I understand what modifies clause means for the following method empty:

class DList
{
  var head : Node;
  
  constructor empty()
    modifies this;
    ensures head == null;
  {
    head := null;
  }
}

It allows to change fields of "this", and method changes "this.head".

But it don't understand what modifies clause means for the following method insert:

class DList
{
  var head : Node;
  
  method insert(x : T)
    modifies this, head;
    ensures fresh(head);
  {
    var h := new Node.create(x);
    h.next := head;
    if (head != null) {
      head.prev := h;      
    }
    head := h;
  }
}
Method "insert" has "modifies this", so it may change fields of "this" amd it changes "this.head" (head := h). But it also can "modifies head", but head is changed in this method. So there are "ore head" and "post head". What "modifies head" means in this case ?

Oct 9, 2012 at 2:50 AM

In the specification of the method insert(x : T), modifies head; is giving the method license to modify the fields of this.head for the initial value of this.head (which you refer to as "pre head"). This is exactly the specification you need for the assignment head.prev := h, which says that a field prev of the initial value of this.head gets value h. The value of this.head is indeed changed in the last statement of the method (which is permitted because of modifies this; specification), and this is your "post head".

In short, "modifies head" means that you have a license to modify the fields of your "pre head".

Hope this helps,

Edgar

Oct 9, 2012 at 7:50 AM

Thank you, Edgar!

 

Eugene