Consider these two methods. Are they the same or different?

    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;
    }

Not only do these methods have different code; they actually have different behavior:

But when val occurs at exactly one index of the array, the two methods behave the same.

To make it possible to substitute one implementation for another, we need a specification:

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