主页 / coding / 问题 / 76923628
Accepted
Carl
Asked: 2023-08-18 00:54:53 +0800 CST

在 Dafny 中，计算小于阈值的集合元素

  • 772

我想计算 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|
  {
    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;

}

错误是：this operator chain cannot continue with an ascending operator

verification

1 个回答

  1. Best Answer

    您有语法错误。该ensures条款应该是：

    ensures count == |set i | i in numbers && i < threshold|

    由于|该语法中有多种不同的用法，因此很难阅读。您可能想将 分解set成一个函数只是为了给它一个名称：

    function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
  set i | i in numbers && i < threshold
}

    然后你可以ensures写成

    ensures count == |SetLessThan(numbers, threshold)|
    • 1

相关问题