Dafny Power User:

old and unchanged

old and unchanged

**Abstract.** This note addresses the question "What's the difference between `old`

and `unchanged`

?".

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.

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`

.

**Exercise 0.**

What does the following specification mean?

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

**Answer.**

It gives `M`

permission to modify the fields of `c.y`

. For example, the body
of `M`

can do the following assignment:

`c.y.z := 15;`

It does *not* give `M`

the permission to modify the `y`

field of object `c`

.
For example, the following is not allowed:

`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`

.

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
```

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.

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.

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.

**Exercise 1.**

Write a precondition for `R`

that makes all assignments legal.

**Answer.**

`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.

`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;`

**Exercise 2.**

What error message does Dafny produce for the following method?

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

**Answer.**

The error is

receiver must be allocated in the state in which its fields are accessed

The expression `old(d.z)`

tries to get pre-state value of the `z`

field of
(the current value of) `d`

. But the object referenced by `d`

was not allocated
in the pre-state of the method, so it makes no sense to ask for the value of
`d.z`

in the method's pre-state. Dafny detects this and produces an error.

**Exercise 3.**

Consider the following method:

```
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;
}
```

This method takes an array with more than `100`

elements. The first `c.x`

of elements start off as `5`

, and the rest equal `6`

. The `modifies`

clause
and postcondition say that the method is allowed to modify both the fields
of `c`

and the elements of `a`

. You can see that the method's implementation
satisfies that specification.

How do you write a postcondition that refers to

a) the final (that is, post-state) value of the array element at the
index given by the final value of `c.x`

?

b) the initial (that is, pre-state) value of the array element at the
index given by the initial value of `c.x`

?

c) the final value of the array element at the
index given by the initial value of `c.x`

?

d) (tricky!) the initial value of the array element at the
index given by the final value of `c.x`

?

**Answer.**

a) Easy peasy:

`ensures a[c.x] == 15`

b) Easy peasy:

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

c) By wrapping `old`

around `c.x`

, the dereference (that is, the dot) picks
up the initial value of `c.x`

. By making sure you don't wrap the array
dereference (that is, the brackets) inside `old`

, the expression `a[...]`

will pick up the final value of teh array element.

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

d) If we could, we'd wrap `old`

around the brackets, but not the `.`

. But
that doesn't work, because what goes between the parentheses of `old`

must
syntactically be an expression, not just some random characters. Instead,
we can use a let expression: let the bound variable `k`

be the final
value of `c.x`

, and then use this bound variable inside `old`

:

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

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.

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.

`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;
}
}
```