
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.



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.



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.



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] == []
}



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] == []
}

