如何检查集合中只有一个元素在dafny确保中发生了更改

Question

如何检查一个集合中只有一个元素在一个愚蠢的ensures中发生了更改？

示例：

method myMethod(myParameter: int)
requires myParameter >= 0
modifies mySet
ensures ONLY_ONE_ELEMENT_IN_THE_SET_HAS_CHANGED
{
...
}

Answer 1

如果您的意思是删除了一个元素并添加了另一个元素，则需要显式地将它们作为(ghost(返回变量提供，并使用old关键字引用mySet的前一个值

method myMethod(myParameter: int) returns (ghost removed: int, ghost added: int)
requires myParameter >= 0
modifies mySet
ensures old(mySet) - {removed} + {added} == mySet
{
...
}