Dafny error: rbrace expected when using sum

Question

datatype MapSet<T> = MapSet (s : map<int,bool>)

function getSize<T> (m:MapSet<int>): int {
   sum i: m.s :: if (m.s[i]) then 1 else 0
}

I'm getting an error using using the sum quantifier in my dafny code for a map dataset. According to vscode, the error appears on the i part in the "sum i"

Tried putting curly braces everywhere on the code, nothing worked.

Answer 1

Did you get that sum snippet from an AI like chatGPT or copilot? You can get the size of a map using the cardinality operator. If you are trying to count the number of mapped items that are true then you will need to do it recursively.

datatype MapSet = MapSet (s : map<int,bool>)

function getSize(m:MapSet): nat {
   |m.s|
}

ghost function getTrueCount(m : MapSet): nat 
    decreases |m.s|
{
    if |m.s| == 0 then 0 else 
    var x :| x in m.s; 
    if m.s[x] then 1 + getTrueCount(MapSet(m.s-{x})) else getTrueCount(MapSet(m.s-{x}))
    
}

If you need this function outside of specification contexts (i.e. non-ghost) you'll need to specify an order in which to count the items in the map. Take a look at this paper. https://leino.science/papers/krml274.html

Or you can use sets.

function getTrueSetCount(m : MapSet): nat 
{
    |set key | key in m.s && m.s[key]|
}