public class Counter { private int increments; private int decrements; sealed model int value { // We declared the model field sealed because subclasses cannot see the satisfies clause (since increments and decrements are private) satisfies value == increments - decrements; } public void increment() ensures value == old(value) + 1; { expose(this) // The expose statement is required by the Spec# methodology because a model field depends on the updated field increments++; } public void decrement() ensures value == old(value) - 1; { expose(this) // The expose statement is required by the Spec# methodology because a model field depends on the updated field decrements++; } public int get() ensures result == value; { return increments - decrements; } }