using Microsoft.Contracts; public class Counter { private int increments; private int decrements; public void increment() ensures get() == old(get()) + 1; { increments++; } public void decrement() ensures get() == old(get()) - 1; { decrements++; } [Pure] public int get() { return increments - decrements; } }