org.jmlspecs.models
Class JMLResources

java.lang.Object
  org.jmlspecs.models.JMLResources

public class JMLResources

extends Object

Model variables for reasoning à la Eric Hehner.

Version:

$Revision: 1.11 $

Author:

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

JMLResources()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

bytesUsed

public static long bytesUsed

machineCycles

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

JMLResources

public JMLResources()