Dafny函數返回一組點

Question

的

讓Rectangle和Pair是中定義的Dafny數據類型如下：

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

一個數學抽象/當前矩形，我想在Dafny到碼錶示，是該矩形包含的所有點（i，j）的集合。例如矩形矩形（pos：（5,5），width = 2，height = 3）表示點集合：{（5,5），（6,5），（7,5），（5， 6），（6,6），（7,6）}

讓abs是函數方法（一行法），用於返回該抽象的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)}; 
}