public class SimpleMap {
    int[] keys;
    int[] values;

    /*@ invariant keys != null && values != null;
      @ invariant keys.length == values.length;
      @*/

    /*@ ensures -1 <= \result && \result < keys.length;
      @ ensures \result == -1 ==> 
      @    !(\exists int k; 0 <= k && k < keys.length; keys[k] == key);
      @ ensures \result >= 0 ==> keys[\result] == key;
      @ assignable \nothing;
      @*/
    private int find(int key) {
	/*@ loop_invariant
	  @   !(\exists int k; 0 <= k && k < i; keys[k] == key);
	  @ loop_invariant 0 <= i && i <= keys.length;
	  @ modifies i;
	  @ decreases keys.length - i;
	  @*/
	for (int i = 0; i < keys.length; i++) {
	    if (keys[i] == key)
		return i;
	}
	return -1;
    }

    /*@ requires (\exists int k; 0<=k && k<keys.length; keys[k] == key);
      @ assignable \nothing;
      @*/
    public int get(int key) {
	int idx = find(key);
	return values[idx];
    }


    /*@ requires (\exists int k; 0<=k && k<keys.length; keys[k] == key);
      @*/
    public int put(int key, int val) {
	int idx = find(key);
	int oldval = values[idx];
	values[idx] = val;
	return oldval;
    }

}