小编Car*_*arl的帖子

我对任何可验证的 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 …