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

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

また、2 つの代替アプローチと、元の設計に対する別の解決策を提案したいと思います。

実装を変更しなければ、個人的にはおそらく次のように仕様を記述します。

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 - Dafny と出現回数のカウント

1 に答える 1

Related

Reference