（Dafny） - ループ不変

Question

Iは入力として二つの配列aとbを取り、bようb[i] = a[0] + a[1] + ... + a[i]を修正する機能sumを有しています。私はこの関数を書いて、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