Dafny 中的高阶计数 (P)

Question

我想在数组上使用高阶 Count(P) 函数，例如：

Count(even, a)，或Count(higher_than_10, a)，其中第一个参数是谓词，第二个参数是数组。

也就是说，计算这个 P 命题在一个数组上出现了多少次。

Dafny 有办法做到这一点吗？我认为这种函数是存在的，但可能它们的语法已经改变了。

谢谢

我已经看过了：

-https://stackoverflow.com/questions/35167124/dafny-and-counting-of-occurrences
-https://stackoverflow.com/questions/51379857/polymorphism-in-dafny
-https://gitter.im/dafny-lang/community?at=5d90c402086a72719e848f24
-https://www.imperial.ac.uk/events/104961/higher-order-functions-in-the-verification-aware-programming-language-dafny-k-rustan-m-leino/

Answer 1

这是定义此类函数的一种方法。

function method CountHelper<T>(P: T -> bool, a: array<T>, i: int): int
  requires 0 <= i <= a.Length
  reads a
  decreases a.Length - i
{
  if i == a.Length
  then 0
  else (if P(a[i]) then 1 else 0) + CountHelper(P, a, i+1)
}

function method Count<T>(P: T -> bool, a: array<T>): int
  reads a
{
  CountHelper(P, a, 0)
}

method Main()
{
  var a := new int[10] (i => i);
  var evens := Count(x => x % 2 == 0, a);
  print evens, "\n";
  var bigs := Count(x => x >= 5, a);
  print bigs, "\n";
}

运行时，它会按预期打印两次5。

$ dafny /compile:3 count.dfy
Dafny 3.0.0.20820

Dafny program verifier finished with 3 verified, 0 errors
Running...

5
5