我可以允许对 Dafny 中的高阶函数的参数设置先决条件吗？

Question

有没有办法说高阶函数允许对它作为参数的函数设置先决条件？

这是我要解决的具体情况。我编写了这个函数，用于根据谓词过滤seq 中的项目：

function method filterSeq<T>(s: seq<T>, fn: T -> bool): seq<T>
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: fn(filterSeq(s, fn)[i]) == true
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: filterSeq(s, fn)[i] in s
  ensures forall i | 0 <= i < |s| :: fn(s[i]) ==> s[i] in filterSeq(s, fn)
  {
    if |s| == 0 then [] else (
      if fn(s[0]) then [s[0]] + filterSeq(s[1..], fn) else filterSeq(s[1..], fn)
    )
  }

这涵盖了我关心的后置条件，但没有说明fn 的论点。我想说，对于在s 中适用于所有T 的任何属性，此属性是允许作为fn 的前提条件的。

导致我出现此问题的问题是尝试过滤包含其他序列的序列：

var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];
assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

var result := filterSeq(sequences, sequence => sequence[0] == 4);

当我尝试这个时，我在sequence[0] 上收到一个错误，上面写着index out of range。很公平，我尝试为 lambda 添加一个先决条件：

var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

var result := filterSeq(sequences,
  sequence requires |sequence| == 3 => sequence[0] == 4);

现在我在 lambda 参数上收到错误 value does not satisfy the subset constraints of 'seq<int> -> bool' (possible cause: it may be partial or have read effects)。这也是有道理的，我传递了一个部分函数，​​我在其中为非部分函数编写了类型签名。

我的问题是：如何更改 filterSeq 以允许这样做？我可以以某种方式编写它以便它可以在任意前提条件下工作，还是我必须编写一个单独的 filterSeqOfSequences 方法来涵盖这个特定的用例？

Answer 1

很好的问题。答案是肯定的。您需要使用 Dafny 的偏函数概念，它是用双虚线箭头编写的，例如 T --> bool。如果f 有这种类型，那么f.requires 就是它的前置条件。 （实际上，您可以将总函数类型T -> bool 视为T --> bool 的一个特例，其中f.requires 对于T 类型的所有值都为真。）

这是重写高阶函数以接受部分函数作为参数的一种方法：

function method filterSeq<T>(s: seq<T>, fn: T --> bool): seq<T>
  requires forall x | x in s :: fn.requires(x)        // ***
  ensures forall x | x in filterSeq(s, fn) :: x in s  // ***
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: fn(filterSeq(s, fn)[i]) == true
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: filterSeq(s, fn)[i] in s
  ensures forall i | 0 <= i < |s| :: fn(s[i]) ==> s[i] in filterSeq(s, fn)
{
  if |s| == 0
  then []
  else if fn(s[0]) 
  then [s[0]] + filterSeq(s[1..], fn) 
  else filterSeq(s[1..], fn)
}

method Test()
{
  var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

  assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

  var result := filterSeq(sequences,
    sequence requires |sequence| == 3 => sequence[0] == 4);
}

我刚刚对您的代码做了两处更改，标记为***。

首先是您在问题中已经提到的filterSeq 的新前提条件，它要求fn.requires 包含s 的所有元素。其次，我们还需要一个新的技术后置条件来保证filterSeq 的输出是其输入的一个子集。这是为了确保其他后置条件的格式良好，这些后置条件尝试在输出元素上调用fn。

Test 方法根本没有改变。它只适用于新版本的filterSeq。