public class CounterFunction { //@ public JMLDataGroup valueFoot; private int increments; //@ in valueFoot; private int decrements; //@ in valueFoot; /*@ public pure model @ int value() { @ return increments - decrements; @ } @*/ //@ assignable valueFoot; //@ ensures value() == 0; public CounterFunction() { increments = 0; decrements = 0; } //@ assignable valueFoot; //@ ensures value() == \old(value()+1); public void increment() { increments = increments + 1; } //@ assignable valueFoot; //@ ensures value() == \old(value()-1); public void decrement() { decrements = decrements + 1; } //@ ensures \result == value(); public /*@ pure @*/ int get() { return increments - decrements; } }