java.util
Class Locale

java.lang.Object
  java.util.Locale

All Implemented Interfaces:

Cloneable, Serializable

public final class Locale

extends Object

implements Cloneable, Serializable

Class Specifications

Specifications inherited from class Object

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

Model Field Summary

 

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
static Locale	CANADA
static Locale	CANADA_FRENCH
static Locale	CHINA
static Locale	CHINESE
static Locale	ENGLISH
static Locale	FRANCE
static Locale	FRENCH
static Locale	GERMAN
static Locale	GERMANY
static Locale	ITALIAN
static Locale	ITALY
static Locale	JAPAN
static Locale	JAPANESE
static Locale	KOREA
static Locale	KOREAN
static Locale	PRC
(package private) static long	serialVersionUID
static Locale	SIMPLIFIED_CHINESE
static Locale	TAIWAN
static Locale	TRADITIONAL_CHINESE
static Locale	UK
static Locale	US

 

Constructor Summary

Locale(String language)

Locale(String language, String country)

Locale(String language, String country, String variant)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()
boolean	equals(nullable Object obj)
static Locale[]	getAvailableLocales()
String	getCountry()
static Locale	getDefault()
String	getDisplayCountry()
String	getDisplayCountry(Locale inLocale)
String	getDisplayLanguage()
String	getDisplayLanguage(Locale inLocale)
String	getDisplayName()
String	getDisplayName(Locale inLocale)
String	getDisplayVariant()
String	getDisplayVariant(Locale inLocale)
String	getISO3Country()
String	getISO3Language()
static String[]	getISOCountries()
static String[]	getISOLanguages()
String	getLanguage()
String	getVariant()
int	hashCode()
static void	setDefault(Locale newLocale)
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Field Detail

ENGLISH

public static final Locale ENGLISH

FRENCH

public static final Locale FRENCH

GERMAN

public static final Locale GERMAN

ITALIAN

public static final Locale ITALIAN

JAPANESE

public static final Locale JAPANESE

KOREAN

public static final Locale KOREAN

CHINESE

public static final Locale CHINESE

SIMPLIFIED_CHINESE

public static final Locale SIMPLIFIED_CHINESE

TRADITIONAL_CHINESE

public static final Locale TRADITIONAL_CHINESE

FRANCE

public static final Locale FRANCE

GERMANY

public static final Locale GERMANY

ITALY

public static final Locale ITALY

JAPAN

public static final Locale JAPAN

KOREA

public static final Locale KOREA

CHINA

public static final Locale CHINA

PRC

public static final Locale PRC

TAIWAN

public static final Locale TAIWAN

UK

public static final Locale UK

US

public static final Locale US

CANADA

public static final Locale CANADA

CANADA_FRENCH

public static final Locale CANADA_FRENCH

serialVersionUID

static final long serialVersionUID

Locale

public Locale(String language,
              String country,
              String variant)

Locale

public Locale(String language,
              String country)

Locale

public Locale(String language)

getDefault

public static Locale getDefault()

Specifications: pure

setDefault

public static void setDefault(Locale newLocale)

Specifications:

public normal_behavior
requires newLocale != null;
assignable \everything;
ensures getDefault() == newLocale;

getAvailableLocales

public static Locale[] getAvailableLocales()

Specifications: pure

ensures \result != null;

getISOCountries

public static String[] getISOCountries()

Specifications: pure

ensures \result != null;

getISOLanguages

public static String[] getISOLanguages()

Specifications: pure

ensures \result != null;

getLanguage

public String getLanguage()

Specifications: pure

ensures \result != null;

getCountry

public String getCountry()

Specifications: pure

ensures \result != null;

getVariant

public String getVariant()

Specifications: pure

ensures \result != null;

toString

public final String toString()

Overrides:

toString in class Object

Specifications: pure

     also

ensures \result != null;

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;

getISO3Language

public String getISO3Language()
                       throws MissingResourceException

Throws:

MissingResourceException

Specifications: pure

ensures \result != null;

getISO3Country

public String getISO3Country()
                      throws MissingResourceException

Throws:

MissingResourceException

Specifications: pure

ensures \result != null;

getDisplayLanguage

public final String getDisplayLanguage()

Specifications: pure

ensures \result != null;

getDisplayLanguage

public String getDisplayLanguage(Locale inLocale)

Specifications: pure

public normal_behavior
requires inLocale != null;
ensures \result != null;

getDisplayCountry

public final String getDisplayCountry()

Specifications: pure

ensures \result != null;

getDisplayCountry

public String getDisplayCountry(Locale inLocale)

Specifications: pure

public normal_behavior
requires inLocale != null;
ensures \result != null;

getDisplayVariant

public final String getDisplayVariant()

Specifications: pure

ensures \result != null;

getDisplayVariant

public String getDisplayVariant(Locale inLocale)

Specifications: pure

public normal_behavior
requires inLocale != null;
ensures \result != null;

getDisplayName

public final String getDisplayName()

Specifications: pure

ensures \result != null;

getDisplayName

public String getDisplayName(Locale inLocale)

Specifications: pure

public normal_behavior
requires inLocale != null;
ensures \result != null;

clone

public Object clone()

Overrides:

clone in class Object

Specifications:

     also

ensures \result != null;

Specifications inherited from overridden method in class Object:
       non_null

protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);

     also

protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));

     also

protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;

     also

protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

hashCode

public int hashCode()

Overrides:

hashCode in class Object

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: pure

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 ;