content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.security;
  
  public class ProtectionDomain extends java.lang.Object
  {
     final java.security.ProtectionDomain$Key key;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public ProtectionDomain(java.security.CodeSource arg0, java.security.PermissionCollection arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public ProtectionDomain(java.security.CodeSource arg0, java.security.PermissionCollection arg1, java.lang.ClassLoader arg2, java.security.Principal[] arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.security.CodeSource getCodeSource();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.ClassLoader getClassLoader();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.security.Principal[] getPrincipals();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.security.PermissionCollection getPermissions();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean implies(java.security.Permission arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  }
  