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
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)|