01: // @(#)$Id: JMLResources.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
02:
03: // Copyright (C) 1998, 1999 Iowa State University
04:
05: // This file is part of JML
06:
07: // JML is free software; you can redistribute it and/or modify
08: // it under the terms of the GNU General Public License as published by
09: // the Free Software Foundation; either version 2, or (at your option)
10: // any later version.
11:
12: // JML is distributed in the hope that it will be useful,
13: // but WITHOUT ANY WARRANTY; without even the implied warranty of
14: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: // GNU General Public License for more details.
16:
17: // You should have received a copy of the GNU General Public License
18: // along with JML; see the file COPYING. If not, write to
19: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
20:
21: package org.jmlspecs.models;
22:
23: import java.math.BigInteger;
24:
25: /** Model variables for reasoning à la Eric Hehner.
26: *
27: * @version $Revision: 1.1 $
28: * @author Gary T. Leavens
29: * @see JMLInfiniteInteger
30: * @see Runtime
31: */
32: //-@ immutable
33: public/*@ pure @*/class JMLResources {
34:
35: /** The number of JVM cycles used since beginning execution.
36: *
37: * <p> A cycle is defined to be the time unit used (in the worst
38: * case) by the fastest source-level instruction in Java code.
39: * When such an instruction is executed, machineCycles increases
40: * by 1. All other instructions increase machineCycles by an
41: * appropriate amount, sometimes greater than 1.
42: *
43: * <p> Multiply machineCycles by the speed of your JVM to get the
44: * time used. For example, if your JVM executes one cycle every
45: * 2 milliseconds, then the number of milliseconds spent in
46: * execution is 2 * machineCycles.
47: *
48: * <p>We imagine that the number of machine cycles is infinite
49: * when the program goes into an infinite loop.
50: *
51: * @see JMLInfiniteInteger
52: * @see JMLPositiveInfinity
53: */
54: //@ ghost public static JMLInfiniteInteger machineCycles;
55: static {
56: //@ set machineCycles = JMLFiniteInteger.ZERO;
57: }
58:
59: //@ public static invariant machineCycles != null;
60: /*@ public static invariant machineCycles.greaterThanOrEqualTo(
61: @ JMLFiniteInteger.ZERO);
62: @ public static constraint machineCycles.greaterThanOrEqualTo(
63: @ \old(machineCycles));
64: @*/
65:
66: //@ public static model long bytesUsed;
67: /*@ public static represents bytesUsed
68: @ <- (long)(Runtime.getRuntime().totalMemory()
69: @ - Runtime.getRuntime().freeMemory());
70: @*/
71: }
|