Dafny: Не работает проверка самого простого суммирования массивов. Может кто-нибудь объяснить мне, почему?

Поскольку массивы Dafny размещаются в куче, им разрешено использовать псевдонимы. Таким образом, вы можете вызвать свой метод, например, когда c и a указывают на один и тот же массив в памяти. Также возможно, что j == h. В этом случае постусловие может не выполняться, поскольку запись в c[j] также записывается в a[h] (поскольку c и a указывают на один и тот же массив и j == h).

Вы можете исправить это, добавив предварительное условие, что a != c и b != c.

Я написал ваш пример для проекта Dafny и как мы будем решать его с помощью кодовых действий: https://github.com/dafny-lang/dafny/issues/3102

Я воспроизвожу подробное решение здесь, чтобы вычислить самое слабое предварительное условие.

Если сделать утверждение явным, это приведет к

  {
    c[j] := a[h] + b[i];
    assert c[j] == a[h] + b[i];
  }

Теперь мы не можем просто «переместить утверждение вверх», потому что в противном случае нам пришлось бы рассуждать о состоянии кучи после присваивания, а old@ еще не может ссылаться на метку, определенную впоследствии. Итак, следующим шагом будет введение метки и выполнение самого слабого исчисления предусловия ниже присваивания

  {
    label before: // Added
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == a[h] + b[i]; // Added, now failing
    assert c[j] == a[h] + b[i];
  }

Хорошая вещь в том, что это поможет пользователю естественным образом открыть для себя «старый» синтаксис. Поскольку самое слабое предварительное условие теперь видит еще две потенциально конфликтующие ссылки, может быть предложено следующее кодовое действие для удаления ссылки на кучу после присваивания:

  {
    label before: // Added
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
    assert c[j] == a[h] + b[i];
  }

Теперь, поскольку это выражение вообще не относится к куче после присваивания c[j}, самое слабое исчисление предусловия сможет переместить это утверждение раньше и удалить выражения old@.

  {
    assert a[h] + b[i] == (if a == c && j == h then a[h] + b[i] else a[h]) + (if b == c && j == i then a[h] + b[i] else b[i]); // Just added, now failing.
    label before:
    c[j] := a[h] + b[i];
    assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
    assert old@before(a[h] + b[i]) == a[h] + b[i];
    assert c[j] == a[h] + b[i];
  }

и в конечном итоге переместите его в требование метода. Затем пользователь может уточнить это самое слабое предварительное условие, чтобы оставить a != c && b != c только в том случае, если он этого захочет. Или не.

Я также добавляю еще один ответ, потому что считаю его независимым. Постусловие по умолчанию ссылается на кучу в конце метода. Вы можете сделать так, чтобы постусловие сохранялось, сославшись на разыменование a и b в начале кучи, вставив old(...) следующим образом:

method addThreeArrays(a: array<int>, b: array<int>, c: array<int>, h: int, i: int, j: int)
  modifies c
  requires 0 <= h < a.Length
  requires 0 <= i < b.Length
  requires 0 <= j < c.Length
  
  ensures c[j] == old(a[h] + b[i])
  {
    c[j] := a[h] + b[i];
  }

Это работает как шарм, и это именно то, что делает ваш метод. Спасибо Рустану Лейно за то, что он указал мне на это решение.