Dafny使用sum量词时出现“rbrace expected”错误求助

你的代码错误出在sum量词的语法使用不当，Dafny要求遍历映射或集合的量词必须用in关键字明确指定范围，你漏掉了这个关键字，导致解析器无法正确识别语法结构，从而抛出"rbrace expected"错误。

修正后的代码 #

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

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

关键调整说明 #

• 在sum i后添加in关键字，明确i的取值范围是映射m.s的键集合
• 移除了if条件里多余的括号（Dafny中条件表达式的括号不是必须的，不影响功能但更简洁）
• 将函数参数的MapSet<int>改为MapSet<T>，因为你的MapSet泛型参数T并未在成员s中使用，这样函数可以适用于任意类型参数的MapSet实例

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