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

【问题标题】：How do I represent a pair (two tuple) in Dafny?如何在 Dafny 中表示一对（两个元组）？
【发布时间】：2016-08-06 22:05:56
【问题描述】：

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

我从

开始

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

这似乎不起作用。

【问题讨论】：

标签： dafny

【解决方案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..]) 
}

【讨论】：