CODEWITHSUNDEEP
arraysloop-invariantdafny
Dory
Dory

Reputation: 139

(Dafny) Adding elements of an array into another - loop invariant

I have a function sum that takes two arrays a and b as inputs and modifies b such that b[i] = a[0] + a[1] + ... + a[i]. I wrote this function and want to verify it with Dafny. However, Dafny tells me that my loop invariant might not be maintainted by the loop. Here is the 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;
    }
}

How can I fix this error?

Upvotes: 4

Views: 2053

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

Your program would not be correct if a and b reference the same array. You need the precondition a != b. (If you add it, Dafny will verify your program.)

Rustan

Upvotes: 4

Related Questions