Как представить пару (два кортежа) в Dafny?

Как я могу написать dafny function, который принимает последовательность целых чисел и возвращает последовательность пар? например, ввод = [1,2], вывод = [Пара (1,1), Пара (1,2)]

я начал с

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

который, кажется, не работает.


dafny
person JRR    schedule 15.04.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы не можете использовать 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..]) 
}
person lexicalscope    schedule 15.04.2016