java.lang
Class System

java.lang.Object
  java.lang.System

public final class System

extends Object

JML's specification of java.lang.System.

Version:

$Revision: 1.31 $

Author:

Gary T. Leavens

Class Specifications

static public represents SystemSecurityManager <- getSecurityManager(); static represents SystemProperties <- getProperties(); public initially java.lang.System.in != null; public initially java.lang.System.out != null; public initially java.lang.System.err != null;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
static JMLDataGroup	clock
static Properties	SystemProperties
static SecurityManager	SystemSecurityManager

 

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
static PrintStream	err
static InputStream	in
static PrintStream	out

 

Constructor Summary
private	System()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static void	arraycopy(non_null Object src, int srcPos, non_null Object dest, int destPos, int length)
static long	currentTimeMillis()
static void	exit(int status)
static void	gc()
(package private) static Class	getCallerClass()
static String	getenv(non_null String name)           Deprecated. use java.lang.System.getProperty.
static Properties	getProperties()
static String	getProperty(non_null String key)
static String	getProperty(non_null String key, String def)
static SecurityManager	getSecurityManager()
static int	identityHashCode(nullable Object x)
static void	load(non_null String filename)
static void	loadLibrary(non_null String libname)
static String	mapLibraryName(non_null String libname)
static void	runFinalization()
static void	runFinalizersOnExit(boolean value)           Deprecated. this is unsafe.
static void	setErr(PrintStream e)
static void	setIn(InputStream i)
static void	setOut(PrintStream o)
static void	setProperties(non_null Properties props)
static String	setProperty(non_null String key, non_null String value)
static void	setSecurityManager(nullable SecurityManager s)

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Model Field Detail

SystemSecurityManager

public static SecurityManager SystemSecurityManager

clock

public static transient JMLDataGroup clock

SystemProperties

public static Properties SystemProperties

in

public static final InputStream in

Specifications: non_null

out

public static final PrintStream out

Specifications: non_null

err

public static final PrintStream err

Specifications: non_null

System

private System()

Specifications: pure

setIn

public static void setIn(InputStream i)

Specifications:

assignable in;
ensures java.lang.System.in == i;

setOut

public static void setOut(PrintStream o)

Specifications:

assignable out;
ensures java.lang.System.out == o;

setErr

public static void setErr(PrintStream e)

Specifications:

assignable err;
ensures java.lang.System.err == e;

setSecurityManager

public static void setSecurityManager(nullable SecurityManager s)

Specifications:

public normal_behavior
requires s == null;
assignable \nothing;
ensures \not_modified(SystemSecurityManager);

     also

public behavior
requires s != null;
assignable SystemSecurityManager;
ensures java.lang.System.SystemSecurityManager == s;
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if the change is not permitted *);

getSecurityManager

public static SecurityManager getSecurityManager()

Specifications: pure nullable

ensures \result == java.lang.System.SystemSecurityManager;

currentTimeMillis

public static long currentTimeMillis()

Specifications:

assignable clock;

arraycopy

public static void arraycopy(non_null Object src,
                             int srcPos,
                             non_null Object dest,
                             int destPos,
                             int length)

Specifications:

public exceptional_behavior
requires !(src.getClass().isArray())||!(dest.getClass().isArray());
assignable \nothing;
signals_only java.lang.ArrayStoreException;

     also

public exceptional_behavior
requires !(!(src.getClass().isArray())||!(dest.getClass().isArray()));
requires (srcPos < 0||destPos < 0||length < 0||srcPos+length > ((java.lang.Object[])src).length||destPos+length > ((java.lang.Object[])dest).length);
assignable \nothing;
signals_only java.lang.ArrayIndexOutOfBoundsException;

     also

public normal_behavior
requires !(!(src.getClass().isArray())||!(dest.getClass().isArray()));
requires !(srcPos < 0||destPos < 0||length < 0);

{|

requires \elemtype(\typeof(src)) <: \type(java.lang.Object)&&\elemtype(\typeof(dest)) <: \type(java.lang.Object)&&srcPos+length <= ((java.lang.Object[])src).length&&destPos+length <= ((java.lang.Object[])dest).length;

{|

old java.lang.Object[] sa = (java.lang.Object[])src;
old java.lang.Object[] da = (java.lang.Object[])dest;
assignable da[destPos .. destPos+length-1];
ensures ( \forall int i; 0 <= i&&i < length; \old(sa[(int)(srcPos+i)]) == da[(int)(destPos+i)]);

|}

also

requires \elemtype(\typeof(src)) == \type(int)&&\elemtype(\typeof(dest)) == \type(int)&&srcPos+length <= ((int[])src).length&&destPos+length <= ((int[])dest).length;

{|

old int[] sa = (int[])src;
old int[] da = (int[])dest;
assignable da[destPos .. destPos+length-1];
ensures ( \forall int i; 0 <= i&&i < length; sa[(int)(srcPos+i)] == da[(int)(destPos+i)]);

|}

|}

    implies_that

requires length >= 0&&0 <= srcPos&&0 <= destPos;

identityHashCode

public static int identityHashCode(nullable Object x)

Specifications: pure

getProperties

public static Properties getProperties()

Specifications: pure non_null

public behavior
ensures \result != null&&\result .equals(java.lang.System.SystemProperties);
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if access is not permitted *);

setProperties

public static void setProperties(non_null Properties props)

Specifications:

public behavior
assignable SystemProperties;
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if access is not permitted *);

getProperty

public static String getProperty(non_null String key)

Specifications: pure nullable

signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if access is not permitted *);

getProperty

public static String getProperty(non_null String key,
                                 String def)

Specifications: pure nullable

ensures def != null ==> \result != null;
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if access is not permitted *);

setProperty

public static String setProperty(non_null String key,
                                 non_null String value)

Specifications: nullable

public behavior
assignable SystemProperties;
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if access is not permitted *);

getenv

public static String getenv(non_null String name)

Deprecated. use java.lang.System.getProperty.

Specifications: pure nullable

exit

public static void exit(int status)

Specifications:

public behavior
diverges true;
assignable \nothing;
ensures false;
signals_only java.lang.SecurityException;
signals (java.lang.SecurityException) (* if exiting is not permitted *);

    implies_that

ensures false;

gc

public static void gc()

runFinalization

public static void runFinalization()

runFinalizersOnExit

public static void runFinalizersOnExit(boolean value)

Deprecated. this is unsafe.

load

public static void load(non_null String filename)

loadLibrary

public static void loadLibrary(non_null String libname)

mapLibraryName

public static String mapLibraryName(non_null String libname)

Specifications: pure

getCallerClass

static Class getCallerClass()