content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.util;
  
  public final class Locale extends java.lang.Object implements java.lang.Cloneable, java.io.Serializable
  {
     public final static java.util.Locale ENGLISH;
     public final static java.util.Locale FRENCH;
     public final static java.util.Locale GERMAN;
     public final static java.util.Locale ITALIAN;
     public final static java.util.Locale JAPANESE;
     public final static java.util.Locale KOREAN;
     public final static java.util.Locale CHINESE;
     public final static java.util.Locale SIMPLIFIED_CHINESE;
     public final static java.util.Locale TRADITIONAL_CHINESE;
     public final static java.util.Locale FRANCE;
     public final static java.util.Locale GERMANY;
     public final static java.util.Locale ITALY;
     public final static java.util.Locale JAPAN;
     public final static java.util.Locale KOREA;
     public final static java.util.Locale CHINA;
     public final static java.util.Locale PRC;
     public final static java.util.Locale TAIWAN;
     public final static java.util.Locale UK;
     public final static java.util.Locale US;
     public final static java.util.Locale CANADA;
     public final static java.util.Locale CANADA_FRENCH;
     public final static java.util.Locale ROOT;
     public final static char PRIVATE_USE_EXTENSION = 120;
     public final static char UNICODE_LOCALE_EXTENSION = 117;
     final static long serialVersionUID = 9149081749638150636L;
     final static boolean $assertionsDisabled;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public Locale(java.lang.String arg0, java.lang.String arg1, java.lang.String arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Locale(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Locale(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Locale getDefault();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Locale getDefault(java.util.Locale$Category arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setDefault(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setDefault(java.util.Locale$Category arg0, java.util.Locale arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Locale[] getAvailableLocales();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String[] getISOCountries();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.String[] getISOLanguages();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getLanguage();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getScript();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getCountry();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getVariant();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getExtension(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Set getExtensionKeys();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Set getUnicodeLocaleAttributes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getUnicodeLocaleType(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Set getUnicodeLocaleKeys();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toLanguageTag();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.util.Locale forLanguageTag(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.util.MissingResourceException e) true; */
     public java.lang.String getISO3Language() throws java.util.MissingResourceException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.util.MissingResourceException e) true; */
     public java.lang.String getISO3Country() throws java.util.MissingResourceException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String getDisplayLanguage();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayLanguage(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayScript();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayScript(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String getDisplayCountry();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayCountry(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String getDisplayVariant();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayVariant(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String getDisplayName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getDisplayName(java.util.Locale arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object clone();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  }
  