In Dafny, count set elements less than a threshold

Question

I'd like to count the elements in a Dafny that are set less than a threshold, but I can't figure out the 'ensure'.

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;

}

The error is: this operator chain cannot continue with an ascending operator

Answer 1

You have a syntax error. The ensures clause should be:

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

Because of the multiple different uses of | in this syntax, it's hard to read. You might want to factor out the set into a function just to give it a name:

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

Then you can write the ensures as

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