class Counter { function method Value(): int reads this; { increments - decrements } var increments: int; var decrements: int; method Init() modifies this; ensures Value() == 0; { increments := 0; decrements := 0; } method Increment() modifies this; ensures Value() == old(Value()) + 1; { increments := increments + 1; } method Decrement() modifies this; ensures Value() == old(Value()) - 1; { decrements := decrements + 1; } method Get() returns (val: int) // this method is not needed, since function Value() can be used instead ensures val == Value(); { val := Value(); } }