package java.lang;

public class String{
  public String(byte[] src);
    //@ requires src != null;
    //@ ensures true;

  public boolean equals(String other);
    //@ requires true;
    //@ ensures true;
  public int indexOf(String other);
    //@ requires true;
    //@ ensures result>=(-1);
  public String substring(int begin,int end);
    //@ requires begin>=0;
    //@ ensures result!=null;
  public int length();
    //@ requires true;
    //@ ensures result>=0;
  public boolean matches(String regex);
    //@ requires true;
    //@ ensures true;
  public static String valueOf(int value);
    //@ requires true;
    //@ ensures true;
}