Dafny 和发生次数计数

Dafny and counting of occurrences

我一直在研究 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;
}

我会使用基于多重集的 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;
}

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

  1. 在不改变实现的情况下,我个人大概会这样写规范:

    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[..];
    }
    
  2. 如果我也决定实现,那么我会这样写:

    method occurences(items: array<int>, item: int) returns (num: nat)
      requires items != null
      ensures num == multiset(items[..])[item]
    {
      num := multiset(items[..])[item];
    }
    
  3. 有一种方法可以通过添加额外的断言来验证原件。注意。我认为 "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;
    }