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 Character extends java.lang.Object implements java.io.Serializable, java.lang.Comparable
  {
     public final static int MIN_RADIX = 2;
     public final static int MAX_RADIX = 36;
     public final static char MIN_VALUE = 0;
     public final static char MAX_VALUE = 65535;
     public final static java.lang.Class TYPE;
     public final static byte UNASSIGNED = 0;
     public final static byte UPPERCASE_LETTER = 1;
     public final static byte LOWERCASE_LETTER = 2;
     public final static byte TITLECASE_LETTER = 3;
     public final static byte MODIFIER_LETTER = 4;
     public final static byte OTHER_LETTER = 5;
     public final static byte NON_SPACING_MARK = 6;
     public final static byte ENCLOSING_MARK = 7;
     public final static byte COMBINING_SPACING_MARK = 8;
     public final static byte DECIMAL_DIGIT_NUMBER = 9;
     public final static byte LETTER_NUMBER = 10;
     public final static byte OTHER_NUMBER = 11;
     public final static byte SPACE_SEPARATOR = 12;
     public final static byte LINE_SEPARATOR = 13;
     public final static byte PARAGRAPH_SEPARATOR = 14;
     public final static byte CONTROL = 15;
     public final static byte FORMAT = 16;
     public final static byte PRIVATE_USE = 18;
     public final static byte SURROGATE = 19;
     public final static byte DASH_PUNCTUATION = 20;
     public final static byte START_PUNCTUATION = 21;
     public final static byte END_PUNCTUATION = 22;
     public final static byte CONNECTOR_PUNCTUATION = 23;
     public final static byte OTHER_PUNCTUATION = 24;
     public final static byte MATH_SYMBOL = 25;
     public final static byte CURRENCY_SYMBOL = 26;
     public final static byte MODIFIER_SYMBOL = 27;
     public final static byte OTHER_SYMBOL = 28;
     public final static byte INITIAL_QUOTE_PUNCTUATION = 29;
     public final static byte FINAL_QUOTE_PUNCTUATION = 30;
     final static int ERROR = -1;
     public final static byte DIRECTIONALITY_UNDEFINED = -1;
     public final static byte DIRECTIONALITY_LEFT_TO_RIGHT = 0;
     public final static byte DIRECTIONALITY_RIGHT_TO_LEFT = 1;
     public final static byte DIRECTIONALITY_RIGHT_TO_LEFT_ARABIC = 2;
     public final static byte DIRECTIONALITY_EUROPEAN_NUMBER = 3;
     public final static byte DIRECTIONALITY_EUROPEAN_NUMBER_SEPARATOR = 4;
     public final static byte DIRECTIONALITY_EUROPEAN_NUMBER_TERMINATOR = 5;
     public final static byte DIRECTIONALITY_ARABIC_NUMBER = 6;
     public final static byte DIRECTIONALITY_COMMON_NUMBER_SEPARATOR = 7;
     public final static byte DIRECTIONALITY_NONSPACING_MARK = 8;
     public final static byte DIRECTIONALITY_BOUNDARY_NEUTRAL = 9;
     public final static byte DIRECTIONALITY_PARAGRAPH_SEPARATOR = 10;
     public final static byte DIRECTIONALITY_SEGMENT_SEPARATOR = 11;
     public final static byte DIRECTIONALITY_WHITESPACE = 12;
     public final static byte DIRECTIONALITY_OTHER_NEUTRALS = 13;
     public final static byte DIRECTIONALITY_LEFT_TO_RIGHT_EMBEDDING = 14;
     public final static byte DIRECTIONALITY_LEFT_TO_RIGHT_OVERRIDE = 15;
     public final static byte DIRECTIONALITY_RIGHT_TO_LEFT_EMBEDDING = 16;
     public final static byte DIRECTIONALITY_RIGHT_TO_LEFT_OVERRIDE = 17;
     public final static byte DIRECTIONALITY_POP_DIRECTIONAL_FORMAT = 18;
     public final static char MIN_HIGH_SURROGATE = 55296;
     public final static char MAX_HIGH_SURROGATE = 56319;
     public final static char MIN_LOW_SURROGATE = 56320;
     public final static char MAX_LOW_SURROGATE = 57343;
     public final static char MIN_SURROGATE = 55296;
     public final static char MAX_SURROGATE = 57343;
     public final static int MIN_SUPPLEMENTARY_CODE_POINT = 65536;
     public final static int MIN_CODE_POINT = 0;
     public final static int MAX_CODE_POINT = 1114111;
     public final static int SIZE = 16;
     final static boolean $assertionsDisabled;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public Character(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.Character valueOf(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public char charValue();
  
     /*@ 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; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String toString(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isValidCodePoint(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isBmpCodePoint(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSupplementaryCodePoint(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isHighSurrogate(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLowSurrogate(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSurrogate(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSurrogatePair(char arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int charCount(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int toCodePoint(char arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointAt(java.lang.CharSequence arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointAt(char[] arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointAt(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointBefore(java.lang.CharSequence arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointBefore(char[] arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointBefore(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char highSurrogate(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char lowSurrogate(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int toChars(int arg0, char[] arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char[] toChars(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointCount(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int codePointCount(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int offsetByCodePoints(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int offsetByCodePoints(char[] arg0, int arg1, int arg2, int arg3, int arg4);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLowerCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLowerCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUpperCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUpperCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isTitleCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isTitleCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isDigit(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isDigit(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isDefined(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isDefined(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLetter(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLetter(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLetterOrDigit(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isLetterOrDigit(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaLetter(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaLetterOrDigit(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isAlphabetic(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isIdeographic(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaIdentifierStart(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaIdentifierStart(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaIdentifierPart(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isJavaIdentifierPart(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUnicodeIdentifierStart(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUnicodeIdentifierStart(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUnicodeIdentifierPart(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isUnicodeIdentifierPart(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isIdentifierIgnorable(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isIdentifierIgnorable(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char toLowerCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int toLowerCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char toUpperCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int toUpperCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char toTitleCase(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int toTitleCase(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int digit(char arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int digit(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getNumericValue(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getNumericValue(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSpace(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSpaceChar(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isSpaceChar(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isWhitespace(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isWhitespace(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isISOControl(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isISOControl(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getType(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int getType(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char forDigit(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static byte getDirectionality(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static byte getDirectionality(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isMirrored(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static boolean isMirrored(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Character arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static int compare(char arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static char reverseBytes(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String getName(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  