dafny - 如何在 Dafny 中表示一对（两个元组）？

Question

我怎样才能写一个function接受一个整数序列并返回一个对序列的 dafny？例如，输入 = [1,2]，输出 = [Pair(1,1), Pair(1,2)]

我从

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

这似乎不起作用。

Answer 1

您不能new在函数中使用，因为在 Dafny 中函数是纯函数，它们不能修改堆。要么使用归纳数据类型

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..]) 
}

或者使用元组

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