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 overthinking this. Any help is appreciated.
