Ghost variables only in specification contexts

Feb 7, 2013 at 3:02 AM
When I compile

method Test() {
ghost var x:= 0;
x:= x+1;
ghost var y:= new int[1];
y[0]:= 0;
y[0]:= y[0]+1;

I get

Dafny program verifier version, Copyright (c) 2003-2013, Microsoft.
test6.dfy(6,10): Error: ghost variables are allowed only in specification contexts
1 resolution/type errors detected in test6.dfy

where Dafny seems to object to the occurrence of y[0] on the right of the assignment to itself. But with (scalar) x, it is ok.

What's the rationale for this?
Feb 7, 2013 at 4:56 PM
Arrays are objects in the heap, and their elements are like fields. That is, you can think of a[E] as computing the "field name" E and then accessing that field of a. Those fields (that is, the array elements) are currently always non-ghost. So the fact that the pointer to the array is stored in a ghost variable does not help you.

It would be nice to have ghost arrays, but that would required some changes in the type system.

The workaround is to use a sequence instead of an array. Sequences are value types.

Feb 7, 2013 at 10:06 PM
Thanks Rustan for the explanation! And for the work-arounds.