/*@ requires \valid_range(p,0,n-1);
    requires \valid_range(q,0,n-1);
    requires n >= 0 ;
    ensures    
      (\forall integer i ; 0 <= i < n ==> p[i] == q[i]) 
             ==> 
          \result == 1;
    ensures 
      !(\forall integer i ; (0 <= i < n) ==> (p[i] == q[i])) 
             ==> 
          \result == 0 ;
*/
int compare_arrays(int *p, int *q, int n)
{
  int i;
  /*@ loop invariant 0 <= i <= n ;
      loop invariant 
        \forall integer j; (0 <= j < i) ==> p[j] == q[j] ;
      loop variant n - i ;
 */
  for (i = 0; i < n; i++)
    if (p[i] != q[i]) return 0;
  return 1;
}