content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.util.concurrent;
  
  public abstract class TimeUnit extends java.lang.Enum
  {
     public final static java.util.concurrent.TimeUnit NANOSECONDS;
     public final static java.util.concurrent.TimeUnit MICROSECONDS;
     public final static java.util.concurrent.TimeUnit MILLISECONDS;
     public final static java.util.concurrent.TimeUnit SECONDS;
     public final static java.util.concurrent.TimeUnit MINUTES;
     public final static java.util.concurrent.TimeUnit HOURS;
     public final static java.util.concurrent.TimeUnit DAYS;
     final static long C0 = 1L;
     final static long C1 = 1000L;
     final static long C2 = 1000000L;
     final static long C3 = 1000000000L;
     final static long C4 = 60000000000L;
     final static long C5 = 3600000000000L;
     final static long C6 = 86400000000000L;
     final static long MAX = 9223372036854775807L;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.concurrent.TimeUnit[] values();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.concurrent.TimeUnit valueOf(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long convert(long arg0, java.util.concurrent.TimeUnit arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toNanos(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toMicros(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toMillis(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toSeconds(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toMinutes(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toHours(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toDays(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public void timedWait(java.lang.Object arg0, long arg1) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public void timedJoin(java.lang.Thread arg0, long arg1) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public void sleep(long arg0) throws java.lang.InterruptedException;
  }
  