Dafny - не знаю, почему assert не будет выполняться после вызова метода, который вычисляет, содержит ли массив элемент - PullRequest
Новая
       18

Dafny - не знаю, почему assert не будет выполняться после вызова метода, который вычисляет, содержит ли массив элемент

1 голос
/ 24 октября 2019

Я пишу метод «Очистить», который выясняет, является ли предоставленный массив «чистым» от предоставленного ключа или нет вхождений элемента в массив. Таким образом, если вхождений нет, возвращается значение true, а при наличии одного из вхождений возвращается значение false. Вот мой код: 

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

method Test()
{
  var find: bool := false;
  var arr1 := new int[5];
  var key : int := 1;

  arr1[0],arr1[1],arr1[2],arr1[3],arr1[4] := 1,2,2,2,3;
  find := Clean(arr1, key);
  assert (find == false);
}

Метод Clean сам по себе не вызывает ошибок. Но когда я создаю тестовую функцию для вызова Clean, оператор assert для всех случаев, когда Clean возвращает true, но никогда не выполняется в случае, когда Clean возвращает false, и я не знаю, откуда она.

Я довольно новичок в Дафни, поэтому любые советы / указатели очень ценятся!

...