content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.security.cert;
  
  public abstract class CertPath extends java.lang.Object implements java.io.Serializable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected CertPath(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getType();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.Iterator getEncodings();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.security.cert.CertificateEncodingException e) true; */
     public abstract byte[] getEncoded() throws java.security.cert.CertificateEncodingException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.security.cert.CertificateEncodingException e) true; */
     public abstract byte[] getEncoded(java.lang.String arg0) throws java.security.cert.CertificateEncodingException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.List getCertificates();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.ObjectStreamException e) true; */
     protected java.lang.Object writeReplace() throws java.io.ObjectStreamException;
  }
  