Dafny 中的高阶 Count(P)

问题描述

我想在数组上使用高阶 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/

解决方法

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

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,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