Dafny 和发生次数计数

Question

我一直在研究 Dafny 中引理的使用，但我发现它很难理解，显然下面的例子没有验证，很可能是因为 Dafny 没有看到归纳法或引理之类的东西证明一些属性的计数？基本上，我不知道我需要如何或定义什么来帮助说服 Dafny 计数是归纳法等等。一些确保和不变量规范不是必需的，但这不是重点。顺便说一句，这在 Spec# 中更容易。

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  if |items| == 0 then 0 else
    (if items[|items| - 1] == item then 1 else 0)
        + count( items[..(|items| - 1)], item )
}

method occurences(items: array<int>, item: int) returns (r: nat)
  requires items != null
  ensures r <= items.Length
  // some number of occurences of item
  ensures r > 0  ==> exists k: nat :: k < items.Length
                     && items[k] == item
  // no occurences of item
  ensures r == 0 ==> forall k: nat :: k < items.Length
                     ==> items[k] != item
  ensures r == count( items[..], item )
{
  var i: nat := 0;
  var num: nat := 0;

  while i < items.Length
    // i is increasing and there could be elements that match
    invariant num <= i <= items.Length
    invariant num > 0 ==> exists k: nat :: k < i
                          && items[k] == item
    invariant num == 0 ==> forall k: nat :: k < i
                           ==> items[k] != item
    invariant num == old(num) + 1 || num == old(num)
    invariant num == count( items[..i], item )
  {
    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  return num;
}

Answer 1

我会使用基于多重集的 count 定义，然后一切正常：

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  multiset(items)[item]
}

method occurences(items: array<int>, item: int) returns (r: nat)
  requires items != null
  ensures r <= items.Length
  // some number of occurences of item
  ensures r > 0  ==> exists k: nat :: k < items.Length
                     && items[k] == item
  // no occurences of item
  ensures r == 0 ==> forall k: nat :: k < items.Length
                     ==> items[k] != item
  ensures r == count(items[..], item)
{
  var i: nat := 0;
  var num: nat := 0;

  while i < items.Length
    // i is increasing and there could be elements that match
    invariant num <= i <= items.Length
    invariant num > 0 ==> exists k: nat :: k < i
                          && items[k] == item
    invariant num == 0 ==> forall k: nat :: k < i
                           ==> items[k] != item
    invariant num == old(num) + 1 || num == old(num)
    invariant num == count(items[..i], item)
  {
    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  assert items[..i] == items[..];
  r := num;
}

我还想建议两种替代方法，以及针对您的原始设计的另一种解决方案。

在不改变实现的情况下，我个人大概会这样写规范：

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  multiset(items)[item]
}

method occurences(items: array<int>, item: int) returns (num: nat)
  requires items != null
  ensures num <= items.Length
  ensures num == 0 <==> item !in items[..]
  ensures num == count(items[..], item)
{
  num := 0;

  var i: nat := 0;
  while i < items.Length
    invariant num <= i <= items.Length
    invariant num == 0 <==> item !in items[..i]
    invariant num == count(items[..i], item)
  {
    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  assert items[..i] == items[..];
}

如果我也决定实现，那么我会这样写：

method occurences(items: array<int>, item: int) returns (num: nat)
  requires items != null
  ensures num == multiset(items[..])[item]
{
  num := multiset(items[..])[item];
}

有一种方法可以通过添加额外的断言来验证原件。注意。我认为 "old" 并没有按照您认为的循环不变式执行。

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  if |items| == 0 then 0 else
    (if items[|items|-1] == item then 1 else 0)
        + count(items[..|items|-1], item )
}

method occurences(items: array<int>, item: int) returns (r: nat)
  requires items != null
  ensures r <= items.Length
  // some number of occurences of item
  ensures r > 0  ==> exists k: nat :: k < items.Length
                     && items[k] == item
  // no occurences of item
  ensures r == 0 ==> forall k: nat :: k < items.Length
                     ==> items[k] != item
  ensures r == count( items[..], item )
{
  var i: nat := 0;
  var num:nat := 0;

  while i < items.Length
    invariant num <= i <= items.Length
    invariant num > 0 ==> exists k: nat :: k < i
                          && items[k] == item
    invariant num == 0 ==> forall k: nat :: k < i
                           ==> items[k] != item
    invariant num == count(items[..i], item)
  {
    assert items[..i+1] == items[..i] + [items[i]];

    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  assert items[..i] == items[..];
  r := num;
}

Dafny 和发生次数计数

Dafny and counting of occurrences

formal-verification

counting

induction

dafny