Dafny 中的高阶计数 (P)

Question

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

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

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

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

Dafny 中的高阶计数 (P)

High order Count(P) in Dafny

arrays

predicate

count

higher-order-functions

dafny