
This piece of code partition an array cond[], putting positive values into a[] and negative values into b[]. But Dafny cannot verify it. Interestingly, if the line b[k]:=cond[i] is commented, everything goes fine. So if it is changed to b[k]:=3;.
I am wondering what's wrong with it. Thanks!
method conditional_copy(a:array<int>,cond:array<int>,b:array<int>)returns(j:int,k:int)
requires a!=null&&cond!=null&&b!=null;
requires a.Length>0&&cond.Length==a.Length&&b.Length==a.Length;
modifies a,b;
ensures 0<=j<=a.Length;
ensures 0<=k<=b.Length;
ensures forall m::0<=m<j==>a[m]>=0;
{
var i:=0;
j:=0;
k:=0;
while(i<cond.Length&&j<a.Length&&k<b.Length)
invariant 0<=j<=a.Length;
invariant 0<=k<=b.Length;
invariant forall m::0<=m<j==>a[m]>=0;
//invariant forall m::0<=m<k==>a[m]<0;
{
if(cond[i]>=0){
assert cond[i]>=0;
a[j] := cond[i];
assert forall m::0<=m<=j==>a[m]>=0;
j:=j+1;
assert forall m::0<=m<j==>a[m]>=0;
}
else{
assert forall m::0<=m<j==>a[m]>=0;
b[k]:=cond[i]; //*
//b[k] := 5;
assert forall m::0<=m<j==>a[m]>=0;
k := k+1;
}
assert forall m::0<=m<j==>a[m]>=0;
i := i+1;
}
}



What if a aliases b?



What does that mean?


Jul 14, 2014 at 9:06 AM
Edited Jul 14, 2014 at 9:07 AM

remijohn wrote:
What does that mean?
An alias is when the same piece of memory is pointed to by more than one name. In this case, your method parameters a and b could refer to the same array.
e.g
...
var x ...
...
conditional_copy(x,cond,x)
If the method is called this way, then both sides of your conditional will be updating the same array  so your method postcondition is incorrect. 'a' can indeed have both values less than and greater than zero.
Probably your method needs a precondition that requires a and b to point to different arrays (a!=b)



That works! Thank you very much!
I've never think about this before.
I'm wondering is there something like separation logic to allow heap reasoning in Dafny?






Thanks a lot!

