Dafny实现O(n)时间复杂度的occursInBoth方法求助

问题背景 #

给定Asc谓词判断数组是否升序排列，需实现occursInBoth方法，判断两个升序数组是否存在相同元素，存在返回true，否则返回false。要求计算步骤不超过a.Length + b.Length，且满足以下规范：

• 前置条件：Asc(a) && Asc(b)
• 后置条件：r == (exists i,j:: 0<=i<a.Length && 0<=j<b.Length && a[i]==b[j])

原始Asc谓词与方法框架：

predicate Asc(a: array<int>)
  reads a
{
  forall i,j:: 0<=i<j<a.Length ==> a[i] <= a[j]
}

method occursInBoth(a: array<int>, b: array<int>) returns (r : bool)
  requires Asc(a) && Asc(b)
  ensures r == (exists i,j:: 0 <=i<a.Length && 0<=j<b.Length && a[i]==b[j])
{
  ... // implement yourself
}

问题重现 #

以下是尝试的实现，但最后一个断言无法通过Dafny验证，因为循环不变式不足以证明返回false时确实无公共元素：

predicate Asc(a: array<int>)
  reads a
{
  forall i,j:: 0<= i < j < a.Length ==> a[i] <= a[j]
}

method occursInBoth(a: array<int>, b: array<int>) returns (r : bool)
  requires Asc(a) && Asc(b)
  ensures r == (exists i, j:: 0 <= i < a.Length && 0 <= j < b.Length && a[i] == b[j])
{
  var i := 0;
  var j := 0;

  while i < a.Length && j < b.Length
    invariant 0 <= i <= a.Length && 0 <= j <= b.Length
  {
    if a[i] < b[j] {
      i := i + 1;
    } else if a[i] > b[j] {
      j := j + 1;
    } else {  // a[i] == b[j]
      return true;
      assert r == (exists i, j:: 0 <= i < a.Length && 0 <= j < b.Length && a[i] == b[j]); // 此断言成立
    }
  }
  return false;
  assert r == (exists i, j:: 0 <= i < a.Length && 0 <= j < b.Length && a[i] == b[j]); // 此断言不成立
}

正确实现 #

核心是补充强循环不变式，证明循环过程中已遍历的元素不可能与对方数组的任何元素匹配，从而让Dafny验证返回false的正确性：

predicate Asc(a: array<int>)
  reads a
{
  forall i,j:: 0<= i < j < a.Length ==> a[i] <= a[j]
}

method occursInBoth(a: array<int>, b: array<int>) returns (r : bool)
  requires Asc(a) && Asc(b)
  ensures r == (exists i, j:: 0 <= i < a.Length && 0 <= j < b.Length && a[i] == b[j])
{
  var i := 0;
  var j := 0;

  while i < a.Length && j < b.Length
    invariant 0 <= i <= a.Length && 0 <= j <= b.Length
    // 已遍历的a[0..i-1]都小于b中所有元素，不可能匹配
    invariant forall k: int, l: int :: 0 <= k < i && 0 <= l < b.Length ==> a[k] < b[l]
    // 已遍历的b[0..j-1]都小于a中所有元素，不可能匹配
    invariant forall k: int, l: int :: 0 <= l < j && 0 <= k < a.Length ==> b[l] < a[k]
  {
    if a[i] < b[j] {
      i := i + 1;
    } else if a[i] > b[j] {
      j := j + 1;
    } else {
      return true;
    }
  }

  return false;
}

关键说明 #

• 新增的两个不变式是验证的核心：
  1. 当i递增时，说明a[i] < b[j]，结合数组升序特性，a[0..i]都小于b[j]，进而小于b[j..b.Length-1]，因此a[0..i]不可能与b中任何元素匹配。
  2. 同理，j递增时，b[0..j]不可能与a中任何元素匹配。
• 循环结束时，要么i遍历完a，要么j遍历完b。结合不变式可推导出：此时不存在任何i,j使得a[i]==b[j]，因此返回false满足后置条件。

内容的提问来源于stack exchange，提问作者Demir Akbalıkcı