(Dafny) Hinzufügen von Elementen eines Arrays in einem anderen - Schleifeninvariante

Question

I haben eine Funktion, die zwei Arrays suma und b als Eingaben nimmt und modifiziert, so daß bb[i] = a[0] + a[1] + ... + a[i]. Ich habe diese Funktion geschrieben und möchte das mit Dafny überprüfen. Dafny teilt mir jedoch mit, dass meine Schleifeninvariante möglicherweise nicht von der Schleife verwaltet wird. Hier ist der Code:

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

method sum(a:array<int>, b:array<int>) 
    requires a != null && b != null 
    requires a.Length >= 1 
    requires a.Length == b.Length 
    modifies b 
    ensures forall x | 0 <= x < b.Length :: b[x] == sumTo(a,x) 
{ 
    b[0] := a[0]; 
    var i := 1; 

    while i < b.Length 
     invariant b[0] == sumTo(a,0) 
     invariant 1 <= i <= b.Length 

     //ERROR : invariant might not be maintained by the loop. 
     invariant forall x | 1 <= x < i :: b[x] == sumTo(a,x) 

     decreases b.Length - i 
    { 
     b[i] := a[i] + b[i-1]; 
     i := i + 1; 
    } 
} 

Wie kann ich diesen Fehler beheben?

Answer 1

Ihr Programm wäre nicht korrekt, wenn a und b das gleiche Array referenzieren. Sie benötigen die Vorbedingung a != b. (Wenn Sie es hinzufügen, wird Dafny Ihr Programm überprüfen.)

Rustan