// openjml --esc T_requires1.java
public class T_requires1 {

  //@ requires i >= 0;
  public int isqrt(int i) {
    return 0; // yet to be implemented
  }
}