Yes, in these terms, the only "global variable" of Dafny is the heap. Let me offer the following explanation of the meaning of
old in Dafny:
In programming languages, there are operations that dereference memory. Memory is like a "big mutable variable", but the name of this "variable" is not given explicitly. In Dafny (and other languages, like Java), the two expressions that
dereference the heap memory are p.f (where p denotes an object reference and
f names a field) and a[k] (where a denotes an array reference and
k denotes an integer index). Note that this.f (like
this.pos above) can be written as just f where this. is implicit. Let us think of the syntactic
. and [ as both referring to the heap. That is, we can think of
o.f as get($Heap, o, f) and of a[k] as
get($Heap, a, k) where I'm using $Heap to denote the current value of heap memory and
get to denote an operation that reads a value from a memory given as a first argument.
The meaning of old is that it changes . and [ to refer not to the current heap, but instead to the heap at the beginning of the enclosing method. So, if we think of inserting a statement:
ghost var $Heap0 := $Heap;
at the beginning of the method (and letting the scope of $Heap0 extend throughout the body of the method and also into the method's postcondition), then
old(o.f) means get($Heap0, o, f) and old(a[k]) means
get($Heap0, a, k) . For other expressions, old simply distributes over all connectives. For example,
old((if n < 5 then o else p).f + a[k])
means
get($Heap0, if n < 5 then o else p, f) + get($Heap0, a, k)
Notes.
 Multidimensional arrays are like the singledimensional arrays shown above, except that
k is a list of expressions.  Note that in and outparameters, local variables, and bound variables are unaffected by
old . forall and exists quantifications over a reference type range over the references allocated in the current state. If such a quantifier is enclosed inside an
old , the quantifier ranges over those references allocated in the method's prestate.
Occasionally, it is useful to "invert" the old operation. To do this, use a let expression. For example, to use the current value of
this.pos to index into the old value of the array referenced by
buf , use:
var k := pos; old(buf[k])
In terms of the expansion above, it means:
get($Heap0, buf, get($Heap, this, pos))
Rustan
