I have a method (fragment)
method read(buf:array<int>,p:nat,len:nat) returns(count:nat) modifies this;
// Other stuff.
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
Your last statement is right. From Boogie (the one that Dafny being translated into) manual , "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.
 KRM Leino. This is Boogie 2.
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
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
denotes an object reference and
names a field) and
denotes an array reference and
denotes an integer index). Note that
above) can be written as just
is implicit. Let us think of the syntactic
as both referring to the heap. That is, we can think of
get($Heap, o, f)
get($Heap, a, k)
where I'm using
to denote the current value of heap memory and
to denote an operation that reads a value from a memory given as a first argument.
The meaning of
is that it changes
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
extend throughout the body of the method and also into the method's postcondition), then
get($Heap0, o, f)
get($Heap0, a, k)
. For other expressions,
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
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
operation. To do this, use a let expression. For example, to use the current value of
to index into the old value of the array referenced by
var k := pos; old(buf[k])
In terms of the expansion above, it means:
get($Heap0, buf, get($Heap, this, pos))