content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.lang;
  
  public class Object
  {
  
     public /*@ pure @*/ Object() { }
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.Class getClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.CloneNotSupportedException e) true; */
     protected java.lang.Object clone() throws java.lang.CloneNotSupportedException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final void notify();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final void notifyAll();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public final void wait(long arg0) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public final void wait(long arg0, int arg1) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public final void wait() throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.Throwable e) true; */
     protected void finalize() throws java.lang.Throwable;
  }
  