dafny нарушение утверждения при использовании результата метода

Вам нужно указать пункт ensures на isClean. Когда Dafny проверяет программу, она просматривает только один method за раз. Поэтому, когда Дафни проверяет Main, он вообще не смотрит на определение isClean. Вместо этого он смотрит только на предложения requires и ensures.

У вас уже есть трудная часть доказательства в инварианте цикла. По сути, вам просто нужно изменить копию этого инварианта, чтобы он имел смысл в контексте вызывающей стороны, как предложение ensures, например:

ensures clean <==> (forall k :: 0 <= k < a.Length ==> a[k] != key)

(Добавьте это прямо под предложением requires в isClean.) В этом предложении ensures clean относится к именованному возвращаемому значению метода isClean. Если вы добавите это предложение, Dafny все равно будет жаловаться, потому что вы просите его доказать, что квантификатор forall равен false. Это эквивалентно попытке доказать квантор exists true и требует явного свидетеля, который представляет собой значение k, из-за которого тело формулы оказывается true/false.

В этом случае интуитивная причина, по которой isClean возвращает false, заключается в том, что a[0] имеет значение 1, поэтому a не чисто от 1. Мы можем продемонстрировать этот свидетель Дафни, добавив утверждение

assert a[0] == 1;

в тело Main сразу после вызова isClean.

Для ясности вот полная версия программы, которая проверяет:

method Main() {
  var a := new int[3];
  a[0], a[1], a[2] := 1,2,3;
  var v := isClean (a, 1);
  assert a[0] == 1;
  assert v == false;
}

method isClean(a: array <int>, key: int) returns (clean: bool)
  requires a.Length > 0
  ensures clean <==> (forall k :: 0 <= k < a.Length ==> a[k] != key)
{
  var i := 0;
  while (i < a.Length)
    invariant 0 <= i <= a.Length
    invariant forall k :: 0 <= k < i ==> a[k] != key
  {
    if (a[i] == key) {
      clean := false;
      return;
    }
    i := i + 1;
  }
  clean := true;
}