dafny - Dafny 函数返回一组点

Question

LetRectangle和PairBe Dafny 数据类型定义如下：

datatype Rectangle = rect(pos: Pair, width: int, height: int)
datatype Pair = pair(x: int, y: int)

这个矩形的一个数学抽象/表示，我想用 Dafny 编码，是这个矩形包含的所有点 (i,j) 的集合。例如矩形 rect(pos:(5,5), width=2, height=3) 表示点的集合：{(5,5), (6,5), (7,5), (5, 6), (6,6), (7,6)}

假设abs是一个函数方法（单行方法），它以 a 的形式返回这个抽象set<Pair>，给定一个类型的变量Rectangle

function method abs(rect: Rectangle): set<Pair>
{
    //..?
}

有谁知道如何在 Dafny 中用一行来表达这个集合？

Answer 1

您的示例似乎交换了我期望的高度和宽度的含义，但这是一个解决方案：

function method abs(rect: Rectangle): set<Pair>
{
    set x:int, y:int | 0 <= x - rect.pos.x < rect.height &&
                       0 <= y - rect.pos.y < rect.width :: pair(x, y)
}

以下引理表明该解决方案满足您的测试用例：

lemma lemma_Test()
{
    var r := rect(pair(5, 5), 2, 3);
    var s := abs(r);
    assert s == {pair(5,5), pair(6,5), pair(7,5), pair(5,6),
                 pair(6,6), pair(7,6)};
}