Dafny-recursiveSum 断言违规

Question

我尝试在dafny中写了一个递归求和函数并证明了它的正确性。我写了：

method Main() {
var a: array<int> := new int[4];
a[0] := 7;
a[1] := -2;
a[2] := 3;
a[3] := -2;
assert a[..] == [7,-2,3,-2];

var s/*, p, c */:= Sum(a, -2);
assert a[0] == 7 && a[1] == -2 && a[2] == 3 && a[3] == -2;
assert s == RecursiveSum(a, 0); // == 6
print "\nThe sum of all elements in [7,-2,3,-2] is ";
print s;
}

function RecursiveSum(a: array<int>, from: nat) : int
reads a
requires a != null
requires from <= a.Length
decreases a.Length-from
{
if from == a.Length then 0
else a[from] + RecursiveSum(a, from+1)
}

这是我写的证明:

method Sum(a: array<int>, key: int) returns (s: int)
requires a != null
ensures s == RecursiveSum(a, 0)

{   
// Introduce local variable (6.1)
var i : nat; //frame s ,i
s,i:=sum1(a);
// Strengthen post condition (1.1)
assert i== a.Length && s == RecursiveSum(a,0);

}

SUM1:

method sum1(a: array<int>) returns (s : int, i : nat)
requires a != null
ensures  i== a.Length && s == RecursiveSum(a,0);
{
assert  RecursiveSum(a,a.Length)==0 ;
//  Assignment (1.3)
s,i:=0,0;
assert  0 <= i <= a.Length && s==RecursiveSum(a,i) ;

// Iteration (5.5)
while (i != a.Length)
  invariant  0 <= i <= a.Length && s==RecursiveSum(a,i) ;
decreases  a.Length-i ;
{
assert 0 <= i <=a.Length && RecursiveSum(a,i)==s && i!=a.Length  ;
    s, i := Sum2(s, a, i);
}
assert i== a.Length && s == RecursiveSum(a,0);
}

SUM2:

method Sum2(s0 : int, a: array<int>, i0 : nat) returns (s : int, i : nat)
requires a != null
requires 0 <= i0 <= a.Length && RecursiveSum(a,i0)==s0 && i0 != a.Length;
ensures RecursiveSum(a,0)==s && 0 <= i <= a.Length;
{
// Assignment (1.3)
s, i := s0, i0;
// Contract frame (5.4)
assert 0 <= i0 <= a.Length && RecursiveSum(a,i0)==s0 && RecursiveSum(a,i0+1)==s0+a[i] ;
// leading assignment (8.5)
s := s0 + a[i];
assert 0 <= i0 <= a.Length && RecursiveSum(a,i0)==s0 && RecursiveSum(a,i0+1)==s0+a[i] ;
i := i + 1;
assert  0 <= i <=a.Length && RecursiveSum(a,0)==s && 0 <= a.Length-i < a.Length-i0 ;
}

我得到的错误：

stdin.dfy(75,32): Error: assertion violation 
stdin.dfy(78,1): Error: decreases expression might not decrease
stdin.dfy(79,37): Error BP5005: This loop invariant might not be maintained   by the loop.
stdin.dfy(96,77): Error: assertion violation
 stdin.dfy(101,47): Error: assertion violation

请帮我理解为什么？

Answer 1

我不明白为什么这个断言应该成立：

s,i:=0,0;
assert  0 <= i <= a.Length && s==RecursiveSum(a,i);

您将变量 s 和 i 设置为 0，然后您说 s==RecursiveSum(a,i)。好吧，如果 a 是数组 [1,2]，那么 RecursiveSum([1,2],0)==3

我认为问题在于你的 sum 递归定义是从末尾对数组求和，而你的迭代版本是从头开始求和。这是与您类似的证明：

method Main() {
var a: array<int> := new int[4];
a[0] := 7;
a[1] := -2;
a[2] := 3;
a[3] := -2;
assert a[..] == [7,-2,3,-2];

var s/*, p, c */:= Sum(a, -2);
assert a[0] == 7 && a[1] == -2 && a[2] == 3 && a[3] == -2;
assert s == RecursiveSum(a, 0); // == 6
print "\nThe sum of all elements in [7,-2,3,-2] is ";
print s;
}

function RecursiveSum(a: array<int>, from: nat) : int
reads a
requires a != null
requires from <= a.Length
decreases a.Length-from
{
if from == a.Length then 0
else a[from] + RecursiveSum(a, from+1)
}

method Sum(a: array<int>, key: int) returns (s: int)
requires a != null
ensures s == RecursiveSum(a, 0)
{   
  var i : nat;
  s,i:=sum1(a);
  assert i == 0 && s == RecursiveSum(a,0);
}

method sum1(a: array<int>) returns (s : int, i : nat)
requires a != null
ensures  i == 0 && s == RecursiveSum(a,0);
{
  assert  RecursiveSum(a,a.Length)==0 ;
  s,i:=0,a.Length;
  assert s==RecursiveSum(a,i);

  while (i > 0)
    invariant  0 <= i <= a.Length && s==RecursiveSum(a,i) ;
    decreases  i;
  {
    s, i := Sum2(s, a, i);
  }
  assert i == 0 && s == RecursiveSum(a,0);
}

method Sum2(s0 : int, a: array<int>, i0 : nat) returns (s : int, i : nat)
requires a != null
requires 0 < i0 <= a.Length && RecursiveSum(a,i0)==s0;
ensures i == i0-1 && RecursiveSum(a,i)==s;
{
s, i := s0 + a[i0-1], i0-1;
}

或者你可以这样做：

 method Main() {
  var a: array<int> := new int[4];
  a[0] := 7;
  a[1] := -2;
  a[2] := 3;
  a[3] := -2;
  assert a[..] == [7,-2,3,-2];

  var s/*, p, c */:= Sum(a, -2);
  assert a[0] == 7 && a[1] == -2 && a[2] == 3 && a[3] == -2;
  assert s == RecursiveSum(a, a.Length);
  print "\nThe sum of all elements in [7,-2,3,-2] is ";
  print s;
}

function RecursiveSum(a: array<int>, to: nat) : int
  reads a
  requires a != null
  requires to <= a.Length
{
  if to == 0 then 0
  else a[to-1] + RecursiveSum(a, to-1)
}


method Sum(a: array<int>, key: int) returns (s: int)
  requires a != null
  ensures s == RecursiveSum(a, a.Length)
{   
  s := 0;
  var i : nat := 0;
  while (i < a.Length)
    invariant  0 <= i <= a.Length && s==RecursiveSum(a,i) ;
  {
    s, i := s+a[i], i+1;
  }
}

Dafny-recursiveSum 断言违规

Dafny-recursiveSum assertion violation

recursion

formal-verification

dafny