JML

java.lang
Class SecurityManager

java.lang.Object
  extended byjava.lang.SecurityManager

public class SecurityManager
extends Object

JML's specification of java.lang.SecurityManager

Version:
$Revision: 1.4 $
Author:
Gary T. Leavens and Tabitha Johnson

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
protected  boolean inCheck
          Deprecated.  
 
Constructor Summary
SecurityManager()
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 void checkAccept(String host, int port)
           
 void checkAccess(Thread t)
           
 void checkAccess(ThreadGroup g)
           
 void checkAwtEventQueueAccess()
           
 void checkConnect(String host, int port)
           
 void checkConnect(String host, int port, Object context)
           
 void checkCreateClassLoader()
           
 void checkDelete(String file)
           
 void checkExec(String cmd)
           
 void checkExit(int status)
           
 void checkLink(String lib)
           
 void checkListen(int port)
           
 void checkMemberAccess(Class clazz, int which)
           
 void checkMulticast(InetAddress maddr)
           
 void checkMulticast(InetAddress maddr, byte ttl)
          Deprecated.  
 void checkPackageAccess(String pkg)
           
 void checkPackageDefinition(String pkg)
           
 void checkPermission(Permission perm)
           
 void checkPermission(Permission perm, nullable Object context)
           
 void checkPrintJobAccess()
           
 void checkPropertiesAccess()
           
 void checkPropertyAccess(String key)
           
 void checkRead(FileDescriptor fd)
           
 void checkRead(String file)
           
 void checkRead(String file, Object context)
           
 void checkSecurityAccess(String target)
           
 void checkSetFactory()
           
 void checkSystemClipboardAccess()
           
 boolean checkTopLevelWindow(Object window)
           
 void checkWrite(FileDescriptor fd)
           
 void checkWrite(String file)
           
protected  int classDepth(String name)
          Deprecated.  
protected  int classLoaderDepth()
          Deprecated.  
protected  ClassLoader currentClassLoader()
          Deprecated.  
protected  Class currentLoadedClass()
          Deprecated.  
protected  Class[] getClassContext()
           
 boolean getInCheck()
          Deprecated.  
 Object getSecurityContext()
           
 ThreadGroup getThreadGroup()
           
protected  boolean inClass(String name)
          Deprecated.  
protected  boolean inClassLoader()
          Deprecated.  
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

inCheck

protected boolean inCheck
Deprecated.  

Constructor Detail

SecurityManager

public SecurityManager()
Specifications:
signals_only java.lang.SecurityException;
Method Detail

getInCheck

public boolean getInCheck()
Deprecated.  


getClassContext

protected Class[] getClassContext()
Specifications:
ensures \nonnullelements(\result );

currentClassLoader

protected ClassLoader currentClassLoader()
Deprecated.  


currentLoadedClass

protected Class currentLoadedClass()
Deprecated.  


classDepth

protected int classDepth(String name)
Deprecated.  


classLoaderDepth

protected int classLoaderDepth()
Deprecated.  


inClass

protected boolean inClass(String name)
Deprecated.  


inClassLoader

protected boolean inClassLoader()
Deprecated.  


getSecurityContext

public Object getSecurityContext()
Specifications:
ensures_redundantly \result != null;

checkPermission

public void checkPermission(Permission perm)
Specifications: pure
requires_redundantly perm != null;
signals_only java.lang.SecurityException;

checkPermission

public void checkPermission(Permission perm,
                            nullable Object context)
Specifications: pure
requires context instanceof java.security.AccessControlContext;
requires_redundantly perm != null;
signals_only java.security.AccessControlException;
     also
requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;
    implies_that
requires context == null;
signals_only java.lang.SecurityException;

checkCreateClassLoader

public void checkCreateClassLoader()
Specifications: pure
signals_only java.lang.SecurityException;

checkAccess

public void checkAccess(Thread t)
Specifications: pure
requires_redundantly t != null;
signals_only java.lang.SecurityException;

checkAccess

public void checkAccess(ThreadGroup g)
Specifications: pure
requires_redundantly g != null;
signals_only java.lang.SecurityException;

checkExit

public void checkExit(int status)
Specifications: pure
signals_only java.lang.SecurityException;

checkExec

public void checkExec(String cmd)
Specifications: pure
requires_redundantly cmd != null;
signals_only java.lang.SecurityException;

checkLink

public void checkLink(String lib)
Specifications: pure
requires_redundantly lib != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(FileDescriptor fd)
Specifications: pure
requires_redundantly fd != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(String file)
Specifications: pure
requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(String file,
                      Object context)
Specifications: pure
requires context instanceof java.security.AccessControlContext;
requires_redundantly file != null;
signals_only java.security.AccessControlException;
     also
requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;
    implies_that
requires context == null;
signals_only java.lang.SecurityException;

checkWrite

public void checkWrite(FileDescriptor fd)
Specifications: pure
requires_redundantly fd != null;
signals_only java.lang.SecurityException;

checkWrite

public void checkWrite(String file)
Specifications: pure
requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkDelete

public void checkDelete(String file)
Specifications: pure
requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkConnect

public void checkConnect(String host,
                         int port)
Specifications: pure
requires_redundantly host != null;
signals_only java.lang.SecurityException;

checkConnect

public void checkConnect(String host,
                         int port,
                         Object context)
Specifications: pure
requires context instanceof java.security.AccessControlContext;
requires_redundantly host != null;
signals_only java.security.AccessControlException;
     also
requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;
    implies_that
requires context == null;
signals_only java.lang.SecurityException;

checkListen

public void checkListen(int port)
Specifications: pure
signals_only java.lang.SecurityException;

checkAccept

public void checkAccept(String host,
                        int port)
Specifications: pure
requires_redundantly host != null;
signals_only java.lang.SecurityException;

checkMulticast

public void checkMulticast(InetAddress maddr)
Specifications: pure
requires_redundantly maddr != null;
signals_only java.lang.SecurityException;

checkMulticast

public void checkMulticast(InetAddress maddr,
                           byte ttl)
Deprecated.  

Specifications: pure
requires_redundantly maddr != null;
signals_only java.lang.SecurityException;

checkPropertiesAccess

public void checkPropertiesAccess()
Specifications: pure
signals_only java.lang.SecurityException;

checkPropertyAccess

public void checkPropertyAccess(String key)
Specifications: pure
requires_redundantly key != null;
signals_only java.lang.SecurityException;

checkTopLevelWindow

public boolean checkTopLevelWindow(Object window)
Specifications: pure
requires_redundantly window != null;

checkPrintJobAccess

public void checkPrintJobAccess()
Specifications: pure
signals_only java.lang.SecurityException;

checkSystemClipboardAccess

public void checkSystemClipboardAccess()
Specifications: pure
signals_only java.lang.SecurityException;

checkAwtEventQueueAccess

public void checkAwtEventQueueAccess()
Specifications: pure
signals_only java.lang.SecurityException;

checkPackageAccess

public void checkPackageAccess(String pkg)
Specifications: pure
requires_redundantly pkg != null;
signals_only java.lang.SecurityException;

checkPackageDefinition

public void checkPackageDefinition(String pkg)
Specifications: pure
requires_redundantly pkg != null;
signals_only java.lang.SecurityException;

checkSetFactory

public void checkSetFactory()
Specifications: pure
signals_only java.lang.SecurityException;

checkMemberAccess

public void checkMemberAccess(Class clazz,
                              int which)
Specifications: pure
requires_redundantly clazz != null;
signals_only java.lang.SecurityException;

checkSecurityAccess

public void checkSecurityAccess(String target)
Specifications: pure
requires !target.equals("");
signals_only java.lang.SecurityException;

getThreadGroup

public ThreadGroup getThreadGroup()
Specifications: pure
ensures_redundantly \result != null;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.