dafny - 如何在 Dafny 中编写一个干净的函数来获得最小的集合？

问题描述

我正在尝试编写一个函数来获取非空集的最小值。

这是我想出的：

method minimum(s: set<int>) returns (out: int)
requires |s| >= 1
ensures forall t : int :: t in s ==> out <= t
{
  var y :| y in s;
  if (|s| > 1) {
    var m := minimum(s - {y});
    out := (if y < m then y else m);
    assert forall t : int :: t in (s - {y}) ==> out <= t;
    assert out <= y;
  } else {
    assert |s| == 1;
    assert y in s;
    assert |s - {y}| == 0;
    assert s - {y} == {};
    assert s == {y};
    return y;
  }
}

这是次优的，原因有两个：

Dafny 给出“未找到触发条件”。线路警告，
```
assert forall t : int :: t in (s - {y}) ==> out <= t;
```
但是，删除此行会导致代码无法验证。我的理解是触发警告并不是很糟糕，它只是一个警告，Dafny 可能有线路问题。（即使它实际上似乎有帮助。）所以它让我觉得我在做一些次优或非惯用的事情。
这是相当低效的。（它每次都构造一个新的集合，所以它会是 O(n^2)。）但我没有看到任何其他方法来迭代一个集合。有没有更快的方法来做到这一点？集真的是为了在 Dafny 中编写“真实”的非幽灵代码吗？

所以我的问题（除了上面的）是：有没有更好的方法来编写minimum函数？

标签： dafny

在这种情况下，我建议忽略触发警告，因为尽管有警告，它似乎工作正常。（对于集合论运算符，Dafny 的触发推断有点过于保守，而 Z3 能够在低级别推断出良好的触发。）如果您真的想修复它，这里有一种方法。将代码的“then”分支替换为

var s' := (s - {y});
var m := minimum(s');
out := (if y < m then y else m);
assert forall t :: t in s ==> t == y || t in s';
assert forall t : int :: t in s' ==> out <= t;
assert out <= y;

第二个问题（关于效率）有些根本。（请参阅 Rustan 的论文“编译 Hilbert 的 Epsilon 运算符”，其中提到编译 let-such-that 语句会导致二次性能。）我更愿意将 Dafnyset视为不应编译的数学结构。（它可以编译的事实对于玩具程序来说是一种便利，而不是对于真正的系统，人们期望基于数据结构的集合的标准库实现。）

dafny - 如何在 Dafny 中编写一个干净的函数来获得最小的集合？

问题描述

解决方案

推荐阅读