Dafny - проверка, является ли значение массива уникальным, но в целом вложенное в него не поддерживается циклом - PullRequest
Новая
       12

Dafny - проверка, является ли значение массива уникальным, но в целом вложенное в него не поддерживается циклом

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

Я проверяю, появляется ли какой-либо ключ только один раз в массиве (где b - возвращаемое значение), однако следующий инвариант говорит, что он не поддерживается циклом: 

invariant b <==> exists j | 0 <= j < i :: a[j] == key && forall k | 0 <= k < i && j != k :: a[k] != key

Цикл продолжается следующим образом 

  var i := 0;
  b := false;
  var keyCount := 0;
  while i < a.Length
  invariant 0 <= i <= a.Length
  invariant b <==> exists j | 0 <= j < i :: a[j] == key && forall k | 0 <= k < i && j != k :: a[k] != key
  {
    if (a[i] == key)
    { keyCount := keyCount + 1; }
    if (keyCount == 1)
    { b := true; }
    else
    { b := false; }
    i := i + 1;
  }

Логика мне кажется здоровой - что-то мне не хватает?

1 Ответ

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

На моей установке Дафни отключается при попытке проверить заданный инвариант цикла. Тем не менее, я думаю, что вы можете сделать то, что вы хотите, заменив этот инвариант цикла более сильными инвариантами: 

invariant multiset(a[..i])[key] == keyCount
invariant b <==> (keyCount == 1)

Первые утверждают, что в мультимножестве, содержащем первые i элементов a, количество ключей равнок вычисленному keyCount. Второй относится b и keyCount. Полное решение приведено ниже: 

method only_once<a(==)>(a: array<a>, key: a)
{
  var i := 0;
  var b := false;
  var keyCount := 0;
  while i < a.Length
  invariant 0 <= i <= a.Length
  invariant multiset(a[..i])[key] == keyCount
  invariant b <==> (keyCount == 1)
  {
    ghost var preCount := keyCount;
    if (a[i] == key)
    { keyCount := keyCount + 1; }
    if (keyCount == 1)
    { b := true; }
    else
    { b := false; }
    i := i + 1;
  }
  assert a[..a.Length] == a[..];
  assert b <==> multiset(a[..])[key] == 1;
}

Я считаю, что последнее утверждение - это то, что вы хотите. Я не уверен, зачем Дафни нужен второй до последнего утверждения a[..a.Length] == a[..], но его удаление приводит к сбою проверки последнего утверждения.

...