如何解决 Dafny 中 let-such-that 表达式中的未确定问题？

Question

这是一个例子：

function intsetmax(s:set<int>):int
  requires |s| > 0
  ensures  var m := intsetmax(s);
           m in s && forall i :: i in s ==> m >= i
{
  var x :| x in s;
  if |s| == 1 then
    assert |s - {x}| == 0;
    x
  else
    var sy := s - {x};
    var y := intsetmax(sy);
    assert forall i :: i in s ==> i in sy || i == x;
    if x > y then x else y
}

函数“intsetmax”想要查找集合中的最大元素，但它显示错误“要可编译，let-such-that 表达式的值必须唯一确定”，因为语句“var x :|” x in s"。

此代码适用于低于 4.0 的 Dafny 版本，但使用 4.0 时会报告错误。

那么，如何解决呢？我必须将该功能设置为“ghost”吗？有没有办法获取集合中的元素？

Answer 1

在低于 4.0 的 Dafny 版本中，

function

表示

ghost function

。所以你应该将该函数标记为

ghost

。

Answer 2

就我个人而言，我认为这是 Dafny 编译器中的一个错误（即您之前可以将其编译为

function method

）。我假设该错误是在从 Dafny 3 切换到 Dafny 4 时引入的。查看更多详细信息此处。