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 System extends java.lang.Object
  {
     public final static java.io.InputStream in;
     public final static java.io.PrintStream out;
     public final static java.io.PrintStream err;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setIn(java.io.InputStream arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setOut(java.io.PrintStream arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setErr(java.io.PrintStream arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.io.Console console();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.nio.channels.Channel inheritedChannel() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setSecurityManager(java.lang.SecurityManager arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.SecurityManager getSecurityManager();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long currentTimeMillis();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long nanoTime();
  
     /*@ public normal_behavior 
       @ requires     src instanceof Object[]     // exclude ArrayStoreExceptions due to non-array type
       @          && dest instanceof Object[] // exclude ArrayStoreExceptions due to non-array type
       @          && srcPos >= 0 && srcPos + length <= ((Object[])src).length   // exclude IndexOutException
       @          && destPos >=0 && destPos + length <= ((Object[])dest).length // exclude IndexOutException
       @          && length >=0  // exclude IndexOutException
       @          && (\forall int i; srcPos<=i && i<srcPos + length; 
       @                  \dl_arrayStoreValid(dest, ((Object[])src)[i])); // exclude ArrayStoreExceptions due to non-assignable array element of a to dest
       @ ensures (\forall int i; 0<=i && i< length; ((Object[])dest)[destPos + i] == \old(((Object[])src)[srcPos+i])) ; 
       @ assignable ((Object[])dest)[destPos..destPos+length-1];
       @*/
      public static /*@ helper @*/ void arraycopy(java.lang.Object src, int srcPos, java.lang.Object dest, int destPos, int length);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int identityHashCode(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Properties getProperties();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String lineSeparator();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setProperties(java.util.Properties arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String getProperty(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String getProperty(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String setProperty(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String clearProperty(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String getenv(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Map getenv();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void exit(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void gc();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void runFinalization();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void runFinalizersOnExit(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void load(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void loadLibrary(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String mapLibraryName(java.lang.String arg0);
  }
  