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.

Class Specifications

protected represents val <- this.count;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Counter

instance public invariant 0 <= this.val&&this.val < 100;

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.misc.Counter

val

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

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.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	inc()           Increment 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.

Specifications:
is in groups: val

Meter

public Meter()

Initialize this Meter.

Specifications:

assignable val;
ensures this.val == 0;

inc

public void inc()

Description copied from interface: Counter

Increment this counter

Specified by:

inc in interface Counter

Specifications inherited from overridden method in interface Counter:

requires this.val < 100;
assignable val;
ensures this.val == \old(this.val+1);

value

public int value()

Description copied from interface: Counter

Return the value of this counter.

Specified by:

value in interface Counter

Specifications: pure

Specifications inherited from overridden method in interface Counter:
       pure

ensures \result == this.val;