iterator - 如何在 Dafny 中迭代有限集对象的元素？

Question

在 Dafny 中迭代有限集对象的元素的最佳方法是什么？一个工作代码的例子会很有趣。

Answer 1

这个答案解释了如何使用 while 循环而不是通过定义迭代器来做到这一点。诀窍是使用“赋值”运算符 :| 来获得一个值 y，使得 y 在集合中，然后在该集合上重复 y 删除，继续直到没有更多元素。减少条款在这里是必要的。有了它，Dafny 证明了 while 循环的终止，但没有它，就不行。

method Main()
{
    var x: set<int> := {1, 2, 3};
    var c := x;
    while ( c != {} )
        decreases c;
    {
        var y :| y in c;
        print y, ", ";
        c := c - { y };
    }
}