Meter (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.samples.misc
Class Meter

java.lang.Object
  org.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()