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 class Properties extends java.util.Hashtable
  {
     protected java.util.Properties defaults;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public Properties();
  
     /*@ requires true; ensures true; assignable \everything; */
     public Properties(java.util.Properties arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object setProperty(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void load(java.io.Reader arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void load(java.io.InputStream arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public void save(java.io.OutputStream arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void store(java.io.Writer arg0, java.lang.String arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void store(java.io.OutputStream arg0, java.lang.String arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; signals (java.util.InvalidPropertiesFormatException e) true; */
     public void loadFromXML(java.io.InputStream arg0) throws java.io.IOException, java.util.InvalidPropertiesFormatException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void storeToXML(java.io.OutputStream arg0, java.lang.String arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void storeToXML(java.io.OutputStream arg0, java.lang.String arg1, java.lang.String arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getProperty(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getProperty(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Enumeration propertyNames();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Set stringPropertyNames();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void list(java.io.PrintStream arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void list(java.io.PrintWriter arg0);
  }
  