Class JMLResources

  extended byorg.jmlspecs.models.JMLResources

public class JMLResources
extends Object

Model variables for reasoning à la Eric Hehner.

$Revision: 1.11 $
Gary T. Leavens
See Also:
JMLInfiniteInteger, Runtime

Class Specifications
static public invariant org.jmlspecs.models.JMLResources.machineCycles != null;
static public invariant org.jmlspecs.models.JMLResources.machineCycles.greaterThanOrEqualTo(org.jmlspecs.models.JMLFiniteInteger.ZERO);
static public constraint org.jmlspecs.models.JMLResources.machineCycles.greaterThanOrEqualTo(\old(org.jmlspecs.models.JMLResources.machineCycles));
static public represents bytesUsed <- (long)(java.lang.Runtime.getRuntime().totalMemory()-java.lang.Runtime.getRuntime().freeMemory());

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
static long bytesUsed
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
Ghost Field Summary
static JMLInfiniteInteger machineCycles
          The number of JVM cycles used since beginning execution.
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
Constructor Summary
Model Method Summary
Model methods inherited from class java.lang.Object
Method Summary
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Model Field Detail


public static long bytesUsed
Ghost Field Detail


public static JMLInfiniteInteger machineCycles
The number of JVM cycles used since beginning execution.

A cycle is defined to be the time unit used (in the worst case) by the fastest source-level instruction in Java code. When such an instruction is executed, machineCycles increases by 1. All other instructions increase machineCycles by an appropriate amount, sometimes greater than 1.

Multiply machineCycles by the speed of your JVM to get the time used. For example, if your JVM executes one cycle every 2 milliseconds, then the number of milliseconds spent in execution is 2 * machineCycles.

We imagine that the number of machine cycles is infinite when the program goes into an infinite loop.

See Also:
JMLInfiniteInteger, JMLPositiveInfinity
Constructor Detail


public JMLResources()


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.