Doubts in proving loop invariants

Dec 1, 2015 at 8:01 PM
Hi I am new to Dafny and trying to prove this basic invariant but Dafny is not to able verify this.
method Main(){

    var servers : seq<int>;

    var numServers := 10;

    servers := [];

    assert |servers| == 0;

    var index := 0;

            /**
                I am trying to populate the sequence and checking
               the  bounds on the size of the sequence on each iteration.
           **/
    while(index <  numServers)
    invariant 0 <= index <= numServers
    invariant 0 <= |servers| <= numServers --> this invariant is failing.
    {

        servers := servers + [index];
        index := index +1;
    }
}

Can anyone help what may be wrong in the above code snippet. When I keep the debug statements it seems fine but I am not sure what I am missing.
Dec 1, 2015 at 8:18 PM

I would guess that you also need:

```
invariant |servers|==index
```

or similar. Otherwise the length of servers could be taken to be 10, whilst index is taken to be 9. Which, I think, is why your invariant fails.

Dec 5, 2015 at 10:42 PM
Thanks a lot :)
Dec 6, 2015 at 12:51 AM
Edited Dec 6, 2015 at 12:54 AM
Hi,

I am facing issue proving one more loop invariant

class LearnInvariants
{
 method testInvariants(){

        var numServers;
        var serverChannel := new seq<int>[numServers,numServers];
        var serverId := 0;


        var temp;

        while serverId < numServers
            invariant 0 <= serverId <= numServers 
                                    --> Dafny is able to prove this
            invariant forall index_1 :: 0 <= index_1 < serverId <= numServers ==> 
            forall index_2 :: 0 <= index_2 < numServers ==> |serverChannel[index_1,index_2]| == 0;
                                            --> Dafny is not able to prove this invariant.
            {
                temp := 0;
                while temp < numServers
                    invariant 0 <= temp <= numServers
                                    --> Dafny is able to prove this
  invariant forall index_2 :: 0 <= index_2 < temp <= numServers ==> |serverChannel[serverId,index_2]| == 0 
                                                                --> This invariant was successful.
                    {

                        serverChannel[serverId,temp] := [];
                        assert |serverChannel[serverId,temp]| == 0;
                        temp := temp+1;
                    }

                serverId := serverId + 1;
            }
        }
}

In the above the program I am just initializing the two dimensional sequence of integers with a blank sequence. I am checking that the length of that sequence is zero.
Dafny is complaining that the invariant is not maintained by the loop. Can any one let me know what might me the issue in the above code snippet.
Dec 8, 2015 at 12:04 AM
The invariant of the inner loop is not strong enough. The invariant doesn't say that the inner loop leaves earlier rows of your matrix unmodified. Dafny does not inspect the body of the inner loop when proving the invariant of the outer loop. It only uses the inner loop invariant and the negation of the loop condition. You can delete the body or comment out the body of the inner loop. So Dafny does not know what the inner loop doesn't do unless you write it in the inner loop invariant.

Here is a version that verifies. I have noticed that creating appropriately named predicates for the importaint invariants helps me to more easily see the relationship between the different steps of the proof.

http://rise4fun.com/Dafny/Z9UU
method testInvariants(numServers:int)
  requires numServers >= 0;
{
        var serverChannel := new seq<int>[numServers,numServers];

        var i := 0;
        while i < numServers
            invariant 0 <= i <= numServers 
            invariant emptyChannels(serverChannel,i,numServers)
            {
                var j := 0;
                while j < numServers
                    invariant 0 <= j <= numServers
                    invariant emptyChannels(serverChannel,i+1,j) 
                    {
                        serverChannel[i,j] := [];
                        j := j+1;
                    }
                i := i + 1;
            }
        }
        
        predicate emptyChannels(serverChannel:array2<seq<int>>, i:int, j:int)
            requires serverChannel != null
            requires 0 <= i <= serverChannel.Length0
            requires 0 <= j <= serverChannel.Length1
        {
          forall x,y ::
                      0 <= x < i && 
                      0 <= y < j
                       ==> emptyChannel(serverChannel,x,y)
        }
        
        predicate emptyChannel(serverChannel:array2<seq<int>>, x:int, y:int)
            requires serverChannel != null
            requires 0 <= x < serverChannel.Length0
            requires 0 <= y < serverChannel.Length1
        {
          serverChannel[x,y] == []
        }
Dec 8, 2015 at 12:17 AM
By the way, there is another kind of "loop" in Dafny which doesn't require comlex invariants to achieve the same result. It is called the forall statement and I think of it as a kind of parallel for loop.

http://rise4fun.com/Dafny/n5x
method testInvariants(numServers:int) returns (serverChannel:array2<seq<int>>)
  requires numServers >= 0
  ensures serverChannel != null 
  ensures serverChannel.Length0 == serverChannel.Length1 == numServers 
  ensures emptyChannels(serverChannel,numServers,numServers)
{
  serverChannel := new seq<int>[numServers,numServers];
  forall i,j | 0 <= i < numServers && 0 <= j < numServers {
    serverChannel[i,j] := [];
  }
}
        
predicate emptyChannels(serverChannel:array2<seq<int>>, i:int, j:int)
  requires serverChannel != null
  requires 0 <= i <= serverChannel.Length0
  requires 0 <= j <= serverChannel.Length1
{
  forall x,y ::
    0 <= x < i && 0 <= y < j ==> emptyChannel(serverChannel,x,y)
}
        
predicate emptyChannel(serverChannel:array2<seq<int>>, x:int, y:int)
    requires serverChannel != null
    requires 0 <= x < serverChannel.Length0
    requires 0 <= y < serverChannel.Length1
{
  serverChannel[x,y] == []
}