Problems of array partition

Jul 11, 2014 at 7:57 AM
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;
  }      
}
Jul 11, 2014 at 11:32 AM
What if a aliases b?
Jul 14, 2014 at 7:19 AM
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)
Marked as answer by remijohn on 7/14/2014 at 4:32 AM
Jul 14, 2014 at 11:32 AM
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?
Jul 14, 2014 at 12:43 PM
Umm, I think Dafny is based on Dynamic Frames. For example the "modifies" clause you have in your example is part of Dafny's heap reasoning facilities. Perhaps looking at some of the examples that come with Dafny will help clarify this:

http://dafny.codeplex.com/SourceControl/latest#Test/dafny1/SeparationLogicList.dfy
Jul 14, 2014 at 11:40 PM
Thanks a lot!