我可以在 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.[=23= 的先决条件]

导致我这样做的问题是试图过滤包含其他序列的序列：

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.

的新版本

我可以在 Dafny 中为高阶函数的参数允许先决条件吗？

Can I allow preconditions on the argument to a higher-order function in Dafny?

dafny