（Dafny）添加一個數組中的元素到另一個 - 循環不變

Question

我有一個函數sum採用兩個陣列a和b作爲輸入並修改b使得b[i] = a[0] + a[1] + ... + a[i]。我寫了這個函數，想用Dafny來驗證它。但是，Dafny告訴我，我的循環不變可能不會被循環維護。這裏是代碼：

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

我該如何解決這個錯誤？

Answer 1

如果a和b引用相同的數組，您的程序將不正確。你需要預先條件a != b。 （如果添加它，Dafny會驗證你的程序。）

Rustan