JML

org.jmlspecs.samples.misc
Class Meter

java.lang.Object
  extended byorg.jmlspecs.samples.misc.Meter
All Implemented Interfaces:
Counter

public class Meter
extends Object
implements Counter

A behavioral subtype of Counter.


Field Summary
protected  int count
          The count of how many times inc has been called.
 
Fields inherited from interface org.jmlspecs.samples.misc.Counter
CAPACITY
 
Constructor Summary
Meter()
          Initialize this Meter.
 
Method Summary
 void inc()
          A model of the value of this counter.
 int value()
          Return the value of this counter.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

count

protected int count
The count of how many times inc has been called.

Constructor Detail

Meter

public Meter()
Initialize this Meter.

Method Detail

inc

public void inc()
Description copied from interface: Counter
A model of the value of this counter. Increment this counter

Specified by:
inc in interface Counter

value

public int value()
Description copied from interface: Counter
Return the value of this counter.

Specified by:
value in interface Counter

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.