content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio.charset;
  
  public abstract class Charset extends java.lang.Object implements java.lang.Comparable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSupported(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.charset.Charset forName(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.SortedMap availableCharsets();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.charset.Charset defaultCharset();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected Charset(java.lang.String arg0, java.lang.String[] arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String name();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.util.Set aliases();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String displayName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean isRegistered();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String displayName(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean contains(java.nio.charset.Charset arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.charset.CharsetDecoder newDecoder();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.charset.CharsetEncoder newEncoder();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean canEncode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.CharBuffer decode(java.nio.ByteBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.ByteBuffer encode(java.nio.CharBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.ByteBuffer encode(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int compareTo(java.nio.charset.Charset arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  