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

错误原因 #

Dafny 4.0对可编译代码中的var x :| P(x)（let-such-that表达式）新增了严格限制：要求表达式必须能唯一确定值。旧版本中这类表达式仅用于验证，编译时不做严格检查，但4.0版本将验证规则同步到了编译阶段，因此触发错误。

解决方案 #

不需要将整个函数设置为ghost，以下是几种可行的处理方式：

1. 使用标准库的Pick函数

Pick(s)是Dafny标准库提供的函数，可返回集合s中的任意元素，其实现满足编译时的唯一性要求。替换原表达式即可解决问题：

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 := Pick(s);
  if |s| == 1 then
    x
  else
    var sy := s - {x};
    var y := intsetmax(sy);
    if x > y then x else y
}

2. 利用整数集合的有序性选择唯一元素

对于整数集合，可以直接调用min(s)或max(s)获取唯一确定的元素（前提是集合非空，符合函数的前置条件）：

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 := min(s);
  if |s| == 1 then
    x
  else
    var sy := s - {x};
    var y := intsetmax(sy);
    if x > y then x else y
}

3. 将let-such-that表达式放入ghost上下文（仅验证场景）

如果仅需要函数通过验证，不需要编译执行，可以将x声明为ghost变量，这样编译时会忽略该变量的唯一性检查：

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

总结 #

• 若需要函数可编译执行，优先选择Pick函数或利用集合有序性的方法；
• 仅验证场景下可使用ghost变量，但无需将整个函数标记为ghost。

内容的提问来源于stack exchange，提问作者ZihaoZhang