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