0. The essence

In a nutshell, the expression old(E) denotes the value of expression E evaluated in the pre-state of the enclosing method. The expression unchanged(R) says that the values of the fields of the object denoted by expression R are the same as in the pre-state.

For instance, consider the following classes, which I will use throughout this note:

class C {
  var x: int
  var y: D
  // ...
}
class D {
  var z: int
}

If c is a parameter of type C, then the expression unchanged(c)means

old(c.x) == c.x && old(c.y) == c.y

But there's more, if you want to know it.

1. modifies

Let's review modifies clauses on methods.

A method must declare the set of (previously allocated) objects whose fields it might modify. So, if a method method M(c: C) wants to do an assignment like

c.x := 10;

or

c.x := c.x + 2;

then its specification must include the object reference c in its modifies clause, like so:

method M(c: C)
  modifies c

This specification gives M permission to modify the fields of c.

method M(c: C, d: D)
  modifies c.y

c.y.z := 15;

c.y := d;  // error: not allowed by modifies clause 

A modifies clause is not transitive. That is, modifies c gives permission to modify the fields of c, but not their fields. In particular, the assignment

c.y.z := 20;

is not allowed by the specification modifies c.

Methods are always allowed to allocate new objects and modify their fields, even without any mention in the modifies clause. So, here's a way to ensure that c.y.z has a post-value of 20:

method M(c: C)
  modifies c
  ensures c.y.z == 20
{
  c.y := new D;  // allowed because c is in the modifies clause
  c.y.z := 20;   // allowed because c.y is newly allocated
}

Note that this program swap out c.y for a new object. The object previously referenced by c.y is not changed by method M.

2. Frame expressions

What follows the modifies keyword is a list of frame expressions. A frame expression denotes a set of objects (or arrays).

For convenience, a frame expression can be given as a set of object or as a single object. The latter is shorthand for the singleton set containing that object. The modifies clause denotes the set union of the objects denoted by each frame expression in the list. For example,

method P(c: C, d: D, S: set<object>)
  modifies c, d, S

is the same as

method P(c: C, d: D, S: set<object>)
  modifies {c} + {d} + S

2.0. old

If you want to say that M has the effect of increasing the value of c.x, then you write a two-state postcondition that mentions the value of c.x in both the method's pre-state and the method's post-state. The former is notated by old(c.x), and the latter simply by c.x:

method M(c: C)
  modifies c
  ensures old(c.x) < c.x

This specification says nothing about the post-value of c.y. More precisely, the modifies clause gives M permission to update all of the fields of c and the ensures clause does not constrain the final value of c.y.

If you want to specify that the value of c.y is not changed, then you can add another postcondition:

method M(c: C)
  modifies c
  ensures old(c.x) < c.x && old(c.y) == c.y

This postcondition constrains the post-value of c.y to be the same as its pre-value.

2.1. unchanged

If you want to say that all fields of an object are unchanged, you can use an unchanged expression. For example,

method M(c: C, k: int)
  modifies c
  ensures k < 0 ==> unchanged(c)

This specification gives M license to modify the fields of c. However, the postcondition constrains the fields to have the initial values if k is negative.

An unchanged expression accepts a variable number of arguments, each a frame expression. In other words, what you put inside the parentheses that follow the unchanged keyword has the same syntax as modifies clauses. For example,

method P(c: C, d: D, S: set<object>, k: int)
  modifies c, d, S
  ensures k < 0 ==> unchanged(c, S)
{
  if d !in S {
    d.z := 5;
  }
  if 0 <= k {
    c.x := c.x + 4;
  }
}

is a method that verifies. Note that if d is in the set S and k is negative, then the postcondition says the fields of d must have their initial values, because unchanged(S) says that all fields of all objects in S must not have changed.

3. The fine print

3.0. modifies determined in pre-state

A modifies clause is evaluated in the method's pre-state.

method R(c: C, d: D)
  modifies c, c.y
{
  var prevCY := c.y;
  c.y := d;  // allowed by "modifies c"
  prevCY.z := 9;  // allowed by "modifies c.y"
  c.y.z := 9;  // not allowed
}

For the last assignment to be legal, the object denoted by c.y at the time of the assignment (namely, d) would have to be in the original modifies clause.

requires c.y == d

The frame expressions given in an unchanged expression are evaluated where the the unchanged is given. For example, the following method satisfies its specification, because the postcondition talks about the fields of the post-state value of c.y.

method S(c: C, d: D)
  requires c.y != d
  modifies c, c.y, d
  ensures unchanged(c.y)
{
  c.y.z := 12;
  c.y := d;
}

If you change unchanged(c.y) to unchanged(old(c.y)), then the postcondition says that the fields of the object denoted by the pre-state value of c.y must not have changed:

method S'(c: C, d: D)
  requires c.y != d
  modifies c, c.y, d
  ensures unchanged(old(c.y))
{
  c.y := d;
  d.z := d.z + 1;
}

So, the body of S' verifies. If the swap the implementations of methods S and S', then neither of them verifies.

3.1. old only affects the heap

old applies only to heap dereferences. If you want to think of it syntactically, then this means the . (dot) in field dereferences (including the . in this.x when you write just x and leave this implicit) and the [ ] (brackets) in array dereferences. In particular, in- and out-parameters, and local and bound variables are unaffected by old.

For example, consider

method W0(c: C, d: D) returns (k: int)
  modifies c
  ensures old(k == c.y.z)  // k refers to the final value of k
{
  k := c.y.z;
  c.y := d;
}

The postcondition of W0 holds, because k refers to the output value for k (not the arbitrary value that k starts off with inside the body, which would be meaningless to a caller, anyhow). Also, c inside the old expression refers to (constant) value of in-parameter c.

Here is another example method that verifies:

method W1(c: C, a: array<int>)
  requires 0 <= c.x < a.Length
  modifies c, a
{
  var m := a[c.x];
  a[c.x] := m + 5;
  c.x := c.x + 1;
  m := m + 2;
  assert old(m == a[c.x] + 2);
}

The assertion in the body could equally well have been written

assert m == old(a[c.x]) + 2;

method W2() {
  var d := new D;
  d.z := 7;
  assert old(d.z) == 7;  // error
}

method W3(c: C, a: array<int>)
  requires 100 <= c.x < a.Length
  requires forall i :: 0 <= i < c.x ==> a[i] == 5
  requires forall i :: c.x <= i < a.Length ==> a[i] == 6
  modifies c, a
  ensures 0 <= c.x < a.Length
{
  a[c.x] := 16;
  c.x := c.x - 1;
  a[c.x] := 15;
}

ensures a[c.x] == 15

ensures old(a[c.x]) == 6

ensures a[old(c.x)] == 16

ensures var k := c.x; old(a[k]) == 5

3.2. modifies permission is checked immediately

For every heap assignment in a method, Dafny checks that the method has license to modify the indicated heap location. That is, the heap location must either be allowed by the modifies clause or be newly allocated (that is, allocated since the start of the enclosing method). If the method does not have this license, then the heap assignment is illegal, even if the method later restores the previous value. For example, the following is illegal:

method M(c: C) {
  c.x := c.x + 1;  // error
  c.x := c.x - 1;
}

In fact, this is also illegal:

method M(c: C) {
  c.x := c.x;  // error
}

But for a method with the following specification:

method M(c: C)
  modifies c
  ensures unchanged(c)

both of the method implementations above are legal.

4. Advanced features

4.0. More precise frame expressions

It is appropriate to think of Dafny's frame expressions as operating at the object granularity. That is, modifies clauses (and also unchanged expressions, as well as the reads clauses of functions) take a set of objects and give permission to modify the fields of those objects (or, for unchanged, say that the fields of those objects are not changed, or, for reads, say that the function is allowed to depend on the fields of those objects).

It can happen that you want to be more precise. For example, suppose you want to say that a method may modify the y field of a given parameter c, but not the x field. You can specify this behavior by

method M(c: C)
  modifies c
  ensures old(c.x) == c.x

This works well if you want to modify most of the fields of c, but want to call out that some fields stay the same. (If a field never changes after construction, it is best to declare it as immutable, which you do with const.) But if instead most fields remain the same and you only want to modify one or two, then the use of old will feel verbose.

Dafny provides a way to give some frame expressions at the object-field granularity. You do this by appending a back-tick and the expression that denotes the object. For example, to specify that only the y field of c may change, you can write

method M(c: C)
  modifies c`y

This says M is not allowed to modify all fields of c, but only the y field. Note that this is quite different from saying modifies c.y, which gives M permission to modify all fields of the object denoted by c.y.

The object-field granularity can also be used in unchanged expressions (and reads clauses). For example, yet another way to specify the method M is

method M(c: C)
  modifies c
  ensures unchanged(c`x)

Just like you can abbreviate this.x by just x (if there is no ambiguity with other local names), you can also abbreviate this`x by just `x.

Regrettably, Dafny does allow this back-tick notation for array elements, for it would be mighty nice to be able to write specifications like

method P(a: array<int>, i: int, m: int, n: int)
  requires 0 <= i < a.Length
  requires 0 <= m <= n <= a.Length
  modifies a`[i], a`[m..n]  // error: this syntax is not supported

A future version of Dafny may support this syntax.

4.1. State labels

old and unchanged are examples of two-state predicates. That means they talk not just about the current state, but also about a previous state—namely, the pre-state of the enclosing method, in all the examples we've seen so far. (Well, old only talks about the previous state, not the current state, but it's still a two-state predicate, because it doesn't just talk about the current state.)

The primary use of two-state expressions is in postconditions. However, you can also use them, for example, in assertions in a method body, like so:

method L(c: C)
  modifies c
{
  c.x := c.x + 2;
  c.x := c.x + 3;
  c.x := c.x + 4;
  assert c.x == old(c.x) + 9 && unchanged(c`y);
}

Sometimes, you want to talk about a heap value in some intermediate state. One way to do that is to use ghost variables. For example:

method L1(c: C)
  modifies c
{
  c.x := c.x + 2;
  ghost var g := c.x;
  c.x := c.x + 3;
  ghost var h := c.x;
  c.x := c.x + 4;
  assert c.x == h + 4 == g + 7 == old(c.x) + 9;
}

If you want to refer to many values in the heap from an previous intermediate state, then you can use labels. These are the same labels as you would use to do a control-flow break out of a loop or other statement. Like in many other languages, the declaration of a label in Dafny ends with a : (colon). Unlike many other languages, Dafny also requires the declaration to start with the keyword label, which is intended to make the placement more prominent.

old and unchanged can be followed with @ and a label, which makes them two-state predicates that refer to the current state and the previous state. Here is an example:

method L2(c: C)
  modifies c
{
  c.x := c.x + 2;
  c.y := new D;
  label G:
  c.x := c.x + 3;
  label H:
  c.x := c.x + 4;
  assert c.x == old@H(c.x) + 4 == old@G(c.x) + 7 == old(c.x) + 9;
  assert unchanged@G(c`y);
}

Here's a more stimulating example:

method Inc(c: C, m: nat, n: nat)
  modifies c
  ensures c.x == old(c.x) + 3 * m + 2 * n
{
  var i := 0;
  while i < m
    invariant 0 <= i <= m
    invariant c.x == old(c.x) + 3 * i
  {
    c.x, i := c.x + 3, i + 1;
  }
  label Middle:
  i := 0;
  while i < n
    invariant 0 <= i <= n
    invariant c.x == old@Middle(c.x) + 2 * i
  {
    c.x, i := c.x + 2, i + 1;
  }
}