Dafny统计集合中小于阈值元素的方法及ensure后置条件报错问题

错误原因 #

报错this operator chain cannot continue with an ascending operator是因为Dafny语法解析器无法正确识别|{i in numbers | i < threshold}|这种写法——集合推导式直接紧跟基数运算符|时，语法优先级解析出现冲突。

解决方案 #

有两种可行的修复方式，同时需要补充循环不变式帮助Dafny验证后置条件：

方式一：给集合推导式加括号 #

通过额外括号明确集合推导式的范围，让解析器正确识别基数运算符的作用对象：

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |({i in numbers | i < threshold})|
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
    invariant count == |{i in numbers - ss | i < threshold}|  // 循环不变式：已处理元素中小于阈值的数量
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }
  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  assert c == 3;  // 现在可以正常验证这个断言
}

方式二：用求和表达式替代集合基数 #

改用sum量化表达式直接计算符合条件的元素数量，这种写法更直观，也避免了语法解析问题：

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == (sum i in numbers if i < threshold then 1 else 0)
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
    invariant count == (sum i in numbers - ss if i < threshold then 1 else 0)
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }
  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  assert c == 3;
}

关键说明 #

• 补充循环不变式是必须的：Dafny需要这个不变式来跟踪循环过程中count和剩余集合ss的关系，从而证明循环结束后count满足后置条件。
• 两种方案都能解决语法错误，且能让Dafny成功验证方法的正确性。

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