counting - 达夫尼和发生次数

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;
}

score 2 · Accepted Answer

我会使用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];
}

有一种方法可以通过添加额外的断言来验证原件。注意。我认为“旧”不会做你认为它在循环不变量中所做的事情。

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;
}

counting - 达夫尼和发生次数

1 回答 1

Related

Reference