Wie stelle ich ein Paar (zwei Tupel) in Dafny dar?

Question

Wie kann ich einen Dafny function schreiben, der eine Folge von Ints aufnimmt und eine Sequenz von Paaren zurückgibt? B. Eingang = [1,2], output = [Paar (1,1), Paar (1,2)]

Ich begann mit

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

, das nicht zu funktionieren scheint.

Answer 1

Sie können new nicht in einer Funktion verwenden, da Funktionen in Dafny rein sind, dürfen sie den Heap nicht ändern. Entweder verwenden 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..]) 
} 

Oder verwenden tuples

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