(Dafny) Ajout d'éléments d'un tableau dans une autre boucle - invariant

Question

I ont une fonction qui prend sum deux réseaux a et b comme entrées et modifie de telle sorte que bb[i] = a[0] + a[1] + ... + a[i]. J'ai écrit cette fonction et je veux la vérifier avec Dafny. Cependant, Dafny me dit que mon invariant de boucle pourrait ne pas être maintenu par la boucle. Voici le 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; 
    } 
} 

Comment réparer cette erreur?

Answer 1

Votre programme ne serait pas correct si a et b référencent le même tableau. Vous avez besoin de la condition préalable a != b. (Si vous l'ajoutez, Dafny vérifiera votre programme.)

Rustan