如何在Dafny中表示一對（兩個元組）？

Question

如何編寫一個dafny function，它接受一系列整數並返回一系列對？例如，輸入= [1,2]，輸出= [對（1,1），對（1,2）]

我開始與

function foo (l : seq<int>) : seq<Pair> 
{ 
    if |l| == 0 then [] 
    else new Pair() .... 
} 

這似乎不工作。

Answer 1

你不能在函數中使用new，因爲函數在Dafny中是純的，它們不能修改堆。要麼使用inductive datatypes

datatype Pair = Pair(fst:int, snd:int) 

function foo (l : seq<int>) : seq<Pair> 
{ 
    if |l| <= 1 then [] 
    else [Pair(l[0],l[1])] + foo(l[2..]) 
} 

或者使用tuples

function foo (l : seq<int>) : seq<(int,int)> 
{ 
    if |l| <= 1 then [] 
    else [(l[0],l[1])] + foo(l[2..]) 
}