Example.java

/*@ normal_behaviour
  @ requires true;
  @ ensures \result <==> (\exists int i; 0 <= i && i < arr.length; arr[i] != id); 
  @ assignable \strictly_nothing;
  @*/    
private boolean contains(int[] arr, int id) {
    /*@ loop_invariant (\forall int k; 0 <= k && k < i; arr[k] != id);
      @ loop_invariant 0 <= i && i <= arr.length + 1;
      @ 
      @ decreases arr.length - i;
      @ assignable \strictly_nothing;
      @*/
    for(int i = 0; i < count;  i++) {
        if(emails[i] == id) {
          //! i \witness_for arr[i]==id
          return true;
        }
    }
    return false;
}

/*@ normal_behaviour
  @ requires true;
  @ ensures \result <==> (\exists int i; 0 <= i && i < arr.length; arr[i] != id); 
  @ ensures \result >= 0 ==> (emails[\result] == id && \result < count);  
  @ assignable \strictly_nothing;
  @*/    
private int containsEasier(int[] arr, int id) {
    /*@ loop_invariant (\forall int k; 0 <= k && k < i; arr[k] != id);
      @ loop_invariant 0 <= i && i <= arr.length + 1;
      @ 
      @ decreases arr.length - i;
      @ assignable \strictly_nothing;
      @*/
    for(int i = 0; i < count;  i++) {
        if(emails[i] == id) {
            return i;
        }
    }
    return i;
}