使用Dafny验证统计整数集中小于阈值元素的CountLessThan函数

我接受任何可验证的CountLessThan函数写法，以下是我的实现代码：

function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
  set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |SetLessThan(numbers, threshold)|
{
  count := 0;
  var shrink := numbers;
  var grow := {};
  while |shrink| > 0
    decreases shrink
    invariant shrink + grow == numbers
    invariant count == |SetLessThan(grow, threshold)|
  {
    var i: int :| i in shrink;
    shrink := shrink - {i};
    grow := grow + {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;
}

这是定义有序集合、有序映射及范围集合的一小步。

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