Converting a method from VCC to Dafny

Jun 11, 2013 at 6:41 PM
I cannot get a Dafny compare array method to verify.

I want a method that will compare two integer arrays and return true if the two arrays are the same (i.e. if a1 = [0,1,2] and a2 = [0,1,2] then these two arrays are equal). There was a method in the VCC tutorial which does this:
typedef int BOOL;
#define TRUE 1
#define FALSE 0

// a function that takes two arrays and checks 
// whether the arrays are equal 
BOOL arrays_eq(int *p, int *q, unsigned len)
  _(requires \thread_local_array(p, len))
  _(requires \thread_local_array(q,len))
  _(ensures \result <==> (\forall unsigned i; 
      i < len ==> p[i] == q[i]))
  _(decreases 0)
{
  for (unsigned i = 0; i < len; i++)
    _(invariant \forall unsigned j; j < i 
      ==> p[j] == q[j])
    if (p[i] != q[i]) return FALSE;
  return TRUE;
}
I want to convert this from VCC to Dafny. I've attempted to convert this to Dafny with the following:
method array_eq(s1: array<int>, s2: array<int>) returns (same: bool) 
    requires s1 != null && s2 != null;
    //requires s1.Length == s2.Length;
    ensures same <==> forall i :: 0 <= i < s1.Length == s2.Length ==> s1[i] == s2[i];
    decreases 0;
{
    var i: int := 0;

    while ( i < s1.Length && i < s2.Length) 
        invariant same ==> forall j :: 0 <= j < i < s1.Length == s2.Length ==> s1[j] == s2[j];
        decreases s1.Length - i;
        decreases s2.Length - i;
    {
        if (s1[i] != s2[i]) { same := false; }
        i := i + 1;
    }

    same := true;
}
I can't get the Dafny method to verify, but the code verifies in VCC (it's straight from the VCC tutorial). Dafny gives an error at the post condition in which the post condition does not hold. Well, (with a laugh) it verifies in VCC. I mimicked VCC as much as possible and it doesn't verify. Why?

I have a feeling its something small, but since I've been at this for a week (on and off), and I might be over-thinking this. Any help is appreciated.
Jun 16, 2013 at 11:00 AM
The converted version is not the same as the Vcc Version. In your dafnyprogram the two array don`t have the same size. Check the following program, it´s a converted version of the vcc program.

http://rise4fun.com/Dafny/wMBrc
Jun 17, 2013 at 3:45 PM
Thank you :) I should have known it had something to do with the array lengths.