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 final class Math extends java.lang.Object
  {
     public final static double E = 2.718281828459045;
     public final static double PI = 3.141592653589793;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double sin(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double cos(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double tan(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double asin(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double acos(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double atan(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double toRadians(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double toDegrees(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double exp(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double log(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double log10(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double sqrt(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double cbrt(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double IEEEremainder(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double ceil(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double floor(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double rint(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double atan2(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double pow(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int round(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long round(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double random();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int abs(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long abs(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float abs(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double abs(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int max(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long max(long arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float max(float arg0, float arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double max(double arg0, double arg1);
  
     /*@ public normal_behaviour 
       @ requires true; 
       @ ensures \result == (arg0 <= arg1 ? arg0 : arg1); 
       @ assignable \strictly_nothing;
       @*/
     public static int min(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long min(long arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float min(float arg0, float arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double min(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double ulp(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float ulp(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double signum(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float signum(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double sinh(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double cosh(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double tanh(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double hypot(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double expm1(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double log1p(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double copySign(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float copySign(float arg0, float arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getExponent(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getExponent(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double nextAfter(double arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float nextAfter(float arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double nextUp(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float nextUp(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static double scalb(double arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static float scalb(float arg0, int arg1);
  }
  