ghost методы в Dafny могут изменять heap

Например, эта программа не доказывается по этой причине: http://rise4fun.com/Dafny/wp1 (объяснение см. в предыдущем посте). Чтобы указать, что ghost метод на самом деле не меняет память, надо его обрамить так:

ghost var cc := a[..];
call the ghost method
assert cc == a[..];

Результат: http://rise4fun.com/Dafny/zNyn .


Для тех, у кого не открывается rise4fun, код по первой ссылке:

function sum(c : seq<int>) : int
{ if |c| == 0 then 0 else c[0] + sum(c[1..]) }

ghost method theorem(c : seq<int>, c1 : seq<int>)
   requires |c1| > 1;
   requires |c| == |c1|;
   requires c[0] == c1[1];
   requires c1[0] == c[1];
   requires c[2..] == c1[2..];
   ensures sum(c) == sum(c1);
{
  assert c[1..][1..] == c[2..];
  assert c1[1..][1..] == c1[2..];
}

method Main(a : array<int>)
   requires a != null;
   requires a.Length > 1;
   ensures sum(a[..]) == sum(old(a[..]));
   modifies a;
{
      var t := a[0]; a[0] := a[1]; a[1] := t;

      theorem(a[..], old(a[..]));
}