Behavioral Equivalence

static int findA (int [] a, int val) {
  for (int i = 0; i < a.length; i++) {
    if (a[i] == val)
      return i;
  }
  return a.length;
}

static int findB (int [] a, int val) {
  for (int i = a.length -1 ; i >= 0; i--) {
    if (a[i] == val) return i;
  }
  return -1;
}   

• Are these behaviorally equivalent?
• Not really They differ when val is either missing or appears more than once.
• Still, it depends on the specification. They would be equivalent if the specification was:

  requires: val occurs in a 
  effects: returns result such that a[result] = val