Dafny - 检查数组值是否唯一，但嵌套的 forall 不由循环维护答案

【问题标题】：Dafny - Checking if array value is unique, but forall nested in exists not maintained by loopDafny - 检查数组值是否唯一，但嵌套的 forall 不由循环维护
【发布时间】：2020-01-31 06:52:58
【问题描述】：

我正在检查某个键是否在数组中只出现一次（其中 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;
  }

逻辑对我来说似乎是正确的 - 有什么我遗漏的吗？

【问题讨论】：

标签： dafny

【解决方案1】：

在我的设置中，Dafny 在尝试验证给定的循环不变量时会超时。但是，我认为您可以通过用更强的不变量替换该循环不变量来完成您想要的：

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

第一个声明在包含 a 的前 i 个元素的多重集中，键的计数等于计算的 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;
}

我相信最终的断言是你想要的。我不确定为什么 Dafny 需要倒数第二个断言 a[..a.Length] == a[..]，但是删除它会导致最后一个断言的验证失败。

【讨论】：