Precise meaning of "old" when the expression contains bound variables

Aug 25, 2014 at 4:28 AM
I have a method (fragment)
method read(buf:array<int>,p:nat,len:nat) returns(count:nat) modifies this; 
    // Other stuff.
    ensures buf[p..p+count]==data[old(pos)..pos];
    ensures forall n:: p+count<n<=buf.Length ==> buf[n..]==old(buf[n..]);
where "old" is used twice. For the first one, I assume the effect is as if a statement
ghost var pos0:= pos
is interpolated at the beginning of the method, and old(pos) in the ensures is interpreted as pos0.

But what about the second one: Interpolating
ghost var bufN0:= buf[n..]
at the beginning doesn't make sense, because n is out of scope. So what does it really mean?
--- Does it (e.g.) lambda-abstract over n?
--- Or would it be the same to write old(buf)[n..] ?
Sep 1, 2014 at 5:49 PM
Edited Sep 1, 2014 at 5:54 PM
Hello Nunibad

Your last statement is right. From Boogie (the one that Dafny being translated into) manual [1], "Only global variables are affected by old expressions".

If you want to know the precise meaning of old expression, why not check the printed Boogie program for the source Dafny program using the following command, it is very interesting:
dafny /print:output.txt input.dfy
For your ensure clause of method read, the expression "buf[n..]==old(buf[n..])" will translate into something like:
Seq#equal (...Seq#FromArray($Heap, buf#4)..., ...Seq#FromArray(old($Heap), buf#4)...)
It is worthwhile to notice where the old expression being placed.

[1] KRM Leino. This is Boogie 2.

Marked as answer by rustanleino on 9/9/2014 at 1:54 PM
Sep 9, 2014 at 8:53 PM
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])
get($Heap0, if n < 5 then o else p, f) + get($Heap0, a, k)
  • Multi-dimensional arrays are like the single-dimensional arrays shown above, except that k is a list of expressions.
  • Note that in- and out-parameters, 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 pre-state.
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))
Marked as answer by rustanleino on 9/9/2014 at 1:54 PM