Если Dafny не верит в неизменность массива

Пусть есть метод, который переставляет два первых элемента некоторого массива:

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

Нам важно, что сумма элементов при этом не изменилась. Записываем соответствующее постусловие и функцию вычисления суммы:

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

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;
}

На это Dafny говорит: A postcondition might not hold on this return path. И показывает на равенство sum. Ну ладно, вобщем-то это и непросто было бы автоматически доказать. Пишем теорему!

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);
{
 // ...
}

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

      theorem(c3, c1);
}

Пока доказательство теоремы нас не интересует, поэтому его тут нет. Ну, если уж мы сами покажем, как доказывать теорему, метод Main должен быть верным. Спрашиваем Dafny: A postcondition might not hold on this return path ! Как будто Dafny не видит нашу теорему! Ну-ка, добавим после нее ассершн, который теорема должна доказать:

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);
{
 // ...
}

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

      theorem(c3, c1);
      assert sum(c3) == sum(c1);
      assert sum(c1) == sum(old(a[..]));
      assert sum(c3) == sum(a[..]);
}

На это получаем: assertion violation! Dafny не верит в то, что в конце метода sum(c3) == sum(a[..]), но ведь до метода было c3 == a[..], после этого содержимое массива не менялось, a[..] тоже не меняет значение после перестановки 0'го и 1'го элемента. Как же побороть assertion violation ?


А побороть его не так сложно. Надо явно сказать, что в теореме a[..] не меняется. Для этого нам нужно передать в теорему сам массив (иначе мы не сможем выразить "неизменчивость") и сформулировать в нем неизменчивость:

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

ghost method theorem(a : array<int>, 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);

   requires a != null;
   ensures a[..] == old(a[..]);
{
 // ...
}

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

      theorem(a, c3, c1);
      assert sum(c3) == sum(c1);
      assert sum(c1) == sum(old(a[..]));
      assert sum(c3) == sum(a[..]);
}

После этого assertion violation исчезнет :)