org.jmlspecs.samples.misc
Interface Counter

All Known Implementing Classes:

Meter

public interface Counter

A simple Counter. This class is a demo of behavioral subtyping.

Class Specifications

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

Specifications inherited from class Object

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

Model Field Summary
[instance]  int	val           A model of the value of this counter.

 

Field Summary
static int	CAPACITY           The capacity of this counter.

 

Method Summary
void	inc()           Increment this counter
int	value()           Return the value of this counter.

 

Model Field Detail

val

public int val

A model of the value of this counter.

Specifications: instance
datagroup contains: org.jmlspecs.samples.misc.Meter.count

CAPACITY

public static final int CAPACITY

The capacity of this counter.

inc

public void inc()

Increment this counter

Specifications:

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

value

public int value()

Return the value of this counter.

Specifications: pure

ensures \result == this.val;