Dafny 错误：使用 sum 时需要 rbrace

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
}

我在地图数据集的 dafny 代码中使用总和量词时遇到错误。根据vscode，错误出现在“sum i”中的i部分

尝试在代码中的任何地方放置大括号，但没有任何效果。

Answer 1

您是从 chatGPT 等 AI 中获取该片段吗？您可以使用基数运算符获取地图的大小。如果您尝试计算真实的映射项的数量，那么您将需要递归地执行此操作。

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

如果您需要在规范上下文之外（即非幽灵）使用此功能，您将需要指定对地图中的项目进行计数的顺序。看看这篇论文。 https://leino.science/papers/krml274.html