Dafny 无法证明函数方法等价，高阶多态递归 vs 线性迭代

如何解决Dafny 无法证明函数方法等价，高阶多态递归 vs 线性迭代

这个消息会有点长，但那是因为我想尽可能地解释它。

在 Dafny 中，我遇到了下一个问题：给定一个数组，计算发生这种情况的长度为 k 的段的数量；片段左半部分的阳性数大于或等于右半部分。

举个例子（想象段只能是偶数，所以没有关于一半是什么的讨论）：

k=2 ---> count(array[-4,-2,2,1],k) ---> 2,as [-4,-2] fulfills and also [2,1]
k=4 ---> count(array[-4,k) ---> 0,1] does not fulfil.
k=6 ---> count(array[-4,as there are not length 6 segments.

我已经通过两种方式实现了这一点：一种是使用函数，使用高阶和多态性（但不是线性的），另一种是使用线性迭代实现。

函数是这样工作的：

1. 我们定义了一个 Count 函数，它计算数组上的一个属性。
2. 我们定义了一种方法，在给定数组的情况下，生成给定长度的所有段。
3. 我们定义了一个谓词，它使用 Count 告诉我们该属性是否满足。

function method CountAux<T>(P: T -> bool,sequ: seq<T>,i: int): int 
//the warning just warns about how it is implemented,as when it warns about the triggers' choice
  requires 0 <= i <= |sequ|
  decreases |sequ| - i //necessary to prove termination
  ensures CountAux(P,sequ,i)>=0; //trivial
{
  if i == |sequ| then 0
  else (if P(sequ[i]) then 1 else 0) + CountAux(P,i+1)
}

function method Count<T>(P: T -> bool,sequ: seq<T>): int
  ensures CountAux(P,0)>=0; //trivial
{
  CountAux(P,0)
}

function method produce_segments (sequ:seq<int>,seg_length:int) : seq<seq<int>>
  requires |sequ| >= seg_length >= 0
   decreases sequ 
  {
    if |sequ| == 0 then [] //if the list is empty
    else if |sequ|-1 < seg_length then [sequ[0..seg_length]] //if the list cannot have any more segments
    else [sequ[0..seg_length]]+produce_segments(sequ[1..],seg_length)
  }

function method segment_LeftMoreSegmentRight (sequ:seq<int>) : bool
  {
    if (Count(x => x >= 0,sequ[0..|sequ|/2])) >= (Count(x => x >= 0,sequ[|sequ|/2..|sequ|])) then true
    else false
  }

现在，这个方法是这样工作的：

1. 我们初始化一个长度为 k 的数组，其中我们已经计算了左侧和右侧的所有正数。
2. 现在，从 k 开始，在每次迭代中，我们将在每一侧增加、减少或保留相同数量的正数：例如，如果 v[i]>=0 那么我们将右边的正数加 1 （而且，显然，如果它是正数，我们会在 v[i-k/2] 中递减这个数字）。
3. 为了计算这一点，我们定义了一个谓词，该谓词告诉我们右侧的正数数量是否高于或等于左侧的数量。

//returns if the number of positives left is higher than the right or not
function method segmentL_isMore_right (pos_left:int,pos_right:int) : bool
  {
    if pos_left>=pos_right then true
    else false
  }
 
 method initialize(sequ:seq<int>,seg_length:int) returns (sequ_new:seq<int>,pos_left: int,pos_right:int)
  requires |sequ| >= seg_length >= 0
{
  var length := |sequ|;
  var pos_left_local := 0;
  var pos_right_local :=0;
  var i:=0;
  while i<(length/2) 
  {
    if sequ[i]>=1 {pos_left_local:=pos_left_local+1;}
    i:=i+1;
  }
  while i<(length) 
  {
    if sequ[i]>=1 {pos_right_local:=pos_right_local+1;}
    i:=i+1;
  }
  
  return sequ[0..],pos_left_local,pos_right_local;
}

//Linear implementation

method Count_linear(sequ:seq<int>,seg_length:int) returns (num_segmts: int)
  requires |sequ| >= seg_length >= 0
  ensures num_segmts == Count(segment_LeftMoreSegmentRight,produce_segments(sequ,seg_length));
{
  var num_segmts_local := 0;
  var new_seq,pos_right_local := initialize(sequ,seg_length);
  var i:=seg_length+1;
  while i<|sequ| 
    decreases |sequ|-i
  {
    if (sequ[i] >=0) {pos_right_local:=pos_right_local+1;}
    if (sequ[i-seg_length]>=0) {pos_left_local:=pos_left_local+1;}
    if (sequ[i-seg_length]/2>=0) 
        {
        pos_right_local:=pos_right_local-1;
        pos_left_local:=pos_left_local+1;
        }
    i:=i+1;
    if segmentL_isMore_right (pos_left_local,pos_right_local) 
      {
        num_segmts_local:=num_segmts_local+1;
      }
  }
  return num_segmts_local;
}


\\if want to prove it:
method Main()
{
  var aseq := [1,3,4,5,6,7,8,9,10];
  var seg2_leftRight := Count(segment_LeftMoreSegmentRight,produce_segments(aseq,4)); //high order and polymorphic
}

现在，关键是 ensures num_segmts == Count(segment_LeftMoreSegmentRight,seg_length)); 没有验证。显然，我将不得不证明一些关于 Count 或 Count_linear 的引理性质，但不知道从哪里开始这个问题。

有什么帮助吗？我希望我已经尽可能最好地解释了这个问题。

解决方法

我把这个作为一个答案，这样我就可以获得很好的代码格式。

您的 Count_linear 有错误。

  var aseq := [1,2,3,4,5,6,7,8,9,10];
  var slow := Count(segment_LeftMoreSegmentRight,produce_segments(aseq,4)); //high order and polymorphic
  var fast := Count_linear(aseq,4);
  print slow,"\n";
  print fast,"\n";

印刷品

7
5