CODEWITHSUNDEEP
dafny
Jamal
Jamal

Reputation: 13

Dafny - Loop invariant for nested loops

I am trying to create a Dafny program that returns true if and only if, A contains no duplicates.

This is what I have so far, however the invariant invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]); says that it will not hold on entry.

Any advice on what I am doing wrong?

`method CheckArr1(A: array<int>) returns (r: bool)
requires A.Length > 0
ensures r <==> (forall i, j :: 0 <= i < A.Length && 0 <= j < A.Length && i != j ==> A[i] != A[j]);
{
    var i := 0;
    r := true;
    while i < A.Length 
    decreases A.Length - i;
    invariant i <= A.Length;
    invariant r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]);
    {
        var j := 0;
        while j < i
        decreases i - j;
        invariant j <= i;
        invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]);
        {
            r := (r && (A[j] != A[i]));
            j := j + 1;
        }
        i := i + 1;
    }
}`

Upvotes: 1

Views: 935

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

The "invariant doesn't hold on entry" error is for the declared invariant

r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i])

of the inner loop. On entry to the that loop, j is 0, so the condition that needs to hold on entry to the inner loop is

r <==> (0 <= 0 < i && 0 != i ==> A[0] != A[i])

which we can simplify to

r <==> (0 < i ==> A[0] != A[i])           // (*)

There is no reason to believe that r will hold this value on entry to the inner loop. All you know inside the body of the outer loop is that 

r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]) // (**)

which says that r tells you whether or not there are any duplicates within the first i elements. Condition (*) says something about a[i], whereas (**) does not say anything about a[i].

From your current program, it would be easier if you changed the inner loop to use a different variable, say s, to achieve the invariant you have given. That is, use the invariant

s <==> (forall j :: 0 <= j < i ==> A[j] != A[i])

Then, after the inner loop, update r using the value you computed for s.

Upvotes: 2

Related Questions