dafny - Dafny使用递归函数查找序列索引

Question

我正在做达夫尼练习。我编写了一个递归函数来返回以双精度形式出现的元素序列。现在我想使用另一个递归函数找到这些双精度元素的索引。但我有点卡住了。

例如，在序列[1,4,2,2,4,6,6]中，双精度序列应该是[2,6]，索引序列应该是[3,6]，也就是最后一个双精度元素的索引.

这是我查找双打序列的代码：

function method doubles(s:seq<int>) :(r:seq<int>)
requires |s|>=0
ensures |r|<=|s|
ensures |r|>=0
ensures forall i:int :: 0 <= i <|r| ==> r[i] in s
decreases s 
{ 
    if(|s|==1 || |s|==0) then []
    else if (s[0]==s[1]) then [s[1]] + doubles(s[1..])
    else doubles(s[1..])
}

并找到双元素的索引。它现在不起作用：

function method doublesIndex(s:seq<int>) :(r:seq<int>)
requires |s|>=0
ensures |r|<=|s|
ensures |r|>=0
decreases s 
{ 
    if(|s|==1 || |s|==0) then [0]
    else if (s[0]==s[1]) then [s[1]] + doublesIndex(s[1..])
    else doublesIndex(s[1..])
}

标签： dafny