java.lang
Class Character

java.lang.Object
  java.lang.Character

All Implemented Interfaces:

Comparable, Serializable

public final class Character

extends Object

implements Serializable, Comparable

JML's specification of java.lang.Character.

Version:

$Revision: 1.22 $

Author:

Curtis Clifton with help from the JML Seminar participants summer 1999., Gary T. Leavens

Class Specifications

public constraint this.ch_ == \old(this.ch_); public represents ch_ <- this.charValue();

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Comparable

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0); instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x))); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Nested Class Summary
static class	Character.Subset
static class	Character.UnicodeBlock

 

Model Field Summary
char	ch_

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
(package private) static char	CHAR_ERROR
static byte	COMBINING_SPACING_MARK
static byte	CONNECTOR_PUNCTUATION
static byte	CONTROL
static byte	CURRENCY_SYMBOL
static byte	DASH_PUNCTUATION
static byte	DECIMAL_DIGIT_NUMBER
static byte	DIRECTIONALITY_ARABIC_NUMBER
static byte	DIRECTIONALITY_BOUNDARY_NEUTRAL
static byte	DIRECTIONALITY_COMMON_NUMBER_SEPARATOR
static byte	DIRECTIONALITY_EUROPEAN_NUMBER
static byte	DIRECTIONALITY_EUROPEAN_NUMBER_SEPARATOR
static byte	DIRECTIONALITY_EUROPEAN_NUMBER_TERMINATOR
static byte	DIRECTIONALITY_LEFT_TO_RIGHT
static byte	DIRECTIONALITY_LEFT_TO_RIGHT_EMBEDDING
static byte	DIRECTIONALITY_LEFT_TO_RIGHT_OVERRIDE
static byte	DIRECTIONALITY_NONSPACING_MARK
static byte	DIRECTIONALITY_OTHER_NEUTRALS
static byte	DIRECTIONALITY_PARAGRAPH_SEPARATOR
static byte	DIRECTIONALITY_POP_DIRECTIONAL_FORMAT
static byte	DIRECTIONALITY_RIGHT_TO_LEFT
static byte	DIRECTIONALITY_RIGHT_TO_LEFT_ARABIC
static byte	DIRECTIONALITY_RIGHT_TO_LEFT_EMBEDDING
static byte	DIRECTIONALITY_RIGHT_TO_LEFT_OVERRIDE
static byte	DIRECTIONALITY_SEGMENT_SEPARATOR
static byte	DIRECTIONALITY_UNDEFINED
static byte	DIRECTIONALITY_WHITESPACE
static byte	ENCLOSING_MARK
static byte	END_PUNCTUATION
static byte	FINAL_QUOTE_PUNCTUATION
static byte	FORMAT
static byte	INITIAL_QUOTE_PUNCTUATION
static byte	LETTER_NUMBER
static byte	LINE_SEPARATOR
static byte	LOWERCASE_LETTER
static byte	MATH_SYMBOL
static int	MAX_RADIX
static char	MAX_VALUE
static int	MIN_RADIX
static char	MIN_VALUE
static byte	MODIFIER_LETTER
static byte	MODIFIER_SYMBOL
static byte	NON_SPACING_MARK
static byte	OTHER_LETTER
static byte	OTHER_NUMBER
static byte	OTHER_PUNCTUATION
static byte	OTHER_SYMBOL
static byte	PARAGRAPH_SEPARATOR
static byte	PRIVATE_USE
static byte	SPACE_SEPARATOR
static byte	START_PUNCTUATION
static byte	SURROGATE
static byte	TITLECASE_LETTER
static Class	TYPE
static byte	UNASSIGNED
static byte	UPPERCASE_LETTER

 

Constructor Summary

Character(char value)

 

Model Method Summary
static int	digitVal(char ch)

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
char	charValue()
int	compareTo(non_null Character anotherCharacter)
int	compareTo(non_null Object o)
static int	digit(char ch, int radix)
boolean	equals(nullable Object obj)
(package private) static int	findInCharMap(char ch)
static char	forDigit(int digit, int radix)
static byte	getDirectionality(char c)
static int	getNumericValue(char ch)
static int	getType(char ch)
int	hashCode()
static boolean	isDefined(char ch)
static boolean	isDigit(char ch)
static boolean	isIdentifierIgnorable(char ch)
static boolean	isISOControl(char ch)
static boolean	isJavaIdentifierPart(char ch)
static boolean	isJavaIdentifierStart(char ch)
static boolean	isJavaLetter(char ch)           Deprecated. Replaced by isJavaIdentifierStart(char).
static boolean	isJavaLetterOrDigit(char ch)           Deprecated. Replaced by isJavaIdentifierPart(char).
static boolean	isLetter(char ch)
static boolean	isLetterOrDigit(char ch)
static boolean	isLowerCase(char ch)
static boolean	isMirrored(char c)
static boolean	isSpace(char ch)           Deprecated. Replaced by isWhitespace(char).
static boolean	isSpaceChar(char ch)
static boolean	isTitleCase(char ch)
static boolean	isUnicodeIdentifierPart(char ch)
static boolean	isUnicodeIdentifierStart(char ch)
static boolean	isUpperCase(char ch)
static boolean	isWhitespace(char ch)
static char	toLowerCase(char ch)
String	toString()
static String	toString(char c)
static char	toTitleCase(char ch)
static char	toUpperCase(char ch)
(package private) static char[]	toUpperCaseCharArray(char ch)
(package private) static char	toUpperCaseEx(char ch)

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

 

Model Field Detail

ch_

public char ch_

MIN_RADIX

public static final int MIN_RADIX

MAX_RADIX

public static final int MAX_RADIX

MIN_VALUE

public static final char MIN_VALUE

MAX_VALUE

public static final char MAX_VALUE

TYPE

public static final Class TYPE

Specifications: non_null

UPPERCASE_LETTER

public static final byte UPPERCASE_LETTER

LOWERCASE_LETTER

public static final byte LOWERCASE_LETTER

TITLECASE_LETTER

public static final byte TITLECASE_LETTER

NON_SPACING_MARK

public static final byte NON_SPACING_MARK

COMBINING_SPACING_MARK

public static final byte COMBINING_SPACING_MARK

ENCLOSING_MARK

public static final byte ENCLOSING_MARK

DECIMAL_DIGIT_NUMBER

public static final byte DECIMAL_DIGIT_NUMBER

LETTER_NUMBER

public static final byte LETTER_NUMBER

OTHER_NUMBER

public static final byte OTHER_NUMBER

SPACE_SEPARATOR

public static final byte SPACE_SEPARATOR

LINE_SEPARATOR

public static final byte LINE_SEPARATOR

PARAGRAPH_SEPARATOR

public static final byte PARAGRAPH_SEPARATOR

CONTROL

public static final byte CONTROL

FORMAT

public static final byte FORMAT

SURROGATE

public static final byte SURROGATE

PRIVATE_USE

public static final byte PRIVATE_USE

UNASSIGNED

public static final byte UNASSIGNED

MODIFIER_LETTER

public static final byte MODIFIER_LETTER

OTHER_LETTER

public static final byte OTHER_LETTER

CONNECTOR_PUNCTUATION

public static final byte CONNECTOR_PUNCTUATION

DASH_PUNCTUATION

public static final byte DASH_PUNCTUATION

START_PUNCTUATION

public static final byte START_PUNCTUATION

END_PUNCTUATION

public static final byte END_PUNCTUATION

INITIAL_QUOTE_PUNCTUATION

public static final byte INITIAL_QUOTE_PUNCTUATION

FINAL_QUOTE_PUNCTUATION

public static final byte FINAL_QUOTE_PUNCTUATION

OTHER_PUNCTUATION

public static final byte OTHER_PUNCTUATION

MATH_SYMBOL

public static final byte MATH_SYMBOL

CURRENCY_SYMBOL

public static final byte CURRENCY_SYMBOL

MODIFIER_SYMBOL

public static final byte MODIFIER_SYMBOL

OTHER_SYMBOL

public static final byte OTHER_SYMBOL

CHAR_ERROR

static final char CHAR_ERROR

DIRECTIONALITY_UNDEFINED

public static final byte DIRECTIONALITY_UNDEFINED

DIRECTIONALITY_LEFT_TO_RIGHT

public static final byte DIRECTIONALITY_LEFT_TO_RIGHT

DIRECTIONALITY_RIGHT_TO_LEFT

public static final byte DIRECTIONALITY_RIGHT_TO_LEFT

DIRECTIONALITY_RIGHT_TO_LEFT_ARABIC

public static final byte DIRECTIONALITY_RIGHT_TO_LEFT_ARABIC

DIRECTIONALITY_EUROPEAN_NUMBER

public static final byte DIRECTIONALITY_EUROPEAN_NUMBER

DIRECTIONALITY_EUROPEAN_NUMBER_SEPARATOR

public static final byte DIRECTIONALITY_EUROPEAN_NUMBER_SEPARATOR

DIRECTIONALITY_EUROPEAN_NUMBER_TERMINATOR

public static final byte DIRECTIONALITY_EUROPEAN_NUMBER_TERMINATOR

DIRECTIONALITY_ARABIC_NUMBER

public static final byte DIRECTIONALITY_ARABIC_NUMBER

DIRECTIONALITY_COMMON_NUMBER_SEPARATOR

public static final byte DIRECTIONALITY_COMMON_NUMBER_SEPARATOR

DIRECTIONALITY_NONSPACING_MARK

public static final byte DIRECTIONALITY_NONSPACING_MARK

DIRECTIONALITY_BOUNDARY_NEUTRAL

public static final byte DIRECTIONALITY_BOUNDARY_NEUTRAL

DIRECTIONALITY_PARAGRAPH_SEPARATOR

public static final byte DIRECTIONALITY_PARAGRAPH_SEPARATOR

DIRECTIONALITY_SEGMENT_SEPARATOR

public static final byte DIRECTIONALITY_SEGMENT_SEPARATOR

DIRECTIONALITY_WHITESPACE

public static final byte DIRECTIONALITY_WHITESPACE

DIRECTIONALITY_OTHER_NEUTRALS

public static final byte DIRECTIONALITY_OTHER_NEUTRALS

DIRECTIONALITY_LEFT_TO_RIGHT_EMBEDDING

public static final byte DIRECTIONALITY_LEFT_TO_RIGHT_EMBEDDING

DIRECTIONALITY_LEFT_TO_RIGHT_OVERRIDE

public static final byte DIRECTIONALITY_LEFT_TO_RIGHT_OVERRIDE

DIRECTIONALITY_RIGHT_TO_LEFT_EMBEDDING

public static final byte DIRECTIONALITY_RIGHT_TO_LEFT_EMBEDDING

DIRECTIONALITY_RIGHT_TO_LEFT_OVERRIDE

public static final byte DIRECTIONALITY_RIGHT_TO_LEFT_OVERRIDE

DIRECTIONALITY_POP_DIRECTIONAL_FORMAT

public static final byte DIRECTIONALITY_POP_DIRECTIONAL_FORMAT

Character

public Character(char value)

Specifications: (class)pure

public normal_behavior
assignable ch_;
ensures this.ch_ == value;

digitVal

public static int digitVal(char ch)

Specifications: pure

charValue

public char charValue()

Specifications: (class)pure

public normal_behavior
ensures \result == this.ch_;

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications: (class)pure

     also

public normal_behavior
ensures \result >= 0&&(* \result is a hash code for ch_ *);

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Object

Specifications: (class)pure

     also

public normal_behavior

{|

requires (obj instanceof java.lang.Character);
ensures \result <==> ((java.lang.Character)obj).ch_ == this.ch_;

also

requires !(obj instanceof java.lang.Character);
ensures \result <==> false;

|}

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null (class)pure

     also

public normal_behavior
ensures \result .length() == 1&&\result .charAt(0) == this.ch_;

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

toString

public static String toString(char c)

Specifications: pure non_null

public normal_behavior
ensures \result .length() == 1&&\result .charAt(0) == c;

isLowerCase

public static boolean isLowerCase(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 2;

isUpperCase

public static boolean isUpperCase(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 1;

isTitleCase

public static boolean isTitleCase(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 3;

isDigit

public static boolean isDigit(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 9;

isDefined

public static boolean isDefined(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) != 0;

isLetter

public static boolean isLetter(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 1||getType(ch) == 2||getType(ch) == 3||getType(ch) == 4||getType(ch) == 5;

isLetterOrDigit

public static boolean isLetterOrDigit(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> isDigit(ch)||isLetter(ch);

isJavaLetter

public static boolean isJavaLetter(char ch)

Deprecated. Replaced by isJavaIdentifierStart(char).

Specifications: pure

public normal_behavior
ensures \result <==> isJavaIdentifierStart(ch);

isJavaLetterOrDigit

public static boolean isJavaLetterOrDigit(char ch)

Deprecated. Replaced by isJavaIdentifierPart(char).

Specifications: pure

public normal_behavior
ensures \result <==> isJavaIdentifierPart(ch);

isJavaIdentifierStart

public static boolean isJavaIdentifierStart(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> isLetter(ch)||getType(ch) == 26||getType(ch) == 23;
ensures_redundantly \result <==> (* ch is permissible as the first character in a Java identifier *);

isJavaIdentifierPart

public static boolean isJavaIdentifierPart(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> isJavaIdentifierStart(ch)||isDigit(ch)||getType(ch) == 10||getType(ch) == 8||getType(ch) == 6||isIdentifierIgnorable(ch);
ensures_redundantly \result <==> (* ch is permissible as a character in a Java identifier *);

isUnicodeIdentifierStart

public static boolean isUnicodeIdentifierStart(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> isLetter(ch);
ensures_redundantly \result <==> (* ch is permissible as the first character in a Unicode identifier *);

isUnicodeIdentifierPart

public static boolean isUnicodeIdentifierPart(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> isLetter(ch)||getType(ch) == 23||isDigit(ch)||getType(ch) == 10||getType(ch) == 8||getType(ch) == 6||isIdentifierIgnorable(ch);
ensures_redundantly \result <==> (* ch is permissible as a character in a Unicode identifier *);

isIdentifierIgnorable

public static boolean isIdentifierIgnorable(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> (0 <= ch&&ch <= 8)||(14 <= ch&&ch <= 27)||(127 <= ch&&ch <= 159)||(8204 <= ch&&ch <= 8207)||(8202 <= ch&&ch <= 8206)||(8298 <= ch&&ch <= 8303)||ch == 65279;
ensures_redundantly \result <==> (* ch is an ignorable character in a Java identifier or a Unicode identifier *);

toLowerCase

public static char toLowerCase(char ch)

Specifications: pure

public normal_behavior

{|

requires (* a lowercase mapping is specified for ch in the Unicode attribute table *);
ensures (* \result == the lowercase mapping of ch in the Unicode attribute table *);

also

requires (* !(a lowercase mapping is specified for ch in the Unicode attribute table) *);
ensures \result == ch;

|}

toUpperCase

public static char toUpperCase(char ch)

Specifications: pure

public normal_behavior

{|

requires (* an uppercase mapping is specified for ch in the Unicode attribute table *);
ensures (* \result == the uppercase mapping of ch in the Unicode attribute table *);

also

requires (* !(an uppercase mapping is specified for ch in the Unicode attribute table) *);
ensures \result == ch;

|}

toTitleCase

public static char toTitleCase(char ch)

Specifications: pure

public normal_behavior

{|

requires (* a titlecase mapping is specified for ch in the Unicode attribute table *);
ensures (* \result == the titlecase mapping of ch in the Unicode attribute table *);

also

requires (* !(a titlecase mapping is specified for ch in the Unicode attribute table) *);
ensures \result == ch;

|}

digit

public static int digit(char ch,
                        int radix)

Specifications: pure

public normal_behavior

{|

requires (2 <= radix&&radix <= 36)&&isDigit(ch)&&digitVal(ch) < radix;
ensures \result == digitVal(ch);

also

requires (2 <= radix&&radix <= 36)&&(ch >= 65&&ch <= 90)&&(ch-65+10) < radix;
ensures \result == (ch-65+10);

also

requires (2 <= radix&&radix <= 36)&&(ch >= 97&&ch <= 122)&&(ch-97+10) < radix;
ensures \result == (ch-97+10);

also

requires radix < 2||radix > 36||(isDigit(ch)&&digitVal(ch) >= radix)||(ch >= 65&&ch <= 90&&(ch-65+10) >= radix)||(ch >= 97&&ch <= 122&&(ch-97+10) >= radix)||(!isDigit(ch)&&!(ch >= 65&&ch <= 90)&&!(ch >= 97&&ch <= 122));
requires_redundantly (* none of the other requires clauses are met *);
ensures \result == -1;

|}

getNumericValue

public static int getNumericValue(char ch)

Specifications: pure

public normal_behavior

{|

requires (* ch has a Unicode numeric value *);

{|

requires (* the Unicode numeric value of ch is a non-negative integer *);
ensures (* \result == the Unicode numeric value of ch *);

also

requires (* !(the Unicode numeric value of ch is a non-negative integer) *);
ensures \result == -2;

|}

also

requires (* !(ch has a Unicode numeric value) *);
ensures \result == -1;

|}

isSpace

public static boolean isSpace(char ch)

Deprecated. Replaced by isWhitespace(char).

Specifications: pure

public normal_behavior
ensures \result <==> ch == 9||ch == 10||ch == 12||ch == 13||ch == 32;

isSpaceChar

public static boolean isSpaceChar(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 12||getType(ch) == 13||getType(ch) == 14;

isWhitespace

public static boolean isWhitespace(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> (getType(ch) == 12&&ch != 160&&ch != 65279)||getType(ch) == 13||getType(ch) == 14||ch == 13||ch == 10||ch == 9||ch == 11||ch == 12||ch == 28||ch == 29||ch == 30||ch == 31;
ensures_redundantly \result <==> (* ch is a Java whitespace character *);

isISOControl

public static boolean isISOControl(char ch)

Specifications: pure

public normal_behavior
ensures \result <==> getType(ch) == 15;
ensures_redundantly \result <==> (0 <= ch&&ch <= 31)||(127 <= ch&&ch <= 159);

getType

public static int getType(char ch)

Specifications: pure

public normal_behavior
ensures 0 <= \result &&\result <= 28&&(* \result == the Unicode character category of ch *);

forDigit

public static char forDigit(int digit,
                            int radix)

Specifications: pure

public normal_behavior

{|

requires 2 <= radix&&radix <= 36&&0 <= digit&&digit <= radix&&digit < 10;
ensures \result == (char)(48+digit);

also

requires 2 <= radix&&radix <= 36&&0 <= digit&&digit <= radix&&digit > 10;
ensures \result == (char)(97+digit-10);

also

requires 2 > radix||radix > 36||0 > digit||digit > radix;
ensures \result == 0;

|}

getDirectionality

public static byte getDirectionality(char c)

Specifications: pure

isMirrored

public static boolean isMirrored(char c)

Specifications: pure

compareTo

public int compareTo(non_null Character anotherCharacter)

Specifications: (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareTo

public int compareTo(non_null Object o)

Specified by:

compareTo in interface Comparable

Specifications: (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

toUpperCaseEx

static char toUpperCaseEx(char ch)

Specifications: pure

toUpperCaseCharArray

static char[] toUpperCaseCharArray(char ch)

Specifications: pure non_null

findInCharMap

static int findInCharMap(char ch)

Specifications: pure