Нарушение утверждения Dafny-recursiveSum

Я попытался написать рекурсивную функцию суммы в 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);

}

СУММ1:

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);
}

СУММ2:

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

Пожалуйста, помогите мне понять, почему?


recursion formal-verification dafny
person greenity    schedule 12.12.2015    source источник
comment
пожалуйста, создайте версию кода, которую можно скопировать и вставить в rise4fun.com/Dafny   -  person lexicalscope    schedule 14.12.2015

Ответы (1)


arrow_upward
0
arrow_downward

Я не понимаю, почему это утверждение должно быть верным:

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

Я думаю, проблема в том, что ваше рекурсивное определение суммы суммирует массив с конца, а ваша итеративная версия суммирует его с самого начала. Вот доказательство чего-то похожего на ваше:

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;
  }
}
person lexicalscope    schedule 13.12.2015