class Counter { ghost var Value: int; function Valid(): bool reads this; { Value == increments - decrements } var increments: int; var decrements: int; method Init() modifies this; ensures Valid() && Value == 0; { increments := 0; decrements := 0; Value := 0; } method Increment() requires Valid(); modifies this; ensures Valid() && Value == old(Value) + 1; { increments := increments + 1; Value := Value + 1; } method Decrement() requires Valid(); modifies this; ensures Valid() && Value == old(Value) - 1; { decrements := decrements + 1; Value := Value - 1; } method Get() returns (val: int) requires Valid(); ensures val == Value; { val := increments - decrements; } }