public class McCarthy {
    /*@ normal_behavior
      @ ensures (x > 100 ==> \result == x - 10) && (x <= 100 ==> \result == 91);
      @ assignable \nothing;
      @*/
    public int f(int x) {
	if (x > 100)
	    return x - 10;
	else
	    return f(f(x+11));
    }
}