Dafny和发生次数计数 [英] Dafny and counting of occurrences

问题描述

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

I've been looking at the use of lemmas in Dafny but am finding it hard to understand and obviously the below example doesn't verify, quite possibly because Dafny doesn't see the induction or something like a lemma to prove some property of count? Basically, I don't know how or what I need to define to help convince Dafny that counting is inductive and a thing etc. Some of the ensures and invariants specifications are not necessary, but that's not the point. btw, this was easier in 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;
}

推荐答案

我将基于多集使用 count 的定义，然后一切正常:

I would use a definition of count based around a multiset, then everything works:

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

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

I would also like to suggest two alternative approaches, and another solution to your original design.

1. 在不更改实现的情况下，我个人可能会这样写规范:

1. Without changing the implementation, I personally would probably write the specification like this:

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[..];
}

如果我也要决定实现方式，那么我会这样写:

If I were to decide on the implementation too then I would write it like this:

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

有一种方法可以通过添加额外的断言来获取原始内容进行验证.注意我认为旧的"在循环不变式中不会像您认为的那样发挥作用.

There is a way to get the original to verify by adding an extra assertion. NB. I think that "old" doesn't do what you think it does in a loop invariant.

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和发生次数计数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！