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

【问题标题】：How do I iterate over the elements of a finite set object in Dafny?如何在 Dafny 中迭代有限集对象的元素？
【发布时间】：2018-07-22 05:03:06
【问题描述】：

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

【问题讨论】：

标签： iterator dafny

【解决方案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 };
    }
}

【讨论】：